Mulai makalah SAT solver

Saya ingin membuat pemecah SAT pertama. Saya tahu kompetisi SAT dan konferensi SAT, dan ada begitu banyak makalah tentang hal ini. Saya seorang pemula, seorang pemula yang kewalahan. Di mana saya harus mulai? Akhirnya saya ingin mendorong yang canggih. Saya ingin beberapa saran ahli tentang cara memulainya, sehingga saya tidak akan membuang waktu untuk hal-hal yang tidak penting terlalu dini. Terimakasih banyak.

Ikhtisar pemula yang sangat baik diberikan oleh artikel berikut dari 2009.

• Kepuasan Boolean: Dari Kekerasan Teoretis hingga Kesuksesan Praktis , Sharad Malik, Lintao Zhang, Komunikasi ACM, 2009

Ada beberapa cara untuk masuk ke aspek teknis. Anda bahkan dapat mulai dengan kertas Davis-Putnam yang asli. Ini sangat jelas dan memiliki contoh-contoh terperinci. Ketika membahas optimasi SAT dalam kursus, kami menemukan bahwa beberapa orang mungkin membayangkan sudah ada di sana. Makalah Davis-Logeman-Loveland (saya merasa) kurang instruktif, tetapi sangat singkat sehingga Anda bisa membacanya.

• Prosedur Komputasi untuk Teori Kuantifikasi , Martin Davis, Hilary Putnam, Jurnal ACM, 1960.
• Program mesin untuk pembuktian teorema , Martin Davis, George Logemann, Donald Loveland, Communications of the ACM, 1962.

Mungkin ada cara untuk mengejar perkembangan 50 tahun ke depan. Saya akan merekomendasikan slide kuliah. Hanya mencari 'DPLL' akan memunculkan banyak tutorial. Jika Anda menjelajahinya, saya yakin kabutnya akan hilang - sampai batas tertentu. Ada juga banyak survei bermanfaat. Kertas Zhang-Malik adalah tempat yang baik untuk memulai. Ada beberapa artikel dalam Buku Pegangan Kepuasan yang mungkin berguna bagi Anda.

• Pencarian untuk Pemecah Kepuasan Boolean yang Efisien , Lintao Zhang, Sharad Malik, makalah yang diundang bersama untuk CAV dan CADE 2002.
• Buku Pegangan Kepuasan , Diedit oleh Armin Biere, Marijn Heule, Hans van Maaren, dan Toby Walsh, 2009
• Anatomi dan Evaluasi Empiris Pemecah SAT Modern , Karem Sakallah, Joao Marques-Silva, Buletin EATCS, 2011.

Saya mendukung saran Mikolaos. Kode MiniSAT bersih dan ukurannya bisa diatur. Anda bisa bermain dengannya. Ada beberapa solver lain yang bisa Anda coba. CryptoMiniSat juga cukup bersih. Anda juga harus berkonsultasi dengan karya Armin Biere , yang menulis solver SAT dan menulis tentang menulis solver SAT.

Saya sarankan pertama memahami teknik mana yang benar-benar memajukan solver, untuk yang saya sarankan ikhtisar dan analisis berikut .

Maka saya akan merekomendasikan mengunduh kode sumber minisat dan membaca deskripsinya .

Tentu saja mungkin individu tetapi saya menemukan melihat kode sumber yang paling berharga.

Jika Anda kewalahan oleh semua pekerjaan yang ada di luar sana, mengapa Anda tidak mulai berpura-pura bahwa tidak ada yang memperbaiki masalah sebelumnya? Jika tujuan Anda adalah untuk akhirnya membangun pemecah SAT yang kompetitif, itu akan menjadi perjalanan yang cukup panjang. Dengan memulai hanya bermain-main tanpa 'memeriksa solusinya', Anda bisa mendapatkan lebih banyak daripada kalah.

$n$$m$$n$$m$ .

$n$$m$

Mulailah dengan kertas survei yang bagus. Sangat mudah untuk menyerang sedikit demi sedikit subjek dan menjadi bingung dengan nama yang berbeda dalam literatur untuk teknik yang sama dan nama yang sama digunakan untuk teknik yang berbeda. Juga mudah untuk memberlakukan kembali pertempuran algoritmik lama (daftar terjadi vs daftar kepala-ekor vs. dua literal yang ditonton untuk implementasi DPLL misalnya) jika Anda tidak tahu bagaimana keadaannya.

Pemecah Kepuasan oleh Gomes, et. Al. akan memberi Anda tanah yang kasar.

Meningkatkan Solver SAT Menggunakan Teknik-Teknik Mutakhir oleh Manthey akan membawa Anda lebih dekat ke masa kini.