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.
ds.algorithms
sat
Kaveh
źródło
źródło
Odpowiedzi:
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.)Φ Φ′ Φ Φ′ Φ′ Φ′
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!
źródło
Mówiono o większości ważnych rzeczy, ale chciałbym podkreślić kilka kwestii.
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.
źródło
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.
źródło
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 ic1∨...∨cm ci=li,1∧...∧li,k ci 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 - kl ¬l 2n−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:
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?
źródło
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.
źródło
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).P NP−complete
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.
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 mak = 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 jestNP−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 hask=0 ) indicates that all the 2n assignments are satisfying. Any other DNF formula is either a Tautology or one of those formulas in the middle (and it is 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 the2n 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 the2n 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.
źródło
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:
Shortest answer to the question: showing satisfiability (solving SAT) via DNF can only be done in exponential time according to the table above.
źródło