variasi SAT

Saya mencari di internet, tetapi saya tidak dapat menemukan 'daftar besar' varian masalah SAT.

Terlepas dari (umum)

• DUDUK,
• k-SAT,
• MAX-kSAT,
• Setengah SAT,
• XOR-SAT,
• NAE-SAT

varian apa lagi yang ada?

(juga akan sangat berguna jika ada kelas kompleksitas diberikan (jika memungkinkan))

(Membuat komentar sebagai jawaban seperti yang diminta dan sedikit berkembang.)

"Pikiran yang ingin tahu" harus membaca teorema dikotomi Schaefer dan generalisasi oleh Allender et al. yang menunjukkan bahwa setiap varian SAT yang mungkin adalah sepele atau di salah satu dari enam kelas kompleksitas yang terkenal:

1. NP-lengkap
2. P-lengkap
3. NL-lengkap
4. L-selesai
5. ⊕L-selesai
6. co-NLOGTIME

Daftar ini akan sangat panjang;) Berikut adalah beberapa varian SAT (NP-complete) favorit saya:

• PLANAR ( $\le 3, 3$ ) -SAT (setiap klausa berisi setidaknya dua dan paling banyak tiga literal, masing-masing variabel muncul tepat dalam tiga klausa; dua kali dalam bentuk yang tidak dinegasikan, dan satu kali dalam bentuk yang dinegasikan, dan satu kali dalam bentuk yang dinegasikan, dan grafik kejadian bipartit adalah planar.)

  Lihat: Dahlhaus, Johnson, Papadimitriou, Seymour, Yannakakis, Kompleksitas pemotongan multiterminal, Jurnal SIAM Komputasi 23 (1994) 864-894

• 4-BOUNDED PLANAR 3-CONNECTED 3SAT (setiap klausa berisi tepat 3 variabel berbeda, setiap variabel muncul di paling banyak 4 klausa, grafik insiden bipatite adalah planar dan 3-terhubung)

  Lihat: Kratochvíl, Masalah kepuasan planar khusus dan konsekuensi dari kelengkapan NP-nya, Discrete Applied Math. 52 (1994) 233-252

• MONOTONE CUBIC 1-IN-3SAT (MONOTONE-1-IN-3SAT di mana setiap variabel muncul tepat 3 kali)

  Lihat: Moore dan Robsen, Hard tilings masalah dengan ubin sederhana, Discrete Compute. Geom. 26 (2001) 573-590

• $k$$k$

  Lihat posting ini .

Pada "sisi NP-complete" saya menemukan varian-varian ini (saya juga mengajukan pertanyaan serupa pada cs.stackexchange):

• Planar 3-SAT;
• Planar 1-in-3 SAT dan Positif Planar 1-in-3 SAT (lihat Mulzer dan Rote );
• NAE 3-SAT;
• 2/2/4-SAT (lihat Menemukan solusi terpendek untuk ekstensi NxN dari 15-Puzzle tidak dapat dipecahkan oleh D. Ratner dan M. Warmuth (1986) );
• XSAT, NAE-SAT untuk Rumus Linear Monoton, XSAT untuk rumus linier yang tepat (lihat karya bagus Ewald Speckenmeyer tentang masalah XSAT linier: Kompleksitas Komputasi SAT, XSAT dan NAE-SAT untuk rumus CNF linear dan campuran );
• k-colourable Monotone NAE-3SAT (lihat P Jain, Tentang varian Monotone NAE-3SAT dan masalah Triangle-Free Cut, 2010 ).

$\mathrm{SAT}(k)$$\mathrm{SAT}$$k$$\mathrm{SAT}(2)$$\mathsf{L}$$\mathrm{SAT}(k)$$k\geq 3$

Terlepas dari daftar di atas, ada juga:

• #SAT: penghitungan model
• All-SAT: model enumerating

Ada hubungan yang sangat klasik antara logika dan aljabar, yang kembali ke asal logika modern dan karya George Boole. Rumus dalam logika proposisional dapat diartikan sebagai unsur aljabar Boolean. Konstanta logis benar dan salah menjadi konsep aljabar elemen atas dan bawah kisi. Operasi logis dari konjungsi, disjungsi, dan negasi akan menjadi operasi aljabar untuk bertemu, bergabung, dan saling melengkapi dalam aljabar Boolean. Koneksi ini kurang ditekankan dalam perawatan logika modern, tetapi ini sangat menarik dalam konteks pertanyaan Anda. Aljabar memungkinkan kita untuk menjauh dari banyak detail spesifik masalah dan menemukan generalisasi masalah yang akan berlaku pada banyak situasi berbeda.

Dalam kasus spesifik SAT, pertanyaan aljabar yang mungkin ditanyakan adalah apa yang terjadi ketika kita menafsirkan formula dalam kisi yang lebih umum daripada aljabar Boolean. Di sisi logis, Anda dapat menggeneralisasi masalah kepuasan dari logika proposisional ke logika intuitionistic. Secara lebih umum, Anda dapat menggeneralisasi masalah kepuasan proposisional dengan masalah menentukan apakah suatu formula, ketika ditafsirkan di atas kisi yang dibatasi (satu dengan bagian atas dan bawah), mendefinisikan elemen dasar kisi. Generalisasi ini memungkinkan Anda untuk memperlakukan masalah dalam analisis program sebagai masalah kepuasan.

Generalisasi lain adalah untuk logika first-order quantifier-free di mana Anda mendapatkan pertanyaan tentang Satisfiability Modulo a Theory. Artinya, selain memiliki variabel Boolean, Anda juga memiliki variabel orde pertama dan simbol fungsi dan Anda ingin tahu apakah formula memuaskan. Pada titik ini Anda dapat mengajukan pertanyaan tentang rumus dalam aritmatika, teori string, atau array, dll. Jadi kami mendapatkan generalisasi SAT yang ketat dan sangat berguna yang memiliki banyak aplikasi dalam sistem, keamanan komputer, bahasa pemrograman, verifikasi program, perencanaan , kecerdasan buatan, dll.