Kelas formula boolean yang terkenal yang membutuhkan bukti resolusi panjang secara eksponensial

Anda mungkin sering menemukan metode cutting plane, propagasi variabel, cabang dan terikat, pembelajaran klausa, backtracking cerdas atau bahkan heuristik manusia yang dirajut tangan dalam solver SAT. Namun selama beberapa dekade solver SAT terbaik sangat bergantung pada teknik bukti resolusi dan menggunakan kombinasi hal-hal lain hanya untuk bantuan dan untuk mengarahkan pencarian gaya resolusi. Jelas, itu diduga bahwa algoritma APAPUN akan gagal untuk memutuskan pertanyaan kepuasan dalam waktu polinomial setidaknya dalam beberapa kasus.

Pada tahun 1985, Haken membuktikan dalam makalahnya "Keteguhan resolusi" bahwa prinsip lubang merpati dikodekan dalam CNF tidak mengakui bukti resolusi ukuran polinomial. Meskipun hal ini membuktikan sesuatu tentang sulitnya algoritme berbasis resolusi, ia juga memberikan kriteria yang dapat digunakan untuk menilai solver canggih - dan pada kenyataannya salah satu dari banyak pertimbangan yang masuk ke dalam merancang solver SAT hari ini adalah bagaimana kemungkinan untuk melakukan pada kasus-kasus 'sulit' yang diketahui.

Memiliki daftar kelas formula Boolean yang terbukti menerima bukti resolusi berukuran eksponensial berguna dalam arti memberikan rumus 'sulit' untuk menguji pemecah SAT baru. Pekerjaan apa yang telah dilakukan dalam menyusun kelas-kelas semacam itu bersama-sama? Apakah ada yang punya referensi yang berisi daftar tersebut dan bukti yang relevan? Harap sebutkan satu kelas rumus Boolean per jawaban.

Contoh sulit untuk resolusi :

1. Rumus Tseitin (lebih dari grafik expander).

2. Prinsip pigeonhole yang lemah ( ke ) (eksponensial dalam batas bawah, untuk sembarang ).n n m > $m$$n$$n$$m>n$

3. 3CNF acak dengan variabel dan klausa , untuk .O ( n 1,5 - ε ) 0 < ε < 1 /$n$$O(n^{1.5-\epsilon})$$0<\epsilon<1/2$

Survei teknis yang baik, relatif terbaru, untuk kompleksitas bukti batas bawah, lihat:

Nathan Segerlind: Kompleksitas Bukti Proposisi. Buletin Simbolik Logika 13 (4): 417-481 (2007) tersedia di: http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps

Ada sejumlah survei dan buku yang bagus tentang kompleksitas bukti proposisional yang berisi daftar tersebut. Banyak sistem bukti yang mensimulasikan resolusi, oleh karena itu setiap formula yang sulit bagi mereka akan sulit untuk diselesaikan.

Buku-buku:
1. Jan Krajicek, "Aritmatika terikat, logika proposisional, dan teori kompleksitas", 1995
2. Stephen A. Cook dan Phoung The Neguyen, "Yayasan Logika Bukti Kompleksitas", 2010

Survei:
1. Paul Beame, dan Toniann Pitassi, "Kompleksitas bukti proposisional: Masa Lalu, Sekarang dan Masa Depan", 2001
2. Samuel R. Buss, "Aritmatika Terikat dan Kompleksitas Bukti Proposisi", 1997
3. Alasdair Urquhart, "Kompleksitas bukti proposisional ", 1995

Lihat juga yang tercantum di sini dan di sini .

Contoh sulit lain untuk resolusi adalah formula papan catur yang dimutilasi. Mereka menyatakan bahwa papan catur dengan dua sudut yang berlawanan secara diagonal tidak dapat ditutupi dengan ubin. Lihat:2 × $2n \times 2n$$2\times 1$

Michael Alekhnovich. Masalah papan catur yang dimutilasi secara eksponensial sulit untuk diselesaikan. Ilmu Komputer Teori 310 (1-3): 513-525 (2004). http://dx.doi.org/10.1016/S0304-3975(03)00395-5

$n\to (k)^2_2$$k=\lfloor \frac12 \log n \rfloor$$\bigvee_{i,j\in K} x_{i,j}$$\bigvee_{i,j\in K} \neg x_{i,j}$$K\subseteq \{ 1 , \ldots , n \}$$|K| = k$

Ada konstruksi di halaman 9 tulisan ini oleh Groote dan Zantema .

Tidakkah DIMACS mempertahankan set contoh instance SAT yang keras? Saya tidak dapat menemukannya di sana hanya dengan tampilan sepintas, tetapi jika Anda memasukkan "SAT" ke dalam kotak pencarian mereka, itu akan memunculkan banyak hits termasuk beberapa makalah / pembicaraan tentang instance SAT yang keras.