Mengukur tingkat kesulitan SAT

Diberikan instance dari SAT, saya ingin dapat memperkirakan seberapa sulitnya untuk menyelesaikan instance.

Salah satu caranya adalah dengan menjalankan solver yang ada, tetapi jenis itu mengalahkan tujuan memperkirakan kesulitan. Cara kedua mungkin mencari rasio klausa terhadap variabel, seperti yang dilakukan untuk transisi fase secara acak-SAT, tapi saya yakin metode yang lebih baik ada.

Diberikan contoh SAT, apakah ada heuristik cepat untuk mengukur kesulitan? Satu-satunya syarat adalah heuristik ini lebih cepat daripada menjalankan solver SAT yang ada saat ini.

Pertanyaan terkait

Masalah SAT mana yang mudah? di cstheory.SE. Pertanyaan ini menanyakan tentang set instance yang bisa ditelusuri. Ini adalah pertanyaan yang serupa, tetapi tidak persis sama. Saya benar-benar tertarik pada heuristik yang memberikan satu instance, membuat semacam dugaan semi-cerdas jika instance tersebut akan menjadi sulit untuk dipecahkan.

Secara umum, ini adalah pertanyaan penelitian yang sangat relevan dan menarik. "Salah satu caranya adalah menjalankan solver yang ada ..." dan apa yang akan dikatakan oleh kita sebenarnya? Kita bisa melihat secara empiris bahwa sebuah instance tampak sulit untuk solver tertentu atau algoritma / heuristik tertentu, tetapi apa yang sebenarnya dikatakannya tentang kekerasan instance tersebut?

Salah satu cara yang telah ditempuh adalah identifikasi berbagai sifat struktural dari instance yang mengarah pada algoritma yang efisien. Properti ini memang lebih disukai untuk "mudah" diidentifikasi. Contohnya adalah topologi grafik kendala yang mendasarinya, diukur menggunakan berbagai parameter lebar grafik. Sebagai contoh diketahui bahwa sebuah instance dapat dipecahkan dalam waktu polinomial jika treewidth dari grafik kendala yang mendasarinya dibatasi oleh konstanta.

Pendekatan lain difokuskan pada peran struktur tersembunyi dari instance. Salah satu contoh adalah set backdoor , yang berarti set variabel sehingga ketika mereka dipakai, masalah yang tersisa menyederhanakan ke kelas yang bisa ditelusur. Sebagai contoh, Williams et al., 2003 [1] menunjukkan bahwa bahkan ketika memperhitungkan biaya untuk mencari variabel backdoor, seseorang masih dapat memperoleh keuntungan komputasi secara keseluruhan dengan berfokus pada set backdoor, asalkan set tersebut cukup kecil. Lebih lanjut, Dilkina et al., 2007 [2] mencatat bahwa seorang pemecah masalah yang disebut Satz-Rand sangat pandai dalam menemukan jalan belakang kecil yang kuat pada berbagai domain eksperimental.

Baru-baru ini, Ansotegui et al., 2008 [3] mengusulkan penggunaan kompleksitas ruang seperti pohon sebagai ukuran untuk pemecah berbasis DPLL. Mereka membuktikan bahwa juga ruang yang dibatasi konstan menyiratkan adanya algoritma keputusan waktu polinomial dengan ruang menjadi derajat polinomial (Teorema 6 dalam makalah). Selain itu, mereka menunjukkan ruang lebih kecil dari ukuran siklus-potongan. Bahkan, berdasarkan asumsi tertentu, ruang juga lebih kecil dari ukuran backdoors.

Mereka juga memformalkan apa yang saya pikir Anda cari, yaitu:

$\psi$$\Gamma$$O(n^{\psi ( \Gamma )})$

[1] Williams, Ryan, Carla P. Gomes, dan Bart Selman. "Kembali ke kompleksitas kasus yang khas." Konferensi Bersama Internasional tentang Kecerdasan Buatan. Vol. 18, 2003.

[2] Dilkina, Bistra, Carla Gomes, dan Ashish Sabharwal. "Pengorbanan dalam Kompleksitas Deteksi Pintu Belakang." Prinsip dan Praktek Pemrograman Kendala (CP 2007), hlm. 256-270, 2007.

[3] Ansótegui, Carlos, Maria Luisa Bonet, Jordi Levy, dan Felip Manya. "Mengukur Kekerasan Mesin Virtual SAT." Dalam Prosiding Konferensi Nasional ke 23 tentang Kecerdasan Buatan (AAAI'08), hlm. 222-228, 2008.

Karena Anda tahu tentang transisi fase, izinkan saya untuk menyebutkan beberapa pemeriksaan sederhana lain yang saya ketahui (yang kemungkinan dimasukkan oleh analisis grafik kendala):

• Beberapa generator SAT acak awal secara tidak sengaja membuat sebagian besar rumus mudah karena mereka menggunakan "kepadatan konstan", yang berarti proporsi yang hampir sama dari semua panjang klausa. Ini sebagian besar mudah karena 2-klausa dan unit menyederhanakan masalah secara signifikan, seperti yang diharapkan, dan klausa yang sangat panjang tidak menambah banyak percabangan atau memfasilitasi hiper-resolusi lebih baik. Jadi, sepertinya lebih baik untuk tetap dengan klausa panjang tetap dan memvariasikan parameter lainnya.
• $|x|*|\lnot x|$$x$
• $v_1, v_2, v_3$$\{v_1, v_2, ...\}, \{v_2, v_3, ...\}, \{v_1, v_3, ...\}$

[1] https://arxiv.org/pdf/1903.03592.pdf

Di atas jawaban yang sangat baik dari Juho, berikut adalah pendekatan lain:

Ercsey-Ravasz & Toroczkai, Optimasi hardness sebagai transient chaos dalam pendekatan analog terhadap kendala constraint , Nature Physics volume 7, halaman 966-970 (2011).

Pendekatan ini adalah untuk menulis ulang masalah SAT menjadi sistem dinamis, di mana setiap penarik sistem adalah solusi untuk masalah SAT. Baskom tarik sistem lebih fraktal karena masalahnya menjadi lebih sulit, dan "kesulitan" dari contoh SAT dapat diukur dengan memeriksa seberapa kacau transien sebelum sistem bertemu.

Dalam praktiknya, ini berarti memulai sekelompok pemecah dari posisi awal yang berbeda dan memeriksa tingkat di mana pemecah lolos dari transien yang kacau sebelum mereka tiba di suatu penarik.

Tidak sulit untuk menghasilkan sistem dinamis yang "solusi" -nya adalah solusi untuk masalah SAT yang diberikan, tetapi sedikit lebih sulit untuk memastikan bahwa semua solusi adalah penarik dan bukan penolak. Solusi mereka adalah memperkenalkan variabel energi (mirip dengan pengganda Lagrange) untuk mewakili seberapa parah suatu kendala dilanggar, dan mencoba membuat sistem untuk meminimalkan energi sistem.

Menariknya, menggunakan sistem dinamis mereka, Anda dapat memecahkan masalah SAT dalam waktu polinomial pada komputer analog, yang dengan sendirinya merupakan hasil yang luar biasa. Ada tangkapan; mungkin memerlukan voltase besar secara eksponensial untuk mewakili variabel energi, jadi sayangnya Anda tidak dapat menyadarinya pada perangkat keras fisik.