Pourquoi CNF est-il utilisé pour SAT et non DNF?

Je ne comprends pas très bien pourquoi presque tous les solveurs SAT utilisent CNF au lieu de DNF. Il me semble que résoudre SAT est plus facile en utilisant DNF. Après tout, il vous suffit de parcourir l'ensemble des implicants et de vérifier si l'un d'eux ne contient pas à la fois une variable et sa négation. Pour CNF, il n'y a pas de procédure simple comme celle-ci.

La réduction des manuels de SAT à 3SAT, due à Karp, transforme une formule booléenne arbitraire en une formule booléenne CNF "équivalente" de taille polynomiale , de telle sorte que est satisfaisante si et seulement si est satisfaisante. (À strictement parler, ces deux formules ne sont pas équivalentes, car a des variables supplémentaires, mais la valeur de ne dépend pas réellement de ces nouvelles variables.)Φ $\Phi$$\Phi'$ Φ ′ Φ ′ Φ $\Phi$$\Phi'$$\Phi'$$\Phi'$

Aucune réduction similaire de formules booléennes arbitraires en formules DNF n'est connue; toutes les transformations connues augmentent de façon exponentielle la taille de la formule. De plus, à moins que P = NP, une telle réduction n'est pas possible!

La plupart des choses importantes ont été dites mais je voudrais souligner quelques points.

1. la satisfiabilité d'une formule DNF est P
2. la satisfiabilité d'une formule CNF est NP
3. tester si une formule CNF est une tautologie est P
4. tester si une formule DNF est une tautologie est coNP
5. la négation des rendements DNF CNF et vice versa

Les solveurs SAT utilisent donc CNF car ils visent la satisfiabilité et toute formule peut être traduite en CNF tout en préservant la satisfiabilité en temps linéaire.

Les solveurs SAT n'utilisent pas CNF - ils reçoivent (souvent) CNF en entrée et font de leur mieux pour résoudre le CNF qui leur est donné. Comme le souligne votre question, la représentation est tout - il est beaucoup plus facile de dire si un DNF est satisfaisable qu'un CNF de même taille.

Cela conduit à la question de savoir pourquoi les solveurs SAT ne peuvent pas simplement transformer leur CNF donné en DNF et résoudre le DNF résultant, et essayer c'est un bon exercice pour comprendre les problèmes de représentation.

7 ^e Septembre 2013: autre réponse a ajouté, en bas de la page de contrôle

---

Fondamentalement, une formule DNF est une disjonction des clauses , où chaque clause c i = l i , 1 ∧ . . . ∧ l i , k est une conjonction de littéraux. Appelons une clause c i conflictuelle si et seulement si elle contient à la fois un l littéral et sa négation ¬ l . Il est facile de voir que chaque clause non conflictuelle code juste 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}$solutions de la formule. Le DNF n'est donc qu'une énumération de solutions. Une formule peut avoir de manière exponentielle de nombreuses solutions, de sorte que la formule DNF correspondante peut avoir de manière exponentielle de nombreuses clauses. Essayez de convertir cette formule 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}$

à sa formule DNF correspondante: vous obtiendrez trop de clauses. En un mot: CNF est compact, tandis que DNF ne l'est pas; CNF est implicite, tandis que DNF est explicite.

Le problème suivant est NP-complet: étant donné une instance DNF, existe-t-il une affectation de variables qui falsifie toutes les clauses?

Je viens de réaliser une dernière chose, qui, espérons-le, mérite une réponse distincte. La présomption de la question n'est pas entièrement vraie. Un diagramme de décision binaire (BDD) pourrait être considéré comme une représentation compacte / raffinée de DNF. Il y a eu quelques solveurs SAT utilisant des BDD mais je pense qu'ils n'apparaissent plus.

Il y a un bel article de Darwiche et Marquis étudiant différentes propriétés de diverses représentations des fonctions booléennes.

Cette réponse supplémentaire est conçue comme une rétroaction au commentaire de dividebyzero sur ma réponse précédente.

Comme le dit dividebyzero, il est certainement vrai que CNF et DNF sont les deux faces d'une même médaille.

Lorsque vous devez trouver une affectation satisfaisante, DNF est explicite car il vous montre manifestement ses affectations satisfaisantes (la satisfaction DNF appartient à ), tandis que CNF est implicite car il s'enroule et se déroule pour cacher ses affectations satisfaisantes à vos yeux (la satisfaction CNF est N P - c o m p l e t e ). Nous ne connaissons aucune procédure capable de déballer et de dérouler une formule CNF en une formule DNF non satisfaisante qui n'est pas de taille exponentielle. C'était le point de ma réponse précédente (dont l'exemple était destiné à montrer l'explosion exponentielle, bien qu'il soit vrai que cet exemple n'était pas le meilleur choix possible).$\mathbf{P}$$\mathbf{NP-complete}$

Inversement, lorsque vous devez trouver une mission de falsification, CNF est explicite car il vous montre manifestement ses missions de falsification (CNF Falsifiability appartient à ), tandis que DNF est implicite car il s'enroule et s'enroule pour cacher ses missions de falsification de vos yeux (DNF Falsifiability est N P - c o m p l e t e ). Nous ne connaissons aucune procédure capable de déballer et de dérouler une formule DNF en une formule CNF équivalente qui n'est pas de taille exponentielle.$\mathbf{P}$$\mathbf{NP-complete}$

À une extrémité, nous avons des contradictions, c'est-à-dire des formules insatisfaisantes. À l'extrémité opposée, nous avons des tautologies, c'est-à-dire des formules infalsifiables. Au milieu, nous avons des formules à la fois satisfaisables et falsifiables.

$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$

Sous cet éclairage, il devient plus clair pourquoi la satisfaction CNF et la falsifiabilité DNF sont équivalentes en termes de dureté de calcul. Parce qu'ils sont en fait le même problème, car la tâche sous-jacente est exactement la même: dire si l'union de plusieurs ensembles est égale à l'espace de toutes les possibilités . Une telle tâche nous amène au domaine plus large du comptage, qui est à mon humble avis l'une de ces voies à explorer avec ferveur afin d'espérer faire des progrès non négligeables sur ces problèmes (je doute que de nouvelles recherches sur les résolveurs basés sur la résolution pourrait éventuellement apporter des avancées théoriques révolutionnaires, tout en continuant certainement à apporter des avancées pratiques surprenantes).

La difficulté d'une telle tâche est que ces ensembles se chevauchent énormément, d'une manière d'inclusion-exclusion.

La présence d'un tel chevauchement est précisément là où réside la dureté du comptage. De plus, le fait de laisser ces ensembles se chevaucher est la raison même qui nous permet d'avoir des formules compactes dont l'espace de solution est néanmoins exponentiellement grand.

J'ai décidé de transformer toutes ces réponses dans ce fil (en particulier la réponse de Giorgio Camerani) en un joli tableau pour que la dualité soit visible d'un seul coup d'œil:

$$\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]}$

Réponse la plus courte à la question: montrer la satisfiabilité (résoudre SAT) via DNF ne peut se faire qu'en temps exponentiel selon le tableau ci-dessus.