Mengubah masalah (matematika) menjadi instance SAT

Apa yang ingin saya lakukan adalah mengubah masalah matematika yang saya miliki menjadi masalah kepuasan boolean (SAT) dan kemudian menyelesaikannya menggunakan SAT Solver. Saya ingin tahu apakah seseorang mengetahui manual, panduan, atau apa pun yang akan membantu saya mengubah masalah saya menjadi instance SAT.

Juga, saya ingin menyelesaikan ini lebih baik daripada waktu yang eksponensial. Saya berharap SAT Solver akan membantu saya.

Bab 2 dari SAT Handbook (oleh Steven Prestwich) membahas bagaimana mengubah masalah keputusan yang terpisah menjadi CNF, secara mendalam. (Sayangnya, saya tidak berpikir ada versi konsep online - mungkin terbaik untuk berkonsultasi dengan perpustakaan setempat Anda.) Beberapa referensi lain yang dikutip dalam ikhtisar unik Magnus Björk Teknik Penyandian SAT yang Sukses juga berguna.

Jika masalah Anda terus-menerus, atau Anda terutama tertarik pada sistem ketidaksetaraan, maka jenis-jenis pemecah masalah lainnya lebih mungkin bermanfaat. Seperti yang ditunjukkan Kyle, pemecah SMT (seperti Z3 , Yices , atau OpenSMT ) mungkin berguna, meskipun teori SMT tradisional cenderung berfokus pada verifikasi perangkat lunak komputer, sehingga pemecah SMT biasanya memiliki dukungan besar untuk hal-hal seperti ekspresi yang melibatkan interval bilangan bulat , tetapi mungkin berkinerja buruk pada kendala injeksi. Untuk masalah yang secara alami dinyatakan sebagai sistem ketidaksetaraan, CPLEX adalah satu-satunya yang harus dikalahkan (dulu tersedia untuk penggunaan akademik secara gratis, dan mungkin masih). Untuk beberapa masalah keputusan kombinatorial (seperti menemukanpaket persegi panjang menjadi persegi ), pemecah kendala seperti Minion mengungguli pemecah SAT dan sering lebih mudah digunakan.

Kecuali jika Anda menerjemahkan masalah matematika ke instance SAT sebagai latihan pembelajaran, waktu Anda akan jauh lebih bermanfaat untuk belajar tentang teori modulo yang memuaskan . SMT akan memungkinkan Anda untuk mengekspresikan persamaan dan kendala lainnya jauh lebih alami daripada sebagai contoh Boolean SAT. Beberapa pemecah SMT mendukung quantifiers eksistensial dan universal, memungkinkan Anda untuk bergerak melampaui NP dan mengekspresikan masalah PSPACE.

Selain lebih ekspresif, pemecah SMT lebih cepat. Bukan P = NP lebih cepat, tetapi lebih efisien karena pemecah SMT yang baik tidak membuang informasi struktural khusus teori yang membantu memandu pemecah melalui ruang pencarian. Melakukan pengurangan Karp langsung ke instance SAT memaksa pemecah SAT untuk mempelajari kembali semua struktur itu, seringkali dengan biaya eksponensial. Misalnya, fakta bahwa penambahan bersifat komutatif hilang pada kedua pemecah SAT berbasis pencarian dan DPLL lokal; pemecah tidak menyadari bahwa itu berurusan dengan angka sama sekali! Untuk menghindari mencoba semua permutasi x + y + z = 10, pemecah SAT perlu kode pemecahan simetri, yang memerlukan deteksi automorfisme grafik. Algoritma pengenalan automorfisme grafik terbaik saat ini membutuhkan eksponensial waktu ke jumlah simpul dalam kasus terburuk,

Dua alat yang mengonversi bahasa tingkat tinggi ke SMT atau CNF.

CVC Sintaksnya dekat dengan CAS.

CBMC Ini mengkonversi program C ke CNF, memungkinkan pernyataan. Penegasan itu selalu benar, atau jika salah input input balik ditemukan. CBMC membuka gulungan, sehingga program C tertentu memiliki CNF / SMT yang besar secara eksponensial.