¿Por qué se usa CNF para SAT y no DNF?

No entiendo por qué casi todos los solucionadores de SAT usan CNF en lugar de DNF. Me parece que resolver SAT es más fácil usando DNF. Después de todo, solo tiene que explorar el conjunto de implicantes y verificar si uno de ellos no contiene tanto una variable como su negación. Para CNF, no existe un procedimiento simple como este.

La reducción del libro de texto de SAT a 3SAT, debido a Karp, transforma una fórmula booleana arbitraria en una fórmula booleana "equivalente" CNF Φ ' de tamaño polinómico , de modo que Φ es satisfactoria si y solo si Φ ′ es satisfactoria. (Estrictamente hablando, estas dos fórmulas no son equivalentes, porque Φ ′ tiene variables adicionales, pero el valor de Φ ′ en realidad no depende de esas nuevas variables).$\Phi$$\Phi'$ $\Phi$$\Phi'$$\Phi'$$\Phi'$

No se conoce una reducción similar de fórmulas booleanas arbitrarias a fórmulas DNF; Todas las transformaciones conocidas aumentan el tamaño de la fórmula exponencialmente. Además, a menos que P = NP, ¡no es posible tal reducción!

Se dijeron la mayoría de las cosas importantes, pero me gustaría enfatizar algunos puntos.

1. La satisfacción de una fórmula de DNF es P
2. La satisfacción de una fórmula CNF es NP
3. probar si una fórmula CNF es una tautología es P
4. probar si una fórmula de DNF es una tautología es coNP
5. negar el DNF produce CNF y viceversa

Por lo tanto, los solucionadores SAT usan CNF porque apuntan a la satisfacción y cualquier fórmula puede traducirse a un CNF mientras se conserva la satisfacción en el tiempo lineal.

Los solucionadores de SAT no "usan" el CNF: a menudo reciben CNF como entradas y hacen todo lo posible para resolver el CNF que reciben. Como su pregunta señala, la representación lo es todo: es mucho más fácil saber si una DNF es satisfactoria que una CNF del mismo tamaño.

Esto lleva a la pregunta de por qué los solucionadores de SAT no pueden simplemente convertir su CNF dado en un DNF y resolver el DNF resultante, e intentar este es un buen ejercicio para comprender los problemas de representación.

7 ^º de septiembre de 2013: Además añadió respuesta, verificación final de la página

---

Básicamente, una fórmula de DNF es una disyunción de las cláusulas , donde cada cláusula c i = l i , 1 ∧ . . . ∧ l i , k es una conjunción de literales. Llamemos a una cláusula c i conflictiva si y solo si contiene tanto un literal l como su negación ¬ l . Es fácil ver que cada cláusula no conflictiva solo codifica 2 n - $c_1 \lor ... \lor c_m$$c_i = l_{i,1} \land ... \land l_{i,k}$$c_i$$l$$\lnot l$$2^{n-k}$soluciones de la fórmula. Entonces, todo el DNF es solo una enumeración de soluciones. Una fórmula puede tener exponencialmente muchas soluciones, por lo que la fórmula DNF correspondiente puede tener exponencialmente muchas cláusulas. Intenta convertir esta fórmula CNF:

$l_1 \lor l_2 \lor l_3 \lor l_4$

$l_5 \lor l_6 \lor l_7 \lor l_8$

$l_9 \lor l_{10} \lor l_{11} \lor l_{12}$

$l_{13} \lor l_{14} \lor l_{15} \lor l_{16}$

$l_{17} \lor l_{18} \lor l_{19} \lor l_{20}$

a su fórmula DNF correspondiente: obtendrá demasiadas cláusulas. En una palabra: CNF es compacto, mientras que DNF no lo es; CNF es implícito, mientras que DNF es explícito.

El siguiente problema es NP-complete: dada una instancia de DNF, ¿hay una asignación de variables que falsifique todas las cláusulas?

Me acabo de dar cuenta de una cosa más, que con suerte merece una respuesta por separado. La presunción de la pregunta no es del todo cierto. Un diagrama de decisión binario (BDD) podría verse como una representación compacta / refinada de DNF. Ha habido algunos solucionadores de SAT que usan BDD, pero creo que ya no aparecen.

Hay un bonito artículo de Darwiche y Marquis que estudia diferentes propiedades de varias representaciones de funciones booleanas.

Esta respuesta adicional se entiende como una retroalimentación al comentario de dividebyzero a mi respuesta anterior.

Como dice dividebyzero, es cierto que CNF y DNF son dos caras de la misma moneda.

$\mathbf{P}$$\mathbf{NP-complete}$

$\mathbf{P}$$\mathbf{NP-complete}$

En un extremo tenemos contradicciones, es decir, fórmulas insatisfactorias. En el extremo opuesto tenemos Tautologías, es decir, fórmulas imposibles de verificar. En el medio, tenemos fórmulas que son tanto satisfactorias como falsificables.

$n$$k$$2^{n-k}$

$n$$k$$2^{n-k}$

$k = 0$$2^n$$\mathbf{NP-complete}$

$k = 0$$2^n$$\mathbf{NP-complete}$

$2^n$

$2^n$

Bajo esta luz, queda más claro por qué la Satisfabilidad CNF y la Falsificabilidad DNF son equivalentes en términos de dureza computacional. Porque en realidad son el mismo problema, ya que la tarea subyacente es exactamente la misma: saber si la unión de varios conjuntos es igual al espacio de todas las posibilidades . Dicha tarea nos lleva al ámbito más amplio de contar, que es, en mi humilde opinión, una de esas vías a explorar fervientemente para tener la esperanza de lograr un progreso no despreciable en estos problemas (dudo que se realicen más investigaciones sobre solucionadores basados ​​en resolución eventualmente puede traer avances teóricos innovadores, mientras que ciertamente continúa trayendo avances prácticos sorprendentes).

La dificultad de tal tarea es que esos conjuntos se superponen enormemente, en una forma de inclusión - exclusión.

La presencia de tal superposición es precisamente donde reside la dureza de contar. Además, el hecho de que dejemos que esos conjuntos se superpongan es la razón que nos permite tener fórmulas compactas cuyo espacio de solución es, sin embargo, exponencialmente grande.

He decidido convertir todas estas respuestas en este hilo (especialmente la respuesta de Giorgio Camerani) en una buena tabla para que la dualidad sea visible de un solo vistazo:

$$\begin{array} {r|c|c} &\text{DNF} & \text{CNF} \\\hline \text{tautology/unfalsifiability} & \textsf{coNP-complete} & \textsf{P} \; \tiny\text{(each clause has a pair of P and ¬P)} \\\hline \text{satisfiability} & \textsf{P} \; \tiny\text{(sat. assignments are explicit)} & \textsf{NP-complete}\\\hline \text{falsifiability} & \textsf{NP-complete} & \textsf{P} \; \tiny\text{(fals. assignments are explicit)} \\\hline \text{unsatisfiability} & \textsf{P} \; \tiny\text{(each clause has a pair of P and ¬P)} & \textsf{coNP-complete} \\\hline \tiny{\text{conversion to normal form, retaining equivalence}} & (*) & (*) \\\hline \tiny{\text{conversion to normal form, retaining satisfiability}} & (**) & \textsf{FP} \\\hline \tiny{\text{conversion to normal form, retaining falsiability}} & \textsf{FP} & (**) \end{array}$$

$(*)$

$(**)$$(*)$$\mathrm{FP}^{\mathrm{NP}[1]}$

La respuesta más corta a la pregunta: mostrar satisfacción (resolver SAT) a través de DNF solo se puede hacer en tiempo exponencial de acuerdo con la tabla anterior.