Mengapa CNF digunakan untuk SAT dan bukan DNF?

Saya tidak begitu mengerti mengapa hampir semua pemecah SAT menggunakan CNF, bukan DNF. Menurut saya menyelesaikan SAT lebih mudah menggunakan DNF. Setelah semua, Anda hanya perlu memindai set implan dan memeriksa apakah salah satu dari mereka tidak mengandung variabel dan negasi. Untuk CNF, tidak ada prosedur sederhana seperti ini.

Pengurangan buku teks dari SAT ke 3SAT, karena Karp, mengubah rumus boolean sewenang-wenang menjadi formula boolean CNF ekuivalen " dari ukuran polinomial , sehingga memuaskan jika dan hanya jika memuaskan. (Sebenarnya, kedua formula ini tidak setara, karena memiliki variabel tambahan, tetapi nilai sebenarnya tidak tergantung pada variabel-variabel baru itu.)Φ ′ Φ Φ ′ Φ ′ Φ $\Phi$$\Phi'$ $\Phi$$\Phi'$$\Phi'$$\Phi'$

Tidak ada pengurangan serupa dari formula boolean yang berubah-ubah menjadi formula DNF yang diketahui; semua transformasi yang diketahui meningkatkan ukuran rumus secara eksponensial. Selain itu, kecuali P = NP, tidak ada pengurangan seperti itu!

Sebagian besar hal-hal penting dikatakan tetapi saya ingin menekankan beberapa poin.

1. kepuasan formula DNF adalah P
2. kepuasan formula CNF adalah NP
3. menguji apakah rumus CNF adalah tautologi adalah P
4. menguji apakah formula DNF adalah tautologi adalah CoNP
5. meniadakan hasil DNF CNF dan sebaliknya

Jadi pemecah SAT menggunakan CNF karena mereka menargetkan kepuasan dan formula apa pun dapat diterjemahkan ke CNF sambil mempertahankan kepuasan dalam waktu linier.

Pemecah SAT tidak "menggunakan" CNF - mereka (sering) diberi CNF sebagai input dan melakukan yang terbaik untuk menyelesaikan CNF yang diberikan. Seperti yang ditunjukkan oleh pertanyaan Anda, representasi adalah segalanya - jauh lebih mudah untuk mengatakan apakah DNF lebih memuaskan daripada CNF dengan ukuran yang sama.

Ini mengarah pada pertanyaan mengapa pemecah SAT tidak bisa hanya mengubah CNF yang diberikan menjadi DNF dan memecahkan DNF yang dihasilkan, dan mencoba ini adalah latihan yang baik untuk dilakukan dalam memahami masalah representasi.

7 ^th September 2013: jawaban lebih lanjut menambahkan, cek bagian bawah halaman

---

$c_1 \lor ... \lor c_m$$c_i = l_{i,1} \land ... \land l_{i,k}$$c_i$$l$$\lnot l$$2^{n-k}$solusi formula. Jadi keseluruhan DNF hanyalah sebuah enumerasi solusi. Rumus mungkin memiliki banyak solusi secara eksponensial, sehingga rumus DNF yang sesuai mungkin memiliki banyak klausa secara eksponensial. Coba konversi rumus CNF ini:

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

ke rumus DNF yang sesuai: Anda akan mendapatkan terlalu banyak klausa. Dalam satu kata: CNF kompak, sedangkan DNF tidak; CNF tersirat, sedangkan DNF eksplisit.

Masalah berikut adalah NP-complete: diberikan contoh DNF, apakah ada penugasan variabel yang memalsukan semua klausa?

Saya baru menyadari satu hal lagi, yang semoga layak mendapat jawaban terpisah. Anggapan pertanyaan itu tidak sepenuhnya benar. Diagram keputusan biner (BDD) dapat dilihat sebagai representasi DNF yang ringkas / halus. Ada beberapa pemecah SAT yang menggunakan BDD tetapi saya yakin mereka tidak lagi muncul.

Ada sebuah makalah yang bagus dari Darwiche dan Marquis yang mempelajari sifat-sifat berbeda dari berbagai representasi fungsi Boolean.

Jawaban lebih lanjut ini dimaksudkan sebagai umpan balik untuk membagi komentar nol dengan jawaban saya sebelumnya.

Seperti yang dikatakan dividebyzero, memang benar bahwa CNF dan DNF adalah dua sisi dari koin yang sama.

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

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

Pada satu ekstremitas kita memiliki Kontradiksi, yaitu formula yang tidak memuaskan. Pada ekstremitas yang berlawanan kita memiliki Tautologi, yaitu formula yang tidak dapat dibenarkan. Di tengah, kami memiliki formula yang memuaskan dan bisa dipalsukan.

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

Di bawah cahaya ini menjadi lebih jelas mengapa Kepuasan CNF dan DNF Falsifiability setara dalam hal kekerasan komputasi. Karena mereka sebenarnya adalah masalah yang sama, karena tugas yang mendasarinya persis sama: untuk mengetahui apakah penyatuan beberapa set sama dengan ruang semua kemungkinan . Tugas semacam itu membawa kita ke ranah penghitungan yang lebih luas, yang menurut pendapat saya sederhana salah satu jalan yang harus dieksplorasi dengan sungguh-sungguh untuk berharap dapat membuat beberapa kemajuan yang tidak dapat diabaikan pada masalah-masalah ini (saya ragu bahwa penelitian lebih lanjut tentang pemecah berbasis resolusi pada akhirnya dapat membawa kemajuan teoretis yang inovatif, sementara itu tentu saja terus membawa kemajuan praktis yang mengejutkan).

Kesulitan dari tugas tersebut adalah bahwa set tersebut tumpang tindih secara liar, dengan cara inklusi - eksklusi.

Kehadiran yang tumpang tindih seperti itulah tepatnya di mana kekerasan berhitung berada. Selain itu, fakta bahwa kita membiarkan set tersebut tumpang tindih adalah alasan yang memungkinkan kita untuk memiliki formula ringkas yang ruang solusinya tetap besar secara eksponensial.

Saya telah memutuskan untuk mengubah semua jawaban ini di utas ini (terutama jawaban Giorgio Camerani) menjadi tabel yang bagus sehingga dualitas dapat dilihat dalam satu pandangan:

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

Jawaban terpendek untuk pertanyaan: menunjukkan kepuasan (penyelesaian SAT) melalui DNF hanya dapat dilakukan dalam waktu eksponensial sesuai dengan tabel di atas.