Di sini tujuannya adalah untuk mengurangi masalah SAT sewenang-wenang menjadi 3-SAT dalam waktu polinomial menggunakan klausa dan variabel paling sedikit. Pertanyaan saya dimotivasi oleh rasa ingin tahu. Secara kurang formal, saya ingin tahu: "Apa pengurangan 'paling alami' dari SAT menjadi 3-SAT?"
Sekarang pengurangan yang selalu saya lihat di buku teks kira-kira begini:
Pertama-tama ambil contoh SAT Anda dan terapkan teorema Cook-Levin untuk menguranginya ke sirkuit SAT.
Kemudian Anda menyelesaikan pekerjaan dengan pengurangan standar sirkuit SAT menjadi 3-SAT dengan mengganti gerbang dengan klausa.
Sementara ini bekerja, klausa 3-SAT yang dihasilkan akhirnya tampak hampir tidak seperti klausa SAT yang Anda mulai, karena aplikasi awal teorema Cook-Levin.
Adakah yang bisa melihat bagaimana melakukan reduksi secara lebih langsung, melewatkan langkah rangkaian lanjutan dan langsung menuju 3-SAT? Saya bahkan akan senang dengan pengurangan langsung dalam kasus khusus n-SAT.
(Saya kira ada beberapa trade-off antara waktu komputasi dan ukuran output. Jelas merosot - walaupun untungnya tidak dapat diterima kecuali P = NP - solusi akan hanya menyelesaikan masalah SAT, kemudian memancarkan sepele 3 Contoh -SAT ...)
EDIT: Berdasarkan jawaban ratchet jelas sekarang bahwa pengurangan ke n-SAT agak sepele (dan bahwa saya benar-benar harus memikirkan satu melalui sedikit lebih hati-hati sebelum memposting). Saya membiarkan pertanyaan ini terbuka sedikit jika seseorang mengetahui jawaban untuk situasi yang lebih umum, jika tidak saya hanya akan menerima jawaban ratchet.
sumber
Jawaban:
Setiap klausa SAT memiliki 1, 2, 3 atau lebih variabel. Klausa 3 variabel dapat disalin tanpa masalah
Klausa variabel 1 dan 2
{a1}
dan{a1,a2}
dapat diperluas ke{a1,a1,a1}
dan{a1,a2,a1}
masing masing.Klausa dengan lebih dari 3 variabel
{a1,a2,a3,a4,a5}
dapat diperluas{a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5}
dengans1
dans2
variabel baru yang nilainya akan bergantung pada variabel mana dalam klausa asli yang benarsumber
sumber
Jika Anda membutuhkan pengurangan dari k-SAT ke 3-SAT, maka jawaban ratchet berfungsi dengan baik.
Jika Anda ingin pengurangan langsung dari formula proposisional generik ke CNF (dan menjadi 3-SAT), maka - setidaknya dari "perspektif pemecah SAT" - Saya pikir jawaban untuk pertanyaan Anda Apa pengurangan 'paling alami' ... ? , adalah: Tidak ada pengurangan 'alami' !
Dari kesimpulan Bab 2 - "Penyandian CNF" dari buku (sangat bagus): Buku Pegangan Kepuasan :
...
Biasanya ada banyak cara untuk memodelkan masalah yang diberikan di CNF, dan beberapa pedoman diketahui memilih di antara mereka. Seringkali ada pilihan fitur masalah untuk dimodelkan sebagai variabel, dan beberapa mungkin perlu dipertimbangkan untuk menemukannya. Pengkodean tseitin bersifat kompak dan mekanis tetapi dalam praktiknya tidak selalu mengarah pada model terbaik, dan beberapa subformula mungkin lebih diperluas. Beberapa klausa dapat dihilangkan dengan pertimbangan polaritas, dan tersirat, klausa yang melanggar simetri atau diblokir dapat ditambahkan. Pengkodean yang berbeda mungkin memiliki kelebihan dan kekurangan yang berbeda seperti ukuran atau kepadatan solusi, dan apa keuntungan untuk satu pemecah SAT mungkin menjadi kerugian bagi yang lain. Singkatnya, pemodelan CNF adalah seni dan kita harus sering melanjutkan dengan intuisi dan eksperimen.
...
Algoritma yang paling dikenal adalah Tseitin (G. Tseitin. Pada kompleksitas derivasi dalam kalkulus proposisional. Otomatisasi Penalaran: Makalah Klasik dalam Logika Komputasi, 2: 466-483, 1983. Springer-Verlag.)
Untuk pengantar pengkodean CNF yang bagus, baca buku yang disarankan Handbook o Satisfiability . Anda juga dapat membaca beberapa karya terbaru dan melihat referensi; sebagai contoh:
sumber
Izinkan saya memposting solusi lain yang mirip dengan Ratchel tetapi agak berbeda. Ini langsung diambil dari bab 9 Edisi 2 "The Algorithm Design Manual" oleh Steven Skiena
sumber