Apa kendala untuk membuat pemecah SAT kompetitif dengan algoritma grafik khusus? Dengan kata lain, apakah layak untuk mengharapkan pemecah SAT yang dapat menggantikan peran perancang algoritma - yaitu, dapat secara otomatis mengenali struktur masalah dan kemudian menyelesaikannya secepat algoritma khusus?
Berikut beberapa contoh yang menurut saya menantang untuk pemecah SAT hari ini:
Menghitung satuan ukuran independen . Pengkodean "x adalah perangkat ukuran k yang independen" memberikan rumus besar yang sulit dipecahkan. Pemecah SAT yang ideal akan mengenali bahwa masalah ini mudah pada grafik lebar pohon yang dibatasi dengan penambahan variabel "jumlah" tambahan untuk tas.
Menemukan pohon Steiner minimum. Sekali lagi, "Steiner tree" memiliki kendala global, namun, algoritma khusus (seperti di sini ) membuat tugas lebih mudah dengan menambahkan variabel tambahan
Masalah apa pun yang mengurangi ke pencocokan sempurna planar.
sumber
Jawaban:
Ada kertas bagus yang membantu memvisualisasikan struktur internal instance SAT. Lihat Memvisualisasikan Mesin Virtual SAT dan Proses Algoritme DPLL oleh Carsten Sienz (Muncul dalam SAT 2004). Pada dasarnya, ini menggambar grafik yang penulis sebut "grafik interaksi variabel" (menurut beberapa aturan) untuk memvisualisasikan hubungan antara klausa yang puas. Penulis menunjukkan ini dengan beberapa kali menjalankan sebagian DPLL.
Klaim utama adalah bahwa teknik visualisasi ini dapat digunakan untuk mendeteksi struktur dan merancang algoritma yang tepat untuknya. Namun, masih belum jelas bagaimana kita dapat mendeteksi struktur secara efisien seperti yang disajikan di koran. Telah diketahui bahwa algoritma SAT untuk satu masalah spesifik berperilaku buruk pada masalah lain. Jadi ada "no-free-lunch", meskipun klaim ini tidak dapat dinyatakan secara formal sejauh yang saya tahu.
sumber