Kendala kepuasan masalah (CSP) vs teori modulo satisfiability (SMT); dengan coda pada pemrograman kendala

Apakah seseorang berani mencoba untuk menjelaskan apa hubungan bidang studi ini atau bahkan mungkin memberikan jawaban yang lebih konkret di tingkat masalah? Seperti yang termasuk yang mengasumsikan beberapa formulasi diterima secara luas. Jika saya mendapatkan ini dengan benar, ketika Anda beralih dari SAT ke SMT pada dasarnya Anda memasuki bidang CSP; sebaliknya, jika Anda membatasi CSP untuk boolean, Anda pada dasarnya berbicara tentang SAT dan mungkin beberapa masalah terkait seperti #SAT. Saya pikir ini sangat jelas (misalnya, bab Kolaitis dan Vardi "Pendekatan logis untuk Memuaskan Kepuasan" dalam Teori Model Hingga dan Penerapannyaoleh Grädel et al.), tetapi yang kurang jelas bagi saya adalah kapan kendala "modulo teori" dan kapan bukan? Apakah SMT selalu menyiratkan teori hanya menggunakan persamaan kesetaraan dan ketidaksetaraan selalu di bidang CSP yang lebih luas? Sejauh yang saya tahu, Anda sering dapat memperkenalkan variabel slack , sehingga perbedaan [jika ada] kurang jelas.

"Buku pedoman Kepuasan" yang relatif baru (IOP Press 2009) mengumpulkan masalah SMT dan CSP di bawah payung "kepuasan" yang luas, tetapi mengingat cara penyusunannya (bab-bab yang ditulis oleh berbagai penulis) tidak benar-benar membantu saya dalam mencari tahu ini. .

Saya berharap terminologi menjadi kurang membingungkan ketika Anda berbicara tentang kendala pemrograman , yang (dengan analogi dengan istilah '' pemrograman matematika '') Saya harap melibatkan meminimalkan / memaksimalkan beberapa fungsi tujuan. Artikel Wikipedia tentang pemrograman kendala sangat samar sehingga saya tidak bisa mengatakan apakah framing ini terjadi. Apa yang dapat saya kumpulkan dari Essentials of Constraint Programming oleh Frühwirth dan Abdennadher (hlm. 56) adalah bahwa "pemecah kendala" biasanya menyediakan lebih dari sekadar pemeriksa kepuasan, dengan penyederhanaan dll menjadi penting dalam praktik.

Walaupun ini bukan pertanyaan riset teori CS yang sebenarnya, saya tidak mengharapkan jawaban yang bagus untuk yang ini di situs CS.SE sarjana yang memberikan apa yang saya lihat di https://cs.stackexchange.com/questions/14946/distinguish- decision-procedure-vs-smt-solver-vs-theorem-prover-vs-constraint-sol (yang berisi banyak kata tetapi tidak apa yang saya anggap sebagai jawaban nyata, sayangnya).

SAT, CP, SMT, (sebagian besar) ASP semuanya berurusan dengan masalah optimisasi kombinatorial yang sama. Namun, mereka datang pada masalah ini dari sudut yang berbeda dan dengan kotak peralatan yang berbeda. Perbedaan-perbedaan ini sebagian besar dalam bagaimana setiap pendekatan menyusun informasi tentang eksplorasi ruang pencarian. Analogi kerja saya adalah bahwa SAT adalah kode mesin, sementara yang lain adalah bahasa tingkat yang lebih tinggi.

$x_1 \lor \overline{x_2} \lor x_3$$\{(x_1,0),(x_2,1),(x_3,0)\}$$x_1$$x_3$$x_2$$x_1 \lor \overline{x_2} \lor x_3 \lor x_4$$x_1 \lor \overline{x_2} \lor x_3 \lor \overline{x_4} \lor x_5$

Perkiraan struktur klausa dijaga untuk mempersempit himpunan solusi, dan untuk membantu menentukan apakah himpunan ini kosong. Selama pencarian beberapa penugasan sebagian mungkin ternyata tidak terkandung dalam solusi apa pun (bahkan jika masing-masing memenuhi masing-masing kendala dalam contoh). Ini dikenal sebagai nogoods , istilah yang diperkenalkan oleh ("Tuan GNU") Stallman dan Sussman$x \le 5$$x = 5$. Oleh karena itu tidak ada struktur klausa umum tunggal tetapi satu terkait dengan masing-masing pilihan representasi, tergantung pada apa yang lajang (literal) dari struktur klausa mewakili.

Constraint programming (CP) secara tradisional merupakan disiplin AI, dengan fokus pada penjadwalan, penjadwalan, dan masalah kombinatorial, dan oleh karena itu memiliki peran sentral untuk variabel yang dapat mengambil lebih dari hanya dua nilai (tetapi biasanya hanya banyak yang terbatas). CP telah menekankan pencarian yang efisien dan, dimotivasi oleh aplikasi tradisional, telah memberikan peran sentral pada all-differentkendala (injectivity), tetapi juga telah mengembangkan penyebar efisien untuk banyak jenis kendala lainnya. Definisi formal CP sudah ada sejak setidaknya 1974 1974 paper Networks of Montanari kendala, dengan prekursor akan kembali lebih awal. Berat sejarah ini mungkin telah berkontribusi pada CP yang tertinggal dari pendekatan lain dalam kinerja mentah selama dekade terakhir. CP secara klasik mempertahankan perkiraan komplemen dari struktur klausa, melalui seperangkat domain aktif untuk variabel. Tujuannya adalah untuk menghilangkan nilai-nilai dari domain aktif, menjelajahi struktur klausa dengan mencoba menetapkan nilai kandidat ke variabel dan melacak kembali bila perlu.

Teori modulo Satisfiability (SMT) keluar dari komunitas verifikasi. Setiap teori dalam pemecah SMT membentuk representasi implisit dari banyak klausa SAT yang berpotensi jauh. Teori-teori yang digunakan dengan SMT dan kendala yang digunakan dalam CP mencerminkan aplikasi historis yang berbeda. Sebagian besar teori yang dipertimbangkan SMT berkaitan dengan array berindeks integer, bidang tertutup nyata, perintah linier, dan semacamnya; ini muncul dari analisis statis program (dalam verifikasi berbantuan komputer) atau ketika memformalkan bukti matematis (dalam penalaran otomatis). Sebaliknya, dalam penjadwalan dan penjadwalan kendala injektivitas adalah sentral, dan meskipun bahasa SMTLIB standar telah memiliki kendala injektivitas sejak awal pada tahun 2003 (melaluidistinctsimbol), hingga 2010 SMT solver hanya diimplementasikan distinctmelalui algoritma naif. Pada tahap itu teknik pencocokan dari standar CP propagator untuk all-differentporting, untuk efek besar ketika diterapkan pada daftar variabel besar; lihat Pemecah kendala alldifferent di SMT oleh Banković dan Marić, SMT 2010. Selain itu, kebanyakan propagator CP dirancang untuk masalah dengan domain terbatas, sedangkan teori SMT standar menangani domain tak terbatas (bilangan bulat, dan baru-baru ini real) di luar kotak. SMT menggunakan instance SAT sebagai pendekatan dari struktur klausa, mengekstraksi nogood klausa dari teori yang sesuai. Ikhtisar yang bagus adalah Teori Modulo Kepuasan: Pendahuluan dan Aplikasi oleh De Moura dan Bjørner, doi: 10.1145 / 1995376.1995394.

Answer set programming (ASP) keluar dari pemrograman logika. Karena fokusnya pada pemecahan masalah yang lebih umum dalam menemukan model yang stabil, dan juga karena memungkinkan kuantifikasi universal dan eksistensial, ASP selama bertahun-tahun tidak bersaing dengan CP atau SMT.

Secara formal, SAT adalah CSP pada domain Boolean, tetapi fokus pada SAT pada pembelajaran klausa, heuristik yang baik untuk deteksi konflik, dan cara cepat untuk mundur sangat berbeda dengan fokus CSP tradisional pada penyebar, membangun konsistensi, dan heuristik untuk pemesanan variabel. SAT biasanya sangat efisien, tetapi untuk banyak masalah diperlukan upaya besar untuk terlebih dahulu mengungkapkan masalah sebagai instance SAT. Menggunakan paradigma tingkat yang lebih tinggi seperti CP dapat memungkinkan ekspresi masalah yang lebih alami, dan kemudian instance CP dapat diterjemahkan ke dalam SAT dengan tangan, atau alat dapat menangani terjemahan. Ikhtisar bagus dari mur dan baut dari SAT adalah Pada Pemecah Kepuasan Pembelajaran Klausa Modern oleh Pipatsrisawat dan Darwiche, doi: 10.1007 / s10817-009-9156-3 .

Sekarang mari kita beralih dari generalisasi ke spesifik hari ini.

Selama dekade terakhir beberapa orang di CP sudah mulai fokus pada lazy clause generation (LCG). Ini pada dasarnya adalah cara untuk mengikat propagator CP bersama-sama menggunakan teknik seperti SMT yang lebih fleksibel daripada abstraksi domain aktif yang agak kaku. Ini berguna karena ada sejarah panjang propagator CP yang diterbitkan untuk secara efisien mewakili dan memecahkan berbagai jenis masalah. (Tentu saja, efek yang sama akan dicapai dengan upaya bersama untuk menerapkan teori-teori baru untuk pemecah SMT.) LCG memiliki kinerja yang seringkali bersaing dengan SMT, dan untuk beberapa masalah mungkin lebih unggul. Tinjauan singkat adalah makalah Stuckey's CPAIOR 2010 Lazy Clause Generation: Menggabungkan kekuatan SAT dan CP (dan MIP?) Pemecahan , lakukan: 10.1007 / 978-3-642-13520-0_3. Juga patut dibaca makalah posisi Garcia de la Banda, Stuckey, Van Hentenryck dan Wallace, yang melukiskan visi CP-sentris dari The Future of Optimization Technology , doi: 10.1007 / s10601-013-9149-z .

Sejauh yang saya tahu, banyak fokus penelitian SMT baru-baru ini tampaknya telah bergeser ke aplikasi dalam metode formal dan matematika formal. Contohnya adalah merekonstruksi bukti yang ditemukan oleh pemecah SMT di dalam sistem bukti seperti Isabelle / HOL, dengan membangun taktik Isabelle / HOL untuk mencerminkan aturan inferensi dalam jejak bukti SMT; lihat Rekonstruksi Bukti Gaya LCF Cepat untuk Z3 oleh Böhmer dan Weber di ITP 2010.

Para pemecah ASP teratas selama beberapa tahun terakhir telah dikembangkan untuk menjadi kompetitif dengan pemecah hanya untuk CP, SMT dan SAT. Saya hanya samar-samar terbiasa dengan detail implementasi yang memungkinkan solver seperti claspmenjadi kompetitif sehingga tidak dapat benar-benar membandingkannya dengan SMT dan CP, tetapi gesper secara eksplisit mengiklankan fokusnya pada pembelajaran nogoods.

Memotong batas-batas tradisional antara formalisme ini adalah terjemahan dari representasi masalah yang lebih abstrak ke formalisme tingkat rendah yang dapat diimplementasikan. Beberapa pemecah top ASP dan CP sekarang secara eksplisit menerjemahkan input mereka ke dalam instance SAT, yang kemudian dipecahkan menggunakan solver SAT off-the-shelf. Dalam CP, asisten pemodelan kendala Savile Row menggunakan teknik desain kompiler untuk menerjemahkan masalah yang diekspresikan dalam bahasa tingkat menengah Essence 'menjadi formalisme tingkat yang lebih rendah, cocok untuk input ke pemecah CP seperti Minion atau MiniZinc . Savile Row awalnya bekerja dengan representasi CP sebagai formalisme tingkat rendah tetapi memperkenalkan SAT sebagai target dalam versi 1.6.2. Apalagi Essence bahasa tingkat lebih tinggisekarang dapat secara otomatis diterjemahkan ke dalam Essence 'oleh alat Conjure . Pada saat yang sama, solver SAT-level rendah seperti Lingeling terus disempurnakan setiap tahun, yang terbaru dengan bergantian belajar klausa dan fase dalam proses; lihat gambaran singkat Apa yang Terpanas dalam Kompetisi SAT dan ASP oleh Heule dan Schaub di AAAI 2015.

Analogi dengan sejarah bahasa pemrograman tampaknya cocok. SAT menjadi semacam "kode mesin", menargetkan model eksplorasi klausa tingkat rendah dalam struktur klausa. Paradigma abstrak menjadi lebih seperti bahasa komputer tingkat yang lebih tinggi, dengan metodologi dan aplikasi mereka sendiri yang baik dalam menangani. Akhirnya, kumpulan tautan yang semakin padat antara berbagai lapisan ini mulai menyerupai ekosistem optimisasi kompiler.