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

22

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.

Kaveh
źródło
5
Nie wszystkie solwery ograniczeń używają CNF jako danych wejściowych. Niektórzy wolą tego nie robić, ponieważ struktura oryginalnego zestawu ograniczeń jest zachowana.
Dave Clarke,
1
to pytanie ma błędną przesłankę i nie sądzę, że zasługuje na tak wysoką ocenę, jak obecnie wyrażane. SAT jest zdefiniowane jako rozwiązanie wzorów CNF. istnieje problem z rozwiązywaniem DNF (możesz nawet nazwać to znalezieniem satysfakcjonujących zadań), ale nie jest nazywany / nazywany SAT w CS. i imho należy to przenieść do cs.se ... kolejna uwaga - konwersja CNF do DNF i odwrotnie jest w rzeczywistości bardzo podobna do algorytmu kompresji lub może być postrzegana jako algorytm kompresji, który zawiedzie w określonych przypadkach (prowadząc do gwałtownego wybuchu w rozmiarze)
dniu
10
@vzn: właściwie „SAT” jest czasem używany w odniesieniu do problemu znalezienia zadowalającego przypisania dla dowolnej formuły boolowskiej. CNF-SAT jest tylko najciekawszym przypadkiem specjalnym, dlatego używamy „SAT” w odniesieniu do CNF-SAT w szczególności jako swego rodzaju synchdoche. Oczywiście DNF-SAT można skutecznie rozwiązać, podobnie jak CNF-TAUTOLOGY można skutecznie rozwiązać. Wydaje się, że pytanie opiera się na niezrozumieniu tego.
Niel de Beaudrap,

Odpowiedzi:

56

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!

Jeffε
źródło
afaik konwersja DNF do CNF i vice versa nie jest dokładnie taka sama jak P w porównaniu z NP, chociaż prawdopodobnie dotyczy pewnych ważnych separacji klas złożoności (najwyraźniej dla klas „większych” niż NP) ... problem polega na tym, że może to prowadzić do gwałtowny wzrost wielkości ... a w każdym razie konwersja między CNF a DNF nie stanowi problemu decyzyjnego ... istnieje wiele sposobów, aby przekształcić go w problem decyzyjny ...
vzn
10
Myślę, że JeffE miał na myśli to, że DNF-SAT jest w P, więc nie może być NP-kompletny, chyba że P = NP.
Luke Mathieson
2
„wszystkie znane transformacje” nie są poprawne, biorąc pod uwagę obecną wiedzę, ponieważ istnieją formuły / konwersje DNF <=> CNF, które prawdopodobnie wymagają wykładniczego powiększenia przestrzeni bez względu na algorytm ... chyba wydawało się, że dyskusja o konwersji CNF <=> konwersja DNF była bardzo istotna na to pytanie i ta odpowiedź na nie wskazuje ... czy skrót „DNF-SAT” jest używany w literaturze? nie przypominam sobie, że widziałem to sam ... wydaje mi się to mylące z natury ... Zadawanie DNF jest problemem decyzyjnym, konwersja DNF <-> CNF jest problemem funkcji, a odpowiedź nie czyni tego rozróżnienia zbyt jasnym; świetna odpowiedź by ...
dniu
@ Jɛ ff E: czy masz coś przeciwko wyjaśnieniu, co rozumiesz przez „arbitralną formułę logiczną”? Patrząc na artykuł Karpa , strona 92, ZADOWOLENIE określa się we wzorach CNF. Nie wpływa to na twoją odpowiedź na pytanie PO, ale staram się upewnić, że nie ma już ogólnych wyników dla dowolnych formuł boolowskich (tj. Formuł, które niekoniecznie są w CNF). Dzięki
lyes,
22

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.

Mikolas
źródło
1
@TayfunPay robią. Na przykład . Jeśli dwa razy nie zezwalasz na klauzule zawierające tę samą zmienną, wówczas istnieje jedna reprezentacja tautologii, czyli pusty zestaw klauzul. {{¬xx}}
Mikolas
3
@Tayfun, chociaż zgadzam się, że definicje zwykle nie pozwalają na powtarzanie zmiennych w klauzulach, nie sądzę, żebym kiedykolwiek widział definicję, która uniemożliwiałaby pusty zestaw klauzul. (I nie jest dla mnie jasne, dlaczego miałbyś to zrobić)
Mikolas
2
@Tayfun 1) czy mógłbyś wskazać mi publikację, która mówi, że w CNF nie ma tautologii lub że pusty zestaw klauzul nie jest CNF? 2) jeśli zabronisz pustego zestawu klauzul, powinieneś również zabronić pustej klauzuli i nie możesz również reprezentować fałszu 3) jeśli nie zezwolisz na true i / lub false w CNF, tracisz właściwość możliwości reprezentowania wszystkie funkcje boolowskie, dlaczego chcesz to zrobić?
Mikolas
1
„w żadnej klauzuli nie powinno się powtarzać zmiennych ani literałów”. --- to nie wyklucza pustych wzorów lub klauzul. BTW Jeśli nie zgadzasz się z pustą klauzulą, nie możesz już robić dowodów odrzucenia rozdzielczości, które stanowią dość ważną część automatycznego rozumowania.
Mikolas
18

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.

Lew Reyzin
źródło
11

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...cmci=li,1...li,kci 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¬l2nkrozwią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:

l1l2l3l4

l5l6l7l8

l9l10l11l12

l13l14l15l16

l17l18l19l20

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?

Giorgio Camerani
źródło
4
Aby uzyskać poprawne formatowanie LaTeX, zamień \ i i \ lub na \ land i \ lor (lub \ wedge i \ vee).
Jeffε
2
Nie ma nic bardziej zwartego w transformacji do zwykłej CNF, prawdziwym kluczem do pytania PO jest fakt, że można tworzyć te „równoważne” funkcje CNF ze zmiennymi pomocniczymi. Prawdopodobnie istnieje podobne przybliżenie, które można zrobić z DNF, aby rozwiązać inny problem zamiast testować pod kątem satysfakcji. (funkcje
równorzędności
1
Ten wgląd Giorgio Camerani nie jest dobry. Ten sam wykładniczy wzrost liczby klauzul może wystąpić, jeśli przekształcisz coś w CNF. Wybierz ten sam przykład i zamień „i” na „lub” s. Konwersja tego małego wyrażenia DNF do CNF będzie ogromna tak samo. Mają z nimi trochę związek ying-and-yang.
dividebyzero
@dividebyzero: Osobną odpowiedź poświęciłem, aby odpowiedzieć na twoje komentarze.
Giorgio Camerani,
6

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.

Mikolas
źródło
4

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).PNPcomplete

PNPcomplete ). 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.

nk2nk przypisań fałszujących.

nk2nk 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 mak=0) wskazuje, że wszystkie 2)nzadania są sfałszowane. Każda inna formuła CNF jest Sprzecznością lub jedną z tych formuł w środku (i tak jestNPcomplete 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 2n assignments are satisfying. Any other DNF formula is either a Tautology or one of those formulas in the middle (and it is NPcomplete 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 2n 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 2n 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.

Giorgio Camerani
źródło
4

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:

DNFCNFtautologia / niefalsyfikowalnośćcoNP-completeP.(każda klauzula ma parę P i ¬P)satysfakcjaP.(sat. zadania są jawne)NP-completefalsyfikowalnośćNP-completeP.(fals. przypisania są jawne)niezadowolenieP.(każda klauzula ma parę P i ¬P)coNP-completekonwersja do postaci normalnej, zachowując równoważność()()konwersja do postaci normalnej, zachowująca zadowalalność()FPkonwersja do postaci normalnej, z zachowaniem falsyfikacjiFP()

(): 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 FPNP[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.

mcb
źródło
1
What is a "PL formula" and what does "NF" mean?
Joshua Grochow
4
There are a few issues here. (1) I think by "unfalsifiability" you mean "tautology". (2) KNF should be CNF.
Huck Bennett
2
Still not clear what you mean by "NF (retain satisfiability)". Does that mean an algorithm A such that A(φ) is satisfiable if φ is, but if φ is unsatisfiable then A(φ) can be either, and furthermore for all satisfiable formulae φ, A(φ) has the same output? That's what I would think from your notation, but this problem wouldn't be in P for CNFs. So what do you mean?
Joshua Grochow
1
(1) "predicate logic" should be "propositional logic". (2) The conversions to normal forms are not decision problems, but function problems (or rather, search problems, as the "normal forms" are not unique). So, the decision classes given in the table are inappropriate.
Emil Jeřábek supports Monica
1
What is the Δ3P doing there?
Emil Jeřábek supports Monica