Dlaczego CNF jest używany do SAT, a nie DNF?

Nie do końca rozumiem, dlaczego prawie wszystkie solwery SAT używają CNF zamiast DNF. Wydaje mi się, że rozwiązywanie SAT jest łatwiejsze przy użyciu DNF. W końcu musisz tylko przejrzeć zestaw implantów i sprawdzić, czy jeden z nich nie zawiera zarówno zmiennej, jak i jej negacji. W przypadku CNF nie ma takiej prostej procedury.

Zmniejszenie Podręcznik, SAT do 3SAT z powodu Karp, przekształca dowolnego logiczna wzorze w o „równoważny” CNF logiczna wzorze cp ' wielomianowej wielkości tak, że Φ jest spe wtedy i tylko wtedy, gdy Φ ' jest spe. (Ściśle mówiąc, te dwie formuły nie są równoważne, ponieważ Φ ′ ma dodatkowe zmienne, ale wartość Φ ′ w rzeczywistości nie zależy od tych nowych zmiennych.)$\Phi$$\Phi'$ $\Phi$$\Phi'$$\Phi'$$\Phi'$

Nie jest znane podobne zmniejszenie z dowolnych wzorów boolowskich do wzorów DNF; wszystkie znane transformacje wykładniczo zwiększają rozmiar formuły. Ponadto, chyba że P = NP, taka redukcja nie jest możliwa!

Mówiono o większości ważnych rzeczy, ale chciałbym podkreślić kilka kwestii.

1. Zgodność formuły DNF wynosi P
2. Zgodność formuły CNF wynosi NP
3. testowanie, czy formuła CNF jest tautologią, to P
4. testowanie, czy formuła DNF jest tautologią, jest koNP
5. negowanie DNF daje CNF i odwrotnie

Tak więc solwery SAT używają CNF, ponieważ są ukierunkowane na satysfakcję, a dowolną formułę można przełożyć na CNF, zachowując zadowalalność w czasie liniowym.

Solwery SAT nie „używają” CNF - otrzymują (często) CNF jako dane wejściowe i starają się rozwiązać otrzymany CNF. Jak wskazuje twoje pytanie, reprezentacja jest wszystkim - o wiele łatwiej jest stwierdzić, czy DNF jest satysfakcjonujący niż CNF tej samej wielkości.

Prowadzi to do pytania, dlaczego solwery SAT nie mogą tak po prostu zamienić ich CNF w DNF i rozwiązać wynikowy DNF, a próba wykonania tego jest dobrym ćwiczeniem do zrozumienia zagadnień reprezentacji.

7 ^th września 2013: Dalsza odpowiedź dodał dolny sprawdzenie stronie

---

Zasadniczo wzór DNF jest rozłączeniem zdań , gdzie każda klauzula c i = l i , 1 ∧ . . . ∧ l i , k to połączenie literałów. Nazwijmy klauzulę c $c_1 \lor ... \lor c_m$$c_i = l_{i,1} \land ... \land l_{i,k}$$c_i$ sprzeczne wtedy i tylko wtedy, gdy zawiera zarówno dosłowne i jego negacji ¬ l . Łatwo zauważyć, że każda klauzula nie powodująca konfliktu po prostu koduje 2 n - $l$$\lnot l$$2^{n-k}$rozwiązania formuły. Cały DNF jest więc tylko wyliczeniem rozwiązań. Formuła może mieć wykładniczo wiele rozwiązań, więc odpowiadająca jej formuła DNF może mieć wykładniczo wiele klauzul. Spróbuj przekonwertować tę formułę 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}$

do odpowiadającej jej formuły DNF: otrzymasz za dużo klauzul. Jednym słowem: CNF jest zwarty, a DNF nie; CNF jest niejawny, a DNF jest jawny.

Następujący problem jest NP-zupełny: biorąc pod uwagę instancję DNF, czy istnieje przypisanie zmiennych, które fałszują wszystkie klauzule?

Właśnie zrozumiałem jeszcze jedną rzecz, która, mam nadzieję, zasługuje na osobną odpowiedź. Domniemanie pytania nie jest do końca prawdziwe. Binarny schemat decyzyjny (BDD) może być postrzegany jako zwarta / udoskonalona reprezentacja DNF. Było kilka solverów SAT korzystających z BDD, ale wierzę, że już się nie pojawiają.

Jest ładny papier autorstwa Darwiche i Markiza badający różne właściwości różnych reprezentacji funkcji boolowskich.

Ta dalsza odpowiedź ma stanowić informację zwrotną do komentarza dividebyzero do mojej poprzedniej odpowiedzi.

Jak mówi dividebyzero, z pewnością prawdą jest, że CNF i DNF są dwiema stronami tej samej monety.

Kiedy musisz znaleźć satysfakcjonujące zadanie, DNF jest jawne, ponieważ w sposób oczywisty pokazuje ci swoje zadowalające zadania (satysfakcja DNF należy do ), podczas gdy CNF jest niejawna, ponieważ owija się i zwija, aby ukryć swoje zadowalające zadania przed twoimi oczami (satysfakcja CNF wynosi N P - c o m p l e t e ). Nie znamy żadnej procedury, która byłaby w stanie rozpakować i rozwinąć dowolną formułę CNF w jakąś równoważną formułę DNF, która nie ma wykładniczego rozmiaru. To był punkt mojej poprzedniej odpowiedzi (której przykład miał na celu pokazanie gwałtownego wybuchu, chociaż wprawdzie taki przykład nie był najlepszym możliwym wyborem).$\mathbf{P}$$\mathbf{NP-complete}$

$\mathbf{P}$$\mathbf{NP-complete}$ ). Nie znamy żadnej procedury, która byłaby w stanie rozpakować i rozwinąć dowolną formułę DNF w jakąś równoważną formułę CNF, która nie ma wykładniczego rozmiaru.

Na jednym krańcu mamy sprzeczności, tj. Niezadowalające formuły. Na przeciwległym krańcu mamy Tautologie, czyli formuły niefalsyfikowalne. W środku mamy formuły, które są zarówno satysfakcjonujące, jak i falsyfikowalne.

$n$$k$$2^{n-k}$ przypisań fałszujących.

$n$$k$$2^{n-k}$ spełniających przypisania.

Formuła CNF bez klauzul jest tautologią, ponieważ nie ma żadnego przypisania fałszującego. Formuła CNF zawierająca pustą klauzulę (która obejmuje każdą inną klauzulę) jest sprzecznością, ponieważ pusta klauzula (która ma$k = 0$) wskazuje, że wszystkie $2^n$zadania są sfałszowane. Każda inna formuła CNF jest Sprzecznością lub jedną z tych formuł w środku (i tak jest$\mathbf{NP-complete}$ to distinguish between these 2 cases).

A DNF formula without terms is a Contradiction, because it does not have any satisfying assignment. A DNF formula containing the empty term (which subsumes every other term) is a Tautology, because the empty term (which has $k = 0$) indicates that all the $2^n$ assignments are satisfying. Any other DNF formula is either a Tautology or one of those formulas in the middle (and it is $\mathbf{NP-complete}$ to distinguish between these 2 cases).

With a CNF formula, distinguishing between the 2 cases above means being able to tell whether all the falsifying assignments collectively brought by the presence of clauses overlap in such a way to cover all the $2^n$ assignments (in which case the formula is a Contradiction, otherwise it is satisfiable).

With a DNF formula, distinguishing between the 2 cases above means being able to tell whether all the satisfying assignments collectively brought by the presence of terms overlap in such a way to cover all the $2^n$ assignments (in which case the formula is a Tautology, otherwise it is falsifiable).

W tym świetle staje się jasne, dlaczego satysfakcjonowanie CNF i falsyfikowalność DNF są równoważne pod względem twardości obliczeniowej. Ponieważ w rzeczywistości stanowią one ten sam problem, ponieważ podstawowe zadanie jest dokładnie takie samo: powiedzieć, czy połączenie kilku zbiorów jest równe przestrzeni wszystkich możliwości . Takie zadanie prowadzi nas do szerszego królestwa liczenia, które moim skromnym zdaniem jest jedną z tych możliwości, które należy żarliwie zbadać, aby mieć nadzieję na dokonanie pewnego niemałego postępu w zakresie tych problemów (wątpię, aby dalsze badania nad rozwiązaniami opartymi na rozdzielczości może w końcu przynieść przełomowe osiągnięcia teoretyczne, podczas gdy z pewnością nadal przynosi zaskakujące postępy praktyczne).

Trudność takiego zadania polega na tym, że zestawy te nakładają się dziko, w sposób włączający - wyłączający.

The presence of such overlapping is precisely where the hardness of counting resides. Moreover, the fact that we let those sets overlap is the very reason that allows us to have compact formulas whose solution space is nevertheless exponentially large.

Postanowiłem zamienić wszystkie te odpowiedzi w tym wątku (zwłaszcza odpowiedź Giorgio Camerani) w ładny stół, aby dualność była widoczna na pierwszy rzut oka:

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

$(*)$: These search problems, as well as DNF to CNF conversion (or vice versa for that matter), require exponential time due to the sheer size of the output. They are in FPSPACE; in fact, they are solvable by a function with a polynomial-time bit-graph, which is as efficient as it gets for an exponential-size-output function, but I’m not aware of this class having a name. Usual notions of poly-time reductions only work sensibly for functions with polynomial-size output; applying them blindly to the present case would make all these search problems FEXP-complete, again due to the size of the output.

$(**)$: These search problems are solvable by an exponential-time function with a polynomial-time bit-graph as in $(*)$. However, they are also solvable in $\mathrm{FP}^{\mathrm{NP}[1]}$, and conversely, they are NP-hard under poly-time Turing reductions (many-one reductions make no sense here, as we are comparing a search problem with a decision problem).

Shortest answer to the question: showing satisfiability (solving SAT) via DNF can only be done in exponential time according to the table above.