Mengapa ada perbedaan besar antara pemecah SAT?

Pemecah SAT sangat penting dalam serangan aljabar , misalnya walksat dan minisat .

Namun, ketika memecahkan masalah benchmark yang tersedia di sini ada perbedaan kinerja yang sangat besar antara keduanya - Walksat jauh lebih cepat daripada mini untuk masalah ini. Kenapa ini?

Ini pelaksanaan walksat tampaknya memiliki beberapa perbaikan kinerja - apakah ada alasan itu tidak termasuk dalam Kompetisi SAT internasional ?

Ya, ada perbedaan besar antara MiniSAT dan WalkSAT. Pertama, mari kita perjelas - MiniSAT adalah implementasi spesifik dari kelas generik dari algoritma DPLL / CDCL yang menggunakan pembelajaran backtracking dan klausa, sedangkan WalkSAT adalah nama umum untuk algoritma yang berganti-ganti antara langkah serakah dan langkah acak.

Secara umum DPLL / CDCL jauh lebih cepat pada instance SAT terstruktur sedangkan WalkSAT lebih cepat pada k-SAT acak . Instance SAT industri dan terapan cenderung memiliki banyak struktur, sehingga DPLL / CDCL dominan di sebagian besar pemecah SAT modern. Contoh untuk satu teknik mungkin menang, yang merupakan salah satu alasan mengapa pemecah portofolio menjadi populer.

Saya mengambil banyak masalah dengan klaim Anda bahwa WalkSAT jauh lebih cepat daripada MiniSAT dalam hal di halaman itu. Untuk satu hal, ada gigabytes instance SAT di sana - berapa banyak yang Anda coba bandingkan? WalkSAT sama sekali tidak kompetitif pada sebagian besar contoh terstruktur yang mengapa itu tidak sering terlihat di kompetisi.

Di samping catatan - Vijay benar bahwa MiniSAT masih relevan. Sebenarnya, karena open source dan ditulis dengan baik, MiniSAT adalah yang solver untuk mengalahkan untuk menunjukkan bahwa optimasi yang diberikan memiliki janji. Banyak orang mengutak-atik MiniSAT sendiri untuk menampilkan optimisasi mereka - lihatlah kategori "retas MiniSAT" dalam kompetisi SAT baru-baru ini.

Ada perbedaan besar antara instance sat . SAT solver mungkin melakukan dengan baik pada kelas contoh, tapi buruk pada kelas contoh, sementara solver berkinerja baik pada kelas dan buruk pada kelas .X Y B Y $A$$X$$Y$$B$$Y$$X$

Makalah yang baik untuk membaca tentang topik ini adalah yang ini oleh Nudelman et al . Inti dari makalah ini adalah untuk menentukan fitur yang mudah untuk dihitung dari instance SAT yang dapat memberi tahu Anda algoritma mana yang cenderung berkinerja baik dan mana yang tidak. Dengan menggunakan teknik ini dimungkinkan untuk membangun algoritma berbasis portofolio yang akan dengan cepat menganalisis instance masalah, kemudian memecahkan instance dengan algoritma yang paling tepat. Ada perkembangan makalah yang mengikuti yang itu; googling SATzilla akan menghasilkan banyak bahan bacaan.

Jika Anda bertanya-tanya mengapa SAT solver mungkin lebih baik daripada solver pada semua contoh, well, saya rasa itu adalah kemajuan :). Jika Anda ingin tahu apa yang membuat pemecah bagus, jawabannya mungkin bisa diubah menjadi beberapa tesis doktoral. Saya sarankan Anda mulai dengan makalah Nudelman et al .$A$$B$