Penjelasan teoretis untuk keberhasilan praktis pemecah SAT?

Penjelasan teoretis apa yang ada untuk keberhasilan praktis pemecah SAT, dan dapatkah seseorang memberikan ikhtisar dan penjelasan "gaya-wikipedia" yang mengikat semuanya?

Secara analogi, analisis yang dihaluskan ( versi arXiv )) untuk algoritme simpleks melakukan pekerjaan yang hebat menjelaskan mengapa ia bekerja dengan sangat baik dalam praktiknya, terlepas dari kenyataan bahwa dibutuhkan waktu yang eksponensial dalam kasus terburuk dan NP-perkasa ( versi arXiv ).

Saya telah mendengar sedikit tentang hal-hal seperti pintu belakang, struktur grafik klausa, dan transisi fase, tetapi (1) Saya tidak melihat bagaimana semua ini cocok untuk memberikan gambaran yang lebih besar (jika mereka lakukan), dan (2) Saya tidak tahu apakah ini benar-benar menjelaskan mengapa pemecah SAT bekerja dengan sangat baik, misalnya, pada contoh industri. Juga, ketika sampai pada hal-hal seperti struktur grafik klausa: mengapa pemecah saat ini dapat mengambil keuntungan dari struktur grafik klausa tertentu?

Saya hanya menemukan hasil tentang transisi fase yang memuaskan sebagian dalam hal ini, setidaknya dalam pemahaman saya saat ini terbatas. Literatur transisi fase adalah tentang instance k-SAT acak , tetapi apakah itu benar-benar menjelaskan apa pun tentang instance dunia nyata? Saya tidak berharap contoh dunia nyata SAT terlihat seperti contoh acak; Haruskah saya? Apakah ada alasan untuk berpikir transisi fase memberi tahu kita sesuatu, bahkan secara intuitif, tentang contoh dunia nyata bahkan jika mereka tidak terlihat seperti contoh acak?

Pertanyaan terkait yang membantu, tetapi tidak sepenuhnya menjawab pertanyaan saya, khususnya permintaan untuk menyatukan berbagai hal menjadi gambaran yang koheren:

• Mengapa ada perbedaan besar antara pemecah SAT?

• Masalah SAT mana yang mudah?

• Apa korelasi antara treewidth dan contoh kekerasan dari 3SAT acak?

Saya mengasumsikan bahwa Anda merujuk pada solver CDCL SAT pada set data benchmark seperti yang digunakan dalam Kompetisi SAT . Program-program ini didasarkan pada banyak heuristik dan banyak optimasi. Ada beberapa pengantar yang sangat baik tentang bagaimana mereka bekerja di Yayasan Teoritis dari lokakarya Pemecahan SAT Terapan di Banff pada tahun 2014 ( video ).

Algoritma ini didasarkan pada algoritma backtracking DPLL yang mencoba untuk menemukan tugas yang memuaskan dengan menetapkan nilai ke variabel dan backtracks ketika menemukan konflik. Orang-orang telah melihat seberapa besar dampak heuristik ini. Misalnya lihat

• Hadi Katebi, Karem A. Sakallah, dan Joao P. Marques-Silva, " Studi Empiris tentang Anatomi Pemecah Sat Modern ", 2011

Tampaknya efisiensi pemecah SAT ini pada tolok ukur terutama berasal dari dua dua heuristik (dan variannya):

1. VSIDS heuristic fir memilih variabel mana yang akan di-branch berikutnya.
2. CDCL: Heuristik klausa pembelajaran yang didorong konflik yang mempelajari klausa baru dari suatu konflik.

Sudah diketahui bahwa bukti DPLL sesuai dengan bukti dalam resolusi. Tanpa CDCL satu-satunya bukti resolusi yang bisa kita dapatkan adalah bukti resolusi pohon yang jauh lebih lemah daripada bukti resolusi umum.

Ada hasil yang menunjukkan dengan CDCL kita bisa mendapatkan bukti resolusi umum. Namun ada peringatan, mereka membutuhkan banyak restart buatan, percabangan buatan, dan / atau preprocessing tertentu, sehingga tidak jelas seberapa dekat ini dengan apa yang dilakukan program-program ini dalam praktek. Lihat misalnya makalah berikut untuk detail lebih lanjut:

• Paul Beame dan Ashish Sabharwal, " Solver SAT Non-Restarting dengan Preprocessing Sederhana Dapat Mensimulasikan Resolusi Secara Efisien ", 2014

CDCL pada dasarnya memotong cabang dari ruang pencarian. Ada berbagai cara untuk memperoleh klausa baru yang dipelajari dari suatu konflik. Idealnya kita akan menambahkan satu set klausa minimal yang menyiratkan konflik, tetapi dalam praktiknya bisa besar dan bisa mahal untuk dihitung. Pemecah SAT terbaik sering menghapus klausa yang dipelajari secara teratur dan itu membantu dalam praktik.

VSIDS heuristik lainnya pada dasarnya mempertahankan skor untuk setiap variabel. Setiap kali ada konflik, semua skor disesuaikan dengan mengalikannya dengan nilai <1 dan menambahkan konstanta pada yang "terlibat" dalam konflik. Untuk melihat apa artinya ini pikirkan tentang urutan yang merupakan 1 jika variabel v "terlibat" dalam konflik ke- . Biarkan menjadi konstanta tetap. Nilai variabel pada waktu adalah: F ( v , i ) i 0 < α < 1 v n ∑ i < n F ( v , i ) α ( n - i $\alpha$$F(v,i)$$i$$0<\alpha<1$$v$$n$

Secara intuitif orang dapat mengatakan bahwa ini mencoba untuk menekankan variabel yang secara konsisten terlibat dalam konflik baru-baru ini. Anda juga dapat menganggapnya sebagai cara yang sederhana namun sangat murah untuk memprediksi variabel mana yang akan terlibat dalam konflik berikutnya. Jadi VSIDS bercabang pertama pada variabel-variabel tersebut. Satu dapat mengklaim bahwa algoritma pada dasarnya adalah algoritma gagal-cepat, menemukan konflik dengan cepat. Cepat terkait dengan sejumlah variabel yang lebih kecil, yang berarti memblokir sub pohon besar dari pohon pencarian. Tapi ini sebagian besar intuisi, afaik tidak ada yang memformalkannya dengan sangat hati-hati untuk mengujinya pada set data SAT. Menjalankan solver SAT pada salah satu set data ini tidak murah, apalagi membandingkannya dengan keputusan yang optimal (ekstensi terkecil dari penugasan saat ini ke variabel yang akan melanggar salah satu klausa). VSIDS juga tergantung pada variabel mana yang kita bentur karena setiap konflik, ada berbagai cara untuk menentukan kapan suatu variabel terlibat dalam konflik.

Ada hasil yang menunjukkan implementasi tertentu dari ide-ide ini sesuai dengan sentralitas tertimbang waktu dalam grafik dinamis.

Ada juga saran yang mengecualikan contoh permusuhan seperti yang didasarkan pada masalah NP-hard dan primitif kripto dan contoh acak (yang solver CDCL SAT tidak pandai) sisa contoh berasal dari hal-hal yang terstruktur dengan sangat baik seperti perangkat lunak dan verifikasi perangkat keras dan entah bagaimana ini struktur dieksploitasi oleh pemecah SAT CDCL (banyak ide telah disebutkan seperti pintu belakang, variabel beku, dll) tetapi afaik mereka kebanyakan ide dan tidak kuat bukti teoritis atau eksperimental untuk mendukung mereka. Saya pikir orang harus dengan tegas mendefinisikan dengan benar dan menunjukkan bahwa contoh-contoh di mana algoritma ini bekerja dengan baik memiliki properti dan kemudian menunjukkan bahwa algoritma ini mengeksploitasi properti tersebut.

Beberapa orang tetap bersikeras bahwa rasio dan ambang klausa adalah satu-satunya permainan di kota. Itu pasti salah karena siapa pun yang sedikit akrab dengan cara kerja pemecah SAT industri atau memiliki pengetahuan tentang kompleksitas bukti akan tahu. Ada banyak hal yang membuat pemecah SAT bekerja dengan baik atau tidak pada contoh dalam praktek dan rasio klausa hanyalah salah satu hal yang mungkin terlibat. Saya pikir survei berikut ini adalah titik awal yang baik untuk belajar tentang hubungan antara kompleksitas bukti dan pemecah SAT dan perspektif:

• Jakob Nordstrom, " Pada Interaksi Antara Kompleksitas Bukti dan Pemecahan SAT ", 2015

Menariknya bahkan fenomena ambang batas lebih rumit daripada yang dipikirkan kebanyakan orang, Moshe Vardi menyatakan dalam ceramahnya " Transisi fase dan kompleksitas komputasi " bahwa median waktu berjalan GRASP tetap eksponensial untuk rumus 3SAT acak setelah ambang tetapi eksponen menurun (afaik, tidak jelas seberapa cepat berkurang).

Mengapa kita mempelajari pemecah SAT (sebagai ahli teori kompleksitas)? Saya pikir jawabannya sama dengan algoritma lainnya: 1. membandingkannya, 2. menemukan keterbatasannya, 3. merancang yang lebih baik, 4. menjawab pertanyaan mendasar dari teori kompleksitas.

Ketika memodelkan heuristik, kita sering mengganti heuristik dengan nondeterminisme. Pertanyaannya kemudian menjadi apakah itu pengganti "adil"? Dan di sini maksud saya seberapa dekat model dalam membantu kita menjawab pertanyaan di atas.

Ketika kita memodelkan pemecah SAT sebagai sistem bukti, kita sebagian menunjukkan batasannya karena algoritme tidak efisien untuk pernyataan yang memiliki batas lebih rendah dalam sistem bukti. Tetapi masih ada celah antara apa yang sebenarnya ditemukan oleh algoritma dan bukti optimal dalam sistem bukti. Jadi kita perlu menunjukkan bahwa sebaliknya juga, yaitu algoritma dapat menemukan bukti yang sama baiknya dengan yang ada di sistem bukti. Kami tidak dekat untuk menjawab pertanyaan itu, tetapi jumlah heuristik yang digantikan oleh non-determinisme menentukan seberapa dekat model tersebut dengan sistem bukti. Saya tidak berharap bahwa kita sepenuhnya menjatuhkan penggantian heuristik dengan nondeterminisme, jika tidak kita akan mendapatkan hasil automatizability yang memiliki konsekuensi pada masalah terbuka di crypto, dll.

Jadi pertanyaan ketika melihat model menjadi: berapa banyak model membantu menjelaskan mengapa SAT solver A lebih baik daripada SAT solver B? Seberapa membantu mereka dalam mengembangkan pemecah SAT yang lebih baik? Apakah pemecah SAT menemukan bukti dalam praktik yang dekat dengan bukti optimal dalam model? ... Kita juga perlu memodelkan contoh-contoh praktis.

Mengenai intuisi bahwa pemecah CDCL SAT "mengeksploitasi struktur instance praktis" (apa pun struktur itu) intuisi yang diterima secara umum, saya pikir. Pertanyaan sebenarnya adalah memberikan penjelasan yang meyakinkan tentang apa artinya dan menunjukkan bahwa itu memang benar.

Lihat juga jawaban Jakob Nordstrom sendiri untuk perkembangan terkini.

Saya mengetik ini dengan cepat karena kendala waktu yang parah (dan bahkan tidak bisa merespons lebih awal karena alasan yang sama), tetapi saya pikir saya akan mencoba setidaknya ikut campur dengan dua sen saya.

Saya pikir ini adalah pertanyaan yang sangat hebat, dan telah menghabiskan banyak waktu selama beberapa tahun terakhir untuk menyelidiki hal ini. (Pengungkapan penuh: Saya telah menerima sebagian besar dana saya saat ini secara tepat untuk mencoba menemukan jawaban atas pertanyaan-pertanyaan jenis ini, dan kemudian berpotensi untuk mengubah wawasan yang lebih dalam menjadi SAT menjadi pemecah SAT yang lebih efisien.)

Jika seseorang harus memberikan jawaban satu kalimat, maka saya pikir

tidak ada yang benar-benar tahu dan ini adalah bidang penelitian aktif

cukup bagus. Kecuali bahwa ada lebih banyak ruang untuk lebih banyak aktivitas, terutama dari sisi teori.

Beberapa penjelasan yang diajukan (tidak saling terpisah), yang telah dibahas dalam jawaban dan komentar lain, adalah

• (a) pintu belakang,
• (B) pertimbangan kompleksitas parameter,
• (c) struktur grafik masalah CNF,
• (d) pertimbangan kompleksitas bukti, dan
• (e) transisi fase.

Mulai dari akhir (e), tampaknya ada beberapa kebingungan tentang transisi fase. Jawaban singkat di sini adalah bahwa tidak ada alasan apa pun untuk percaya bahwa rasio klausa terhadap variabel relevan untuk masalah yang diterapkan atau masalah kombinatorial teoretis (alias instance buatan). Tetapi untuk beberapa alasan itu adalah kesalahpahaman yang tidak terlalu umum di bagian yang diterapkan dari komunitas SAT bahwa rasio klausa-ke-variabel entah bagaimana harus menjadi ukuran yang relevan secara umum. Rasio klausa terhadap variabel sangat relevan untuk k-SAT acak, tetapi tidak untuk model lain.

Perasaan saya adalah bahwa pintu belakang (a) telah menjadi penjelasan yang populer, tetapi saya pribadi belum benar-benar melihat bukti yang meyakinkan bahwa itu menjelaskan apa yang terjadi dalam praktik.

Kompleksitas parameter (b) memberikan teori yang indah tentang beberapa aspek SAT, dan hipotesis yang sangat menarik adalah bahwa instance SAT mudah karena mereka cenderung "dekat dengan beberapa pulau traktabilitas." Saya pikir hipotesis ini membuka banyak arah penelitian yang menarik. Seperti disebutkan dalam beberapa jawaban, ada banyak koneksi antara (a) dan (b). Namun, sejauh ini saya tidak benar-benar melihat bukti bahwa kompleksitas parameter berkorelasi terlalu banyak dengan apa yang terjadi dalam praktik. Secara khusus, tampaknya contoh yang dapat ditelusuri bisa sangat, sangat sulit dalam prakteknya, dan contoh tanpa backdoor kecil masih bisa sangat mudah.

Penjelasan yang tampaknya paling dapat dipercaya bagi saya untuk contoh industri adalah (c), yaitu bahwa (grafik) struktur formula CNF yang bersangkutan harus dikorelasikan dengan kinerja SAT praktis. Idenya di sini adalah bahwa variabel dan klausa contoh industri dapat dikelompokkan ke dalam komunitas yang terhubung dengan baik dengan beberapa koneksi di antara, dan bahwa pemecah SAT entah bagaimana mengeksploitasi struktur ini. Sayangnya, tampaknya cukup sulit untuk menjabarkan ini dengan lebih teliti, dan sama-sama sayangnya daerah ini menderita hype yang cukup banyak. Penjelasan yang diajukan yang saya lihat sejauh ini di makalah cukup tidak memuaskan dan modelnya sepertinya mudah untuk ditembak jatuh. Masalahnya adalah jika seseorang benar-benar ingin melakukan ini secara menyeluruh, kemudian matematika menjadi sangat sulit (karena itu adalah masalah yang sulit) dan juga menjadi sangat berantakan (karena Anda perlu model Anda menjadi cukup dekat dengan kenyataan untuk mendapatkan hasil yang relevan). Secara khusus, makalah yang saya lihat menjelaskan bahwa kinerja VSIDS (variabel state decaying sum) jumlah heuristik untuk pilihan variabel bekerja dengan baik karena mengeksplorasi komunitas dalam grafik representasi contoh cukup tidak meyakinkan, meskipun hipotesis seperti itu masih sangat menarik.

Satu jalur penelitian yang saya lakukan secara pribadi adalah apakah kinerja SAT praktis entah bagaimana berkorelasi dengan ukuran kompleksitas bukti dari formula CNF yang dimaksud. Sayangnya, jawaban singkatnya adalah tidak ada koneksi yang jelas dan meyakinkan. Mungkin masih ada korelasi nontrivial (ini adalah sesuatu yang saat ini kami selidiki dengan cara yang berbeda), tetapi tampaknya teori terlalu bagus dan bersih dan cantik dan kenyataan terlalu berantakan untuk ada pertandingan yang benar-benar bagus. (Mengenai makalah yang Terkait Tindakan Kompleksitas Bukti dan Kekerasan Praktis SAToleh Järvisalo, Matsliah, Nordström, dan Živný di CP '12 ternyata eksperimen yang lebih detail memberikan gambaran yang jauh lebih kompleks dengan kesimpulan yang kurang jelas --- kami berharap dapat membaca versi jurnal lengkap tentang hal ini setiap dekade sekarang, tapi itu rumit, meskipun semoga tetap menarik.)

Garis pekerjaan lain yang terkait dalam kompleksitas bukti adalah memodelkan pemecah SAT canggih sebagai sistem pembuktian dan membuktikan teorema dalam model ini untuk menyimpulkan sifat-sifat pemecah yang sesuai. Ini adalah sedikit ladang ranjau, meskipun, dalam pilihan desain yang kecil dan tampaknya tidak berbahaya pada sisi model teoretis dapat menyebabkan hasil yang sangat tidak relevan dari sudut pandang praktis. Di sisi lain, jika seseorang menginginkan model teoretis yang cukup dekat dengan kenyataan untuk memberikan hasil yang relevan, maka model ini menjadi sangat berantakan. (Ini karena kinerja pemecah SAT tergantung pada sejarah global dari segala sesuatu yang telah terjadi sejauh ini dalam cara nontrivial, dan ini berarti model tidak dapat modular dalam cara kita biasanya mengatur sistem bukti kami --- apakah langkah derivasi tertentu adalah "benar"

Dua makalah yang benar-benar harus disebutkan sebagai pengecualian untuk ini, adalah [Pipatsrisawat dan Darwiche 2011] dan [Atserias, Fichte dan Thurley 2011], di mana ditunjukkan bahwa pembelajaran klausa yang digerakkan oleh konflik, pemecah SAT yang dimodelkan dengan cara alami memiliki berpotensi mensimulasikan secara polinomi penuh, resolusi umum. Ada daftar makalah yang cukup panjang sebelum [PD11] dan [AFT11] yang pada dasarnya mengklaim hasil yang sama, tetapi mereka semua memiliki masalah serius dengan pemodelan. (Memang benar bahwa [PD11] dan [AFT11] juga memerlukan beberapa asumsi untuk bekerja, tetapi mereka cukup banyak yang minimal yang Anda harapkan kecuali Anda meminta makalah yang juga akan menunjukkan bahwa hierarki kompleksitas parameterisasi runtuh.)

Sekali lagi, saya menulis semua ini dengan sangat cepat, tetapi jika ada minat yang substansial untuk hal-hal di atas, saya dapat mencoba menguraikan (walaupun mungkin perlu beberapa saat untuk kembali ke ini lagi --- jangan ragu untuk ping saya jika ada adalah apapun yang Anda ingin saya komentari). Sebagai cara cepat untuk memberikan referensi, izinkan saya melakukan beberapa plug-up tanpa malu-malu (walaupun rasa malu agak berkurang ketika saya melihat bahwa beberapa komentar juga mengutip beberapa referensi ini):

Pembicaraan gaya tutorial Pada Interaksi Antara Kompleksitas Bukti dan Pemecahan SAT yang diberikan di International Summer School on Satisfiability, Satisfiability Modulo Theories, dan Automated Reasoning pada tahun 2016 dengan banyak referensi lengkap di akhir slide: http://www.csc .kth.se / ~ jakobn / research / TalkInterplaySummerSchool2016.pdf

Pembicaraan survei yang sedikit lebih baru, dan lebih singkat, Memahami SAT yang Didorong oleh Konflik melalui Lensa Kompleksitas Bukti dari awal 2017 (juga dengan referensi lengkap di bagian akhir): http://www.csc.kth.se/~jakobn/research /TalkProofComplexityLensCDCL1702.pdf

Survei koneksi antara kompleksitas bukti dan penyelesaian SAT: http://www.csc.kth.se/~jakobn/research/InterplayProofCplxSAT.pdf [Referensi bibliografi: Jakob Nordström. Tentang Interaksi Antara Kompleksitas Bukti dan Pemecahan SAT. ACM SIGLOG News, volume 2, nomor 3, halaman 19-44, Juli 2015. (Versi yang diedit ringan dengan beberapa kesalahan ketik diperbaiki.)]

Makalah SAT '16 dengan CDCL dimodelkan dengan setia sebagai sistem bukti: http://www.csc.kth.se/~jakobn/research/Trade-offsTimeMemoryModelCDCL_SAT.pdf [Referensi bibliografi: Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard , Jakob Nordström, dan Marc Vinyals. Pertukaran antara Waktu dan Memori dalam Model yang Lebih Ketat dari Pemecah SAT CDCL. Dalam Prosiding Konferensi Internasional ke-19 tentang Teori dan Aplikasi Pengujian Kepuasan (SAT '16), Catatan Kuliah dalam Ilmu Komputer, volume 9710, halaman 160-176, Juli 2016.]

Biarkan saya menambahkan dua sen pemahaman saya untuk ini, meskipun saya belum pernah benar-benar bekerja di daerah tersebut.

Anda mengajukan satu dari dua pertanyaan, "apa saja pendekatan yang dikenal untuk membuktikan efisiensi teoretis dari beberapa pemecah SAT untuk beberapa jenis contoh" dan "mengapa pemecah SAT efisien dalam kenyataannya".

Untuk pertanyaan sebelumnya, saya hanya akan mengarahkan Anda ke penelitian Stefan Szeider. Menurut saya, dia adalah area yang paling aktif saat ini dalam topik backdoors dan parameterisasi FPT SAT (yang mencakup kedua pendekatan struktural seperti langkah-langkah berjenis treewidth dan apa yang disebut set pintu belakang, serta beberapa campuran keduanya).

Untuk pertanyaan yang terakhir, sejujurnya, pertanyaan yang tepat telah diperdebatkan di setiap lokakarya penyelesaian SAT yang saya hadiri (termasuk beberapa tahun terakhir), jadi itu bukan masalah yang diselesaikan. Tapi kesan saya adalah sebagai berikut.

Pertama-tama, Anda perlu mengukur atau membatasi apa yang Anda maksud dengan "pada kenyataannya". Tidak benar bahwa pemecah SAT adalah pemecah universal yang baik untuk setiap masalah yang Anda lemparkan (tentu saja), dan di antara berbagai masalah Anda akhirnya membutuhkan strategi yang berbeda. Sebagai contoh, ada beberapa keberhasilan baru-baru ini di mana dugaan matematika telah diverifikasi atau diperketat oleh pencarian komputer besar yang dibantu oleh pemecah SAT. Dalam kasus ini, tampaknya, sering kali peningkatan gaya cerdik CDC dan heuristik yang biasanya digunakan oleh pemecah SAT modern tidak benar-benar membelikan Anda terlalu banyak daya, dan gim ini bermuara pada cara cerdas untuk membagi masalah sumber Anda menjadi bagian, diikuti oleh (pada dasarnya) algoritma percabangan brute-force dengan faktor konstan kecil dalam waktu berjalan.

Saya mungkin sedikit melebih-lebihkan poin ini, tetapi poin saya adalah, ketika pemecah SAT menyerang misalnya Erdos Discrepancy Conjecture, mereka berhasil karena alasan yang berbeda daripada ketika mereka memecahkan contoh industri yang berasal dari pengujian sirkuit.

Jadi kita harus bertanya, mengapa solver berbasis CDCL bekerja sangat baik pada contoh industri, misalnya, verifikasi sirkuit (pengujian kesetaraan sirkuit)? Saya pikirbahwa pandangan yang paling kuat (atau pandangan konsensus) di sini adalah strategi pencarian dari pemecah CDCL sangat baik dengan struktur instance ini. Ini berarti, misalnya, bahwa sirkuit terdiri dari bagian-bagian yang relatif kompleks (menyebutnya cluster), saling berhubungan dengan koneksi yang relatif lebih sedikit dan lebih sederhana, mungkin secara hierarkis; dan bahwa pemecah CDCL dengan semua heuristiknya sangat bagus dalam (de facto) mengeksploitasi ini dan "memproyeksikan" kluster-kluster ini ke variabel-variabel bersama, dengan cara atau urutan apa pun yang paling berguna untuk memverifikasi rangkaian yang ada. Tetapi tampaknya juga masih menjadi pandangan konsensus bahwa ini adalah penjelasan yang tidak mencukupi (misalnya, kita mungkin tidak dapat secara teoritis menjelaskan efisiensi pemecah CDCL SAT dalam domain ini murni dengan merujuk pada struktur grafik dari instance).

Jadi apakah parameterisasi yang dapat ditelusuri berjalan menuju menjelaskan yang terakhir? Sejujurnya, saya tidak tahu. Saya pikir mungkin ada efek yang kuat dalam permainan yang contoh dunia nyata bukan kasus terburuk, juga tidak (mungkin) benar-benar kasus rata-rata berdasarkan distribusi contoh apa pun yang dapat kami tangani. Tapi mungkin masih layak ditanyakan.

Ada sebuah makalah " Menghubungkan Ukuran Kompleksitas Bukti dan Kekerasan Praktis dari SAT " oleh Matti Järvisalo, Arie Matsliah, Jakob Nordström, dan Stanislav Živný di CP '12 yang berupaya menghubungkan kekerasan atau kemudahan menyelesaikan formula tertentu dengan pemecah CDCL dengan bukti resolusi. langkah-langkah kompleksitas, khususnya ruang bukti resolusi. Hasilnya agak campur aduk, tapi saya rasa ini adalah langkah ke arah yang benar.

Saya bukan ahli dalam bidang ini, tetapi saya pikir hal-hal transisi SAT / fase acak kurang lebih sama sekali tidak terkait dengan hal-hal aplikasi industri / praktis.

Misalnya, solver yang sangat baik untuk instance acak (seperti https://www.gableske.net/dimetheus ) didasarkan pada metode fisika statistik (penyebaran kepercayaan, dll.) Saya percaya, sedangkan solver 'umum' yang sangat bagus (seperti sebagai http://fmv.jku.at/lingeling/ ) menggunakan teknik yang tidak terkait (lebih seperti apa yang Kaveh bicarakan) saya percaya.

Tetapi, seperti yang saya katakan, mungkin tidak mengambil kata saya untuk itu; ini datang dari non-ahli yang pasti.