¿Casos especiales de SAT y #SAT correspondiente con una complejidad mayor a O (n ^ 2) Y que tienen algoritmos eficientes para generar instancias?

Question

Estoy interesado en aprender sobre casos especiales de problemas de satisfacibilidad booleanos que se sabe que son polinomiales (o más realista, O (N ^ 2)).Estos casos también deberían tener un algoritmo eficiente para generar realmente todas las instancias satisfactorias, donde por eficiente me refiero a que se necesita O (N #SAT) para generar una secuencia de todas las instancias.Es posible que la segunda condición implique la primera, pero no me queda claro.

Ejemplo trivial: 1SAT :)

Ejemplo trivial: 2SAT con "cadenas" de cláusulas, de modo que el gráfico que une variables con cláusulas es una línea.

¿Hay una lista de más en alguna parte?Gracias.

Answer 1

De La complejidad de los problemas de satisfacción por Schaefer:

Demostramos que (asumiendo P!= NP) SAT (S) es decidible en tiempo polinomial solo si se cumple al menos una de las siguientes condiciones:

(a) Toda relación en S se satisface cuando todas las variables son 0.

(b) Toda relación en S se satisface cuando todas las variables son 1.

(c) Cada relación en S se puede definir mediante una fórmula CNF en la que cada conjunción tiene como máximo una variable negada.

(d) Cada relación en S se puede definir mediante una fórmula CNF en la que cada conjunción tiene como máximo una variable innecesaria.

(e) Cada relación en S se puede definir mediante una fórmula CNF que tiene como máximo 2 literales en cada conjunción.

(f) Toda relación en S es el conjunto de soluciones de un sistema de ecuación lineal sobre el campo de dos elementos {0,1}.

Los dos primeros tienen solución O (1), los tres siguientes O (n) y el último O (n ^ 3) (creo). Entonces, las instancias SAT que desea están en una de las primeras cinco clases.