Adakah yang bisa menunjuk ke satu atau lebih situs web di mana dimungkinkan untuk mengunduh implementasi kerja pemecah #SAT? Saya tertarik pada mereka yang mengembalikan hitungan solusi yang tepat, bukan perkiraan.
ds.algorithms
sat
software
Giorgio Camerani
sumber
sumber
Jawaban:
Anda dapat melakukan ini dengan SAT4J , cukup dengan mengulangi semua model: http://www.sat4j.org/howto.php#models . Saya membayangkan bahwa sebagian besar pemecah SAT memiliki kemampuan ini.
sumber
Anda juga dapat mencoba pemecah #SAT "sharpSAT" ( situs web , github ) untuk menghitung jumlah tugas yang memuaskan dari rumus CNF.
sumber
Salah satu opsi adalah menggunakan perpustakaan BDD, seperti JavaBDD . Semua perpustakaan seperti itu memiliki fungsi yang menghitung solusi dengan cepat atau, setidaknya, mereka membuatnya mudah untuk menulis fungsi seperti itu. Kerugiannya, bagaimanapun, membangun BDD akan lambat dalam banyak kasus dan mungkin membutuhkan banyak memori.
sumber
Topik terkait: Pemecah SAT Terbaik .
sumber
Yang terbaik yang saya temukan adalah "c2d compiler". http://reasoning.cs.ucla.edu/c2d/
Ini menggunakan d-DNNF dan Anda membutuhkan opsi -count .
sumber
MBound Solver yang diberikan di sini http://www.cs.cornell.edu/~sabhar/ dapat memberikan jumlah model dengan jaminan probabilistik. Ini jauh lebih cepat daripada menghitung semua solusi.
sumber
Saya menulis model kecil / enumerator implant utama . Ini sudah bisa digunakan untuk penghitungan model dengan enumerasi model tetapi itu tidak terlalu praktis. Jika ada yang tertarik, saya dapat memperluasnya sehingga menghitung model dari implan utama.
sumber
Situs web BeyondNP berisi inventaris yang baik dari alat yang ada untuk menyelesaikan #SAT (dan masalah sulit terkait lainnya pada rumus CNF). Anda juga dapat menemukan daftar alat untuk perkiraan penghitungan model dan kompilasi pengetahuan (tugas mengubah CNF menjadi struktur data yang mudah-mudahan ringkas yang sering mendukung penghitungan model waktu polinomial).
Anda juga dapat menemukan daftar alat untuk preprocessing formula CNF yang mungkin berguna untuk meningkatkan kinerja penghitung model dan berbagai tolok ukur .
sumber
Berikut ini satu yang disebut tensorCSP dan berdasarkan pada alat yang disebut jaringan tensor. Dijelaskan dalam tulisan ini .
sumber
Glukosa adalah pemecah SAT yang sangat efisien yang dikembangkan di universitas Bordeaux.
https://www.labri.fr/perso/lsimon/glucose/
sumber