Instancias solucionables en tiempo polinómico de Max-Sat

18

El problema Max-Sat le pide que encuentre una asignación de una fórmula CNF que satisfaga tantas cláusulas como sea posible.

Para el problema SAT más simple, existen muchos casos especiales conocidos que pueden resolverse en tiempo polinómico, por ejemplo, podemos resolver 2-SAT en tiempo polinómico.

Para Max-Sat la situación es diferente ya que Max-Sat es NP-hard incluso para fórmulas de 2-CNF (cada cláusula contiene solo 2 variables).

¿Hay alguna entrada especial interesante para la cual Max-Sat sea polinomial?

En particular, me interesaría una referencia estándar para resolver Max-Sat cuando el gráfico de incesión ha acotado el ancho del árbol.

sat treewidth max2sat Martin Vatshelle
fuente
3
Planar max-cut es un caso especial de max-cut, que es (en cierto sentido) un caso especial de max-2-sat.
Jukka Suomela

Respuestas:

6

Esto no responde directamente a su problema de Max-SAT, pero las referencias pueden guiarlo a la respuesta completa.

Szeider demostró que la Satisfacción es manejable con parámetros fijos cuando se parametriza por el ancho del árbol del gráfico de incidencia. Samer y Szeider dieron un algoritmo de programación dinámica eficiente.

Referencias

S. Szeider. En parametrizaciones manejables de parámetros fijos de SAT. En proc. 6ª Conferencia Internacional sobre Teoría y Aplicaciones de la Satisfacción (SAT'03), Documentos seleccionados y revisados, vol. 2919 de LNCS, páginas 188–202. Springer-Verlag, 2004.

M. Samer y S. Szeider. Algoritmos para el conteo de modelos proposicionales. En proc. XIV Conferencia Internacional sobre Lógica para la Programación, Inteligencia Artificial y Razonamiento (LPAR'07), vol. 4790 de LNCS, páginas 484–498. Springer-Verlag, 2007.

Samer y Szeider, trazabilidad de parámetros fijos. En A. Biere, M. Heule, H. van Maaren y T. Walsh, editores, Manual de satisfacción, parte 1, capítulo 13. IOS Press

Mohammad Al-Turkistany
fuente
Sé que algunos de los trabajos de Stefan Szeiders, un artículo más reciente muestra que #SAT es polinomial cuando el gráfico de incesión tiene un ancho de camarilla acotado que también implica un ancho de árbol acotado (aunque aquí tenemos tiempo de ejecución XP en lugar de FPT). Friedrich Slivovsky y Stefan Szeider, Modelo de conteo de fórmulas de ancho de camarilla acotada, algoritmos y cómputo, vol. 8283, pág. 677-687, LNCS, 2013 Sé que este tipo de resultados a menudo se traduciría en MAX-SAT, pero sería mucho más fácil tener una referencia donde esto ya se hace en lugar de hacerlo yo mismo.
Martin Vatshelle