gophersat
1.0.0
Ini adalah Gophersat, pemecah SAT dan pseudo-boolean yang ditulis murni di Go. Gophersat dikembangkan oleh CRIL (Centre de Recherche en Informatique de Lens) di Universitas Artois & CNRS. Ini dirilis di bawah lisensi MIT. Gophersat cukup efisien, yaitu pada benchmark SAT biasa, ia berjalan sekitar 2 hingga 5 kali lebih lambat dibandingkan pemecah tingkat atas (yaitu, glukosa atau minisat) yang sangat menginspirasinya. Itu juga dapat memecahkan masalah MAXSAT, dan masalah keputusan dan optimasi pseudo-boolean.
Versi stabil terakhir Gophersat adalah versi 1.4. Ini mencakup strategi penyelesaian bidang potong opsional.
Beberapa masalah, seperti masalah merpati yang terkenal, membutuhkan waktu yang sangat lama untuk diselesaikan dengan menggunakan penalaran logis murni.
Permasalahan kandang merpati dapat dinyatakan sebagai berikut: apakah mungkin untuk memasukkan n merpati ke dalam m lubang merpati, dimana m = n-1, tanpa memasukkan beberapa merpati ke dalam lubang yang sama dan memasukkan semua merpati ke dalam satu lubang? Jawabannya jelas: jika Anda mempunyai 4 ekor merpati di 3 lubang, Anda tidak bisa memasukkan semuanya ke dalam lubang yang berbeda. Tapi bagaimana Anda membuktikannya ? Pemecah SAT atau PB akan membuktikannya dengan mencoba semua kemungkinan kombinasi, dan jumlah kemungkinan kombinasi bertambah secara eksponensial. Jadi, mencoba menyelesaikan soal dengan n=20 dalam praktiknya tidak mungkin dilakukan, meskipun soal tersebut memiliki jawaban yang jelas.
Beberapa pemecah PB menerapkan strategi alternatif: strategi pemotongan bidang. Hal ini tidak akan dijelaskan secara rinci dalam dokumen ini, namun strategi ini bisa sangat efisien pada beberapa masalah, seperti masalah merpati yang tidak dapat diselesaikan secara efisien dengan penalaran logis murni, namun akan lebih lambat pada sebagian besar masalah.
Sekarang dimungkinkan untuk menggunakan pesawat potong dengan Gophersat. Cukup gunakan opsi baris perintah -cp . Jadi, alih-alih menelepon:
gophersat problem.opb
Telepon saja:
gophersat -cp problem.opb
Versi stabil terakhir Gophersat adalah versi 1.3. Ini adalah pembaruan kecil, menambahkan kemampuan untuk mengakses pemecah yang mendasarinya ketika menangani masalah MAXSAT.
Gophersat versi 1.2 mencakup cara untuk memahami kejadian UNSAT, baik dengan memberikan sertifikat RUP ketika masalahnya adalah UNSAT dan dengan menyediakan kemampuan untuk mengekstrak subset rumus yang tidak dapat dipenuhi. Beberapa bug juga diperbaiki, dan dukungan untuk penyelesaian SAT tambahan ditingkatkan.
Untuk mempelajari lebih lanjut tentang fungsi-fungsi ini, Anda dapat melihat tutorial tentang sertifikat UNSAT dan MUS.
Untuk menghasilkan sertifikat dengan executable gophersat, cukup panggil:
gophersat -certified problem.cnf
Sertifikat kemudian akan dicetak pada keluaran standar dengan menggunakan notasi RUP. Sertifikat dibuat dengan cepat, jadi ketahuilah bahwa sebagian sertifikat yang tidak berguna akan dibuat meskipun masalahnya sebenarnya dapat diselesaikan. Hal ini merupakan praktik yang umum terjadi di masyarakat, dan meskipun klausul yang dihasilkan tidak menimbulkan kebisingan, namun dalam praktiknya hal ini tidak menjadi masalah.
Untuk mengekstrak MUS dari instance UNSAT, cukup panggil:
gophersat -mus problem.cnf
MUS akan dicetak pada output standar. Jika masalahnya bukan pada UNSAT, pesan kesalahan akan ditampilkan.
Untuk saat ini, fasilitas ini hanya tersedia untuk permasalahan SAT murni (yaitu bukan permasalahan pseudo-boolean).
Sejak versi 1.1, Gophersat menyertakan pemecah inti baru yang lebih efisien untuk masalah SAT murni dan paket yang menangani masalah MAXSAT. Ini juga mencakup API baru untuk pengoptimalan dan penghitungan model, tempat model baru ditulis ke saluran segera setelah ditemukan.
Sejak versi 1.0, API Gophersat dianggap stabil, artinya API tersebut dijamin tetap kompatibel hingga versi utama diubah. Dengan kata lain, jika program Anda bekerja dengan gophersat versi 1.0, program tersebut akan tetap bekerja dengan versi 1.1 atau lebih tinggi, namun belum tentu dengan versi di atas 2.0.
Perhatikan bahwa, dengan "masih bekerja", yang kami maksud hanyalah "akan mengkompilasi dan menghasilkan keluaran yang sama", bukan "akan memiliki kinerja yang sama dari segi memori atau waktu". Ini merupakan perbedaan penting: selama peningkatan versi kecil, heuristik atau tipe data baru dapat diperkenalkan, yang berarti beberapa masalah tertentu dapat diselesaikan lebih cepat atau lebih lambat dari sebelumnya.
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat dapat digunakan sebagai pemecah mandiri (membaca file DIMACS CNF) atau sebagai perpustakaan dalam program go apa pun.
Untuk mengatasi file DIMACS, Anda dapat memanggil gophersat dengan sintaks berikut:
gophersat --verbose file.cnf
dimana --verbose merupakan parameter opsional yang membuat solver menampilkan informasi selama proses penyelesaian.
Gophersat juga mampu membaca dan menyelesaikan rumus boolean yang lebih umum, tidak hanya permasalahan yang direpresentasikan dalam format DIMACS yang tidak ramah pengguna. Ia juga berhubungan dengan batasan kardinalitas, yaitu klausa yang harus memiliki setidaknya n literal yang benar, dengan n > 1.
Gophersat dapat digunakan sebagai pemecah mandiri (membaca file OPB) atau sebagai perpustakaan dalam program go apa pun.
Untuk memecahkan masalah pseudo-boolean (baik masalah keputusan atau optimasi), Anda dapat memanggil gophersat dengan sintaks berikut:
gophersat --verbose file.opb
dimana --verbose merupakan parameter opsional yang membuat solver menampilkan informasi selama proses penyelesaian.
Untuk saat ini, hanya dapat menyelesaikan apa yang disebut masalah DEC-SMALLINT-LIN dan OPT-SMALLINT-LIN, yaitu masalah pengambilan keputusan (adakah solusinya atau tidak), untuk batasan linier (penjumlahan literal berbobot) pada bilangan bulat kecil (n < 2^30), atau masalah optimasi (apa solusi terbaik, meminimalkan fungsi biaya tertentu), untuk batasan linier pada bilangan bulat kecil.
Berkat paket maxsat , Gophersat kini dapat mengatasi masalah MAXSAT.
Untuk mengatasi masalah MAXSAT berbobot, Anda dapat memanggil gophersat dengan sintaks berikut:
gophersat --verbose file.wcnf
dimana --verbose merupakan parameter opsional yang membuat solver menampilkan informasi selama proses penyelesaian. File tersebut seharusnya direpresentasikan dalam (format WCNF)[http://www.maxsat.udl.cat/08/index.php?disp=requirements].
SAT, yang merupakan singkatan dari Boolean Satisfiability Problem , adalah masalah NP-complete kanonik, yaitu masalah yang tidak diketahui solusinya dan tidak memerlukan waktu eksponensial dalam kasus terburuk. Singkatnya, pemecah SAT mencoba menemukan, untuk rumus proposisional tertentu, sebuah penugasan untuk semua variabelnya yang membuatnya benar, jika penugasan tersebut ada.
Meskipun penerapan pemecah SAT menggunakan algoritme naif adalah hal yang sepele, penerapan seperti itu akan sangat tidak efisien dalam praktiknya. Gophersat mengimplementasikan fitur-fitur canggih sehingga cukup efisien, sehingga dapat digunakan dalam praktik di program Go yang memerlukan mesin inferensi yang efisien.
Meskipun ini tidak selalu merupakan keputusan terbaik karena alasan praktis, masalah NP-complete apa pun dapat diterjemahkan sebagai masalah SAT dan diselesaikan oleh Gophersat. Permasalahan tersebut meliputi Travelling Salesman Problem, kendala pemrograman, masalah Knapsack, perencanaan, pengecekan model, pengecekan kebenaran perangkat lunak, dan lain-lain.
Lebih lanjut mengenai masalah SAT dapat ditemukan di artikel wikipedia tentang SAT.
Anda juga dapat menemukan informasi tentang cara merepresentasikan rumus boolean Anda sendiri sehingga dapat digunakan oleh gophersat dalam tutorial "SAT for noobs".
MAXSAT adalah optimasi yang setara dengan masalah keputusan SAT. Meskipun pemecah SAT murni akan mengembalikan model yang memenuhi semua klausa atau UNSAT jika tidak ada model seperti itu, pemecah MAXSAT akan mengembalikan model yang memenuhi sebanyak mungkin klausa.
Ada ekstensi untuk MAXSAT.
MAXSAT Parsial berarti bahwa, meskipun kita ingin memenuhi sebanyak mungkin klausa, beberapa klausa (disebut klausa sulit ) harus dipenuhi, apa pun yang terjadi. Masalah MAXSAT parsial dapat dinyatakan tidak memuaskan.
Misalnya, membuat jadwal sekolah merupakan masalah parsial MAXSAT: ada soft (misalnya, kami ingin kelas sesedikit mungkin dimulai setelah jam 4 sore) dan hard (dua guru tidak boleh berada di dua tempat yang berbeda pada jam yang sama). pada saat yang sama) kendala.
MAXSAT tertimbang berarti bahwa klausul dikaitkan dengan biaya: meskipun opsional, beberapa klausul dianggap lebih penting daripada yang lain. Misalnya, jika klausa C1 memiliki biaya sebesar 3 dan klausa C2 dan C3 keduanya memiliki biaya sebesar 1, maka solusi yang memenuhi C1 namun tidak memenuhi C2 maupun C3 akan dianggap lebih baik daripada solusi yang memenuhi C2 dan C3 namun tidak memenuhi C1, semua solusi lainnya segala sesuatunya dianggap sama.
MAXSAT berbobot parsial berarti ada klausa lunak dan klausa keras dalam soal, dan klausa lunak diberi bobot. Dalam hal ini, MAXSAT "murni" adalah kasus khusus dari MAXSAT berbobot parsial yang lebih umum: masalah MAXSAT "murni" adalah masalah MAXSAT berbobot parsial di mana semua klausa merupakan klausa lunak yang diasosiasikan dengan bobot 1.
Masalah pseudo-boolean, dalam beberapa hal, merupakan generalisasi dari masalah SAT: klausa proposisional apa pun dapat ditulis sebagai batasan pseudo-boolean tunggal, tetapi merepresentasikan batasan pseudo-boolean memerlukan jumlah klausa proposisional yang eksponensial.
Ekspresi pseudo-boolean (linier) adalah ekspresi seperti:
w1 l1 + w2 x2 + ... + wn xn ≥ y
dimana y dan semua wi adalah konstanta bilangan bulat dan semua li adalah literal boolean.
Misalnya, ungkapan berikut ini benar
2 ¬x1 + x2 + x3 ≥ 3
variabel boolean x1 harus salah, dan setidaknya salah satu dari x2 dan x3 harus benar. Ini setara dengan rumus proposisional
¬x1 ∧ (x2 ∨ x3)
Ekspresi pseudo-boolean adalah generalisasi dari klausa proposisional: klausa apa pun
x1 ∨ x2 ∨ ... ∨ xn
dapat ditulis ulang menjadi
x1 + x2 + ... + xn ≥ 1
Deskripsi masalah pseudo-boolean bisa jauh lebih kecil daripada versi proposisionalnya, tetapi penyelesaian masalah psudo-boolean masih merupakan NP-complete.
Gophersat memecahkan masalah keputusan (apakah ada solusi untuk masalah tersebut), dan masalah optimasi. Masalah optimasi adalah masalah pseudo-boolean yang berhubungan dengan fungsi biaya, yaitu jumlah suku yang harus diminimalkan. Daripada hanya mencoba menemukan model yang memenuhi batasan yang diberikan, gophersat kemudian akan mencoba menemukan model yang dijamin memenuhi batasan dan meminimalkan fungsi biaya.
Selama pencarian solusi optimal tersebut, gophersat akan memberikan solusi suboptimal (yaitu solusi yang menyelesaikan semua kendala namun belum dijamin optimal) segera setelah menemukannya, sehingga pengguna bisa mendapatkan solusi suboptimal dalam waktu tertentu. batasi, atau tunggu lebih lama untuk jaminan solusi optimal.
Ya dan tidak. Ini jauh lebih cepat daripada implementasi yang naif, cukup cepat untuk digunakan pada permasalahan dunia nyata, namun lebih lambat dibandingkan pemecah tingkat atas, yang sangat optimal, dan canggih.
Gophersat tidak bertujuan untuk menjadi pemecah SAT/PB tercepat yang ada. Tujuannya adalah untuk memberikan akses ke teknologi SAT dan PB kepada para pedagang keliling, tanpa menggunakan antarmuka ke pemecah yang ditulis dalam bahasa lain (biasanya C/C++).
Namun, dalam beberapa kasus, berinteraksi dengan pemecah yang ditulis dalam bahasa lain adalah pilihan terbaik untuk aplikasi Anda. Jika Anda memiliki banyak masalah kecil yang harus diselesaikan, Gophersat akan menjadi alternatif tercepat. Untuk masalah yang lebih besar, jika Anda ingin memiliki ketergantungan sesedikit mungkin dengan mengorbankan waktu penyelesaian, Gophersat juga bagus. Jika Anda perlu memecahkan masalah yang sulit dan tidak keberatan menggunakan cgo atau menggunakan program eksternal, Gophersat mungkin bukan pilihan terbaik.
Ada beberapa pemecah SAT lainnya di Go, terutama go-sat dan gini. Performa Gini hampir setara dengan Gophersat, meskipun rata-rata sedikit lebih lambat, menurut pengujian yang kami lakukan.
Gophersat juga menyediakan fitur-fitur keren yang tidak selalu tersedia pada solver lain (misalnya, format input yang mudah digunakan), sehingga dapat digunakan sebagai alat untuk mendeskripsikan dan memecahkan masalah NP-hard yang dapat dengan mudah direduksi menjadi SAT/PB masalah.
Tidak. Paket bf (untuk "rumus boolean") menyediakan fasilitas untuk menerjemahkan rumus boolean apa pun ke CNF.
Ini dikenal sebagai penghitungan model, dan ya, ada fungsinya: solver.Solver.CountModels .
Anda juga dapat menghitung model dari baris perintah, dengan
gophersat --count filename
dimana nama file dapat berupa file .opb atau .cnf.
