Kapan menggunakan SAT vs Constraint Satisfaction?

Jika saya memiliki masalah, satu pendekatan standar adalah untuk menyatakannya sebagai instance SAT dan mencoba menjalankan solver SAT di atasnya. Pendekatan standar lain adalah untuk menyatakannya sebagai masalah kepuasan kendala, dan coba gunakan pemecah CSP. Keduanya terasa agak mirip dalam masalah seperti apa yang dapat diekspresikan secara alami dalam format input mereka.

Apakah ada pedoman atau aturan praktis tentang bagaimana mengenali, untuk masalah tertentu, pendekatan mana yang lebih mungkin memberikan hasil yang baik? Apakah ada panduan yang dapat ditawarkan siapa pun tentang masalah apa yang dapat ditangani lebih baik oleh pemecah SAT daripada oleh pemecah CSP, atau sebaliknya?

(Jelas, ada beberapa masalah mudah yang dapat diselesaikan dengan kedua pendekatan. Ada juga beberapa masalah sulit yang tidak dapat diselesaikan dengan baik oleh kedua pendekatan. Mari kita kesampingkan itu. Kasus di mana bimbingan paling membantu adalah masalah di mana SAT baik solver berkinerja lebih baik daripada solver CSP, atau di mana solver CSP berkinerja lebih baik daripada solver SAT.Bagaimana saya mengenali kapan solver SAT cenderung lebih cocok daripada solver CSP, atau ketika solver CSP cenderung lebih cocok daripada solver SAT seorang pemecah SAT - yaitu, pendekatan mana yang harus dicoba terlebih dahulu?)

Perhatikan bahwa masalah tidak bisa terlalu sulit jika Anda ingin mengurangi menjadi SAT.

Raphael

Atau mengapa hanya fokus pada SAT / CSP, bagaimana dengan SMT?

Juho

Menggunakan alat solver kendala memiliki keuntungan bahwa Anda dapat dengan mudah mencoba beberapa optimasi (misalnya teknik melanggar simetri) pada contoh yang tidak terlalu sulit (dan periksa efektivitas optimasi seperti itu). Selain itu banyak dari mereka dapat menampilkan file CNF standar sebagai output antara.

Vor

Poin bagus, @Juho! SMT juga patut dipertimbangkan - jangan ragu untuk membandingkan ketiganya (SAT, CSP, SMT), jika Anda memiliki pemikiran tentang itu.

Saya punya pertanyaan yang sama, terima kasih sudah bertanya.

xxx ---

Jawaban:

Saya pikir ini adalah pertanyaan yang sangat bagus. Anda juga bisa bertanya: kapan harus menggunakan SMT solver? Saya punya perasaan mungkin sulit untuk menentukan sebelum memodelkan masalah dan benar-benar menjalankan pemecah CSP / SAT / SMT dan mencari tahu. Telah diketahui bahwa bahkan pemecah yang berbeda bekerja sangat berbeda pada instance yang sama! Intuisi saya juga berasal dari fakta bahwa ada banyak cara untuk memodelkan masalah. Selain itu, ada banyak cara untuk melakukan pencarian dan inferensi, tergantung pada jenis kendala apa yang digunakan (jika formalisme yang dimaksud memungkinkan berbagai jenis).

Ambil contoh puzzle Sudoku standar. Untuk standar $8 \times 8$ puzzle, pemecah SAT / CSP modern akan memecahkan puzzle seperti itu dalam sekejap. Namun, saya lebih suka menggunakan pemecah CSP karena itu lebih mudah untuk mengekspresikan niat saya. Kebutuhan teka-teki yang disebutkan $9+9+9=27$ kendala alldiff, dan saya sudah selesai. Sebenarnya ada sedikit riset dalam konteks pemecah CSP yang mencoba memecahkan contoh Sudoku dengan ukuran berbeda. Sejauh yang saya ingat, mereka tidak melakukan perbandingan antara SAT, tetapi mencoba untuk menentukan inferensi seperti apa yang terbaik, atau teka-teki Sudoku seperti apa yang sulit. Saya tidak tahu jika untuk mengatakan $32 \times 32$ Teka-teki Sudoku, pemecah SAT akan lebih cepat dari pemecah CSP.

Formalisme yang berbeda dapat menangkap informasi spesifik domain dan mengeksploitasinya dengan lebih baik dan dengan cara yang berbeda. Untuk sedikit lebih banyak tentang ini, lihat jawabannya dan komentar di sini .

Juho
sumber