Unduhan #SAT Solver

21

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
2
Halo Walter, pertanyaan Anda dekat dengan perbatasan yang secara resmi akan menjadi "topik" untuk situs ini. Namun, jika Anda tidak memiliki tempat lain untuk mengajukan pertanyaan ini dan kami dapat menjawabnya, mungkin tidak seburuk itu ... (Karena situs ini masih dalam pengembangan, saya pikir kami lebih terbuka daripada situs lain.) Yakinlah bahwa maksud dari komentar ini bukan untuk "memarahi" atau "memperingatkan", itu hanya pemberitahuan ramah.
Ryan Williams
Hai Ryan, terima kasih atas perhatiannya. Maaf jika pertanyaan ini dekat dengan perbatasan. Saya telah mencari di web dan saya tidak menemukan apa-apa: hanya beberapa pemecah SAT, tetapi tidak ada pemecah #SAT. Itu sebabnya saya bertanya di sini. Tentu saja saya tahu bahwa saya dapat menulis kode saya sendiri yang menggunakan SAT solver sebagai mesin untuk menghitung solusi, tetapi saya sedang mencari sesuatu yang sudah dibuat dan siap digunakan.
Giorgio Camerani
12
Saya ingin tidak setuju. Saya pikir pertanyaan seperti itu ada dalam ruang lingkup, dan seharusnya!
Suresh Venkat
setuju dalam ruang lingkupnya. fyi / imho itu tidak terlalu praktis untuk membangun pemecah #SAT dari pemecah SAT kecuali seseorang memiliki kode sumber dan bahkan dalam kasus itu, tidak begitu praktis, kecuali untuk formula yang sangat kecil, karena ledakan eksponensial yang sangat buruk. biasanya teknik khusus yang unik untuk #SAT dan bukan SAT akan diperlukan ...
vzn

Jawaban:

16

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.

Dave Clarke
sumber
Hai supercooldave, terima kasih untuk pointer Anda. Saya tidak tahu bahwa SAT4J memiliki kemampuan ini.
Giorgio Camerani
16

Anda juga dapat mencoba pemecah #SAT "sharpSAT" ( situs web , github ) untuk menghitung jumlah tugas yang memuaskan dari rumus CNF.

Holger
sumber
11

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.

mnO(mn)∼m+n

Radu GRIGore
sumber
7

Topik terkait: Pemecah SAT Terbaik .

MS Dousti
sumber
1
Terima kasih Sadeq. Topik yang Anda pilih tampaknya berorientasi teoretis. Ini daftar beberapa makalah tentang mengurangi batas atas. Ini sangat menarik, tetapi saya sedang mencari implementasi kerja yang siap digunakan.
Giorgio Camerani
2
Sama-sama. Di antara tautan yang dikutip di sana, ada satu yang murni praktis: satcompetition.org . Saya pikir Anda dapat menemukan implementasi yang sangat bagus di sana.
MS Dousti
7

Yang terbaik yang saya temukan adalah "c2d compiler". http://reasoning.cs.ucla.edu/c2d/

Ini menggunakan d-DNNF dan Anda membutuhkan opsi -count .

Leon Leon
sumber
c2d memecahkan lebih banyak CNF daripada sharpsat. Untuk tujuan mainan , pemecah sat "relsat" juga akan melakukannya.
Leon Leon
7

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.

Memilih
sumber
5

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.

Mikolas
sumber
2

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 .

serigala
sumber