Algoritma SAT tidak didasarkan pada DPLL

Jawaban:

21

Pencarian Resolusi (hanya menerapkan aturan resolusi dengan beberapa heuristik yang baik) adalah strategi lain yang mungkin untuk pemecah SAT. Secara teoritis itu secara eksponensial lebih kuat (yaitu ada masalah yang memiliki bukti lebih pendek eksponensial) daripada DPLL (yang hanya melakukan resolusi pohon meskipun Anda dapat menambahnya dengan pembelajaran nogood untuk meningkatkan kekuatannya - apakah itu membuatnya sekuat resolusi umum masih buka sejauh yang saya tahu) tetapi saya tidak tahu implementasi aktual yang berkinerja lebih baik.

Jika Anda tidak membatasi diri untuk menyelesaikan pencarian, maka WalkSat adalah pemecah pencarian lokal yang dapat digunakan untuk menemukan solusi yang memuaskan dan mengungguli pencarian berbasis DPLL dalam banyak kasus. Seseorang tidak dapat menggunakannya untuk membuktikan ketidakpuasan meskipun kecuali satu cache semua tugas yang gagal yang berarti persyaratan memori eksponensial.

Sunting: Lupa menambahkan - Pesawat pemotongan juga dapat digunakan (dengan mengurangi SAT ke program integer). Khususnya pemotongan Gomory cukup untuk menyelesaikan semua program integer ke optimal. Sekali lagi dalam kasus terburuk, nomor eksponensial mungkin diperlukan. Saya pikir buku Komputasi Kompleksitas Arora & Barak memiliki beberapa contoh sistem pembuktian yang secara teori dapat digunakan untuk sesuatu seperti pemecahan SAT. Sekali lagi, saya belum benar-benar melihat implementasi cepat dari apa pun selain metode berbasis pencarian DPLL atau lokal.

Memilih
sumber
9
DPLL dengan pembelajaran klausa (atau nogood learning, demikian Anda menyebutnya) dan restart telah terbukti setara dengan resolusi umum.
Jan Johannsen
1
@JanJohannsen, apakah ini kertas yang Anda rujuk? arxiv.org/abs/1107.0044
Radu GRIGore
5
Ya, ada juga peningkatan dalam makalah berikut: Knot Pipatsrisawat dan Adnan Darwiche. Pada kekuatan pemecah SAT belajar klausa sebagai mesin resolusi. Kecerdasan Buatan 175 (2), 2011, hlm 512-525. dx.doi.org/10.1016/j.artint.2010.10.002
Jan Johannsen
3
Sedangkan makalah karya Beame et al. dihubungkan oleh Radu Grigore menunjukkan bahwa resolusi umum disimulasikan oleh algoritma DPLL dengan strategi pembelajaran artifisial khusus, makalah di atas menunjukkannya untuk strategi pembelajaran alami yang benar-benar digunakan.
Jan Johannsen
12

Propagasi survei adalah algoritma lain yang telah digunakan dengan sukses pada beberapa jenis masalah SAT, terutama contoh SAT acak. Seperti halnya WalkSAT, ini tidak dapat digunakan untuk membuktikan ketidakpuasan, tetapi didasarkan pada ide yang sangat berbeda (algoritma penyampaian pesan) dari WalkSAT.

Timothy Chow
sumber
10

Ada pemecah SAT berdasarkan pencarian lokal. Lihat, misalnya, makalah ini untuk penjelasan.

ilyaraz
sumber
7

Anda juga bisa mengatakan, bahwa semua pemecah CSP juga pemecah SAT. Dan sejauh yang saya tahu ada dua metode yang digunakan dalam CSP:

  • DFS lengkap dengan pemangkasan ruang pencarian dan memeriksa konsistensi busur, mungkin menggunakan pencukuran untuk memastikan bahwa konsistensi dipertahankan sesegera mungkin.
  • Metode lokal (pencarian tabu, anil simulasi)
malejpavouk
sumber
4

Pencarian Pohon Monte Carlo (MCTS) baru-baru ini mencapai beberapa hasil mengesankan pada permainan seperti Go. Ide dasarnya adalah interleaving simulasi acak dengan pencarian pohon. Ini ringan dan mudah diimplementasikan, halaman hub penelitian yang saya tautkan mengandung banyak contoh, makalah dan beberapa kode juga.

Previti et al. [1] melakukan beberapa penyelidikan awal MCTS yang diterapkan pada SAT. Mereka menyebut algoritma pencarian berbasis MCTS UCTSAT ("batas kepercayaan tertinggi diterapkan pada pohon SAT", jika Anda mau). Mereka membandingkan kinerja DPLL dan UCTSAT pada contoh dari repositori SATLIB, dengan tujuan untuk melihat apakah UCTSAT akan menghasilkan pohon pencarian yang jauh lebih kecil daripada DPLL.

Untuk contoh pewarnaan acak 3-SAT dan grafik datar dengan ukuran berbeda, tidak ada perbedaan signifikan. Namun, UCTSAT berkinerja lebih baik untuk contoh di dunia nyata. Ukuran pohon rata-rata (dalam hal jumlah node) untuk empat instance analisis kesalahan rangkaian SSA yang berbeda ada beberapa ribu untuk DPLL, sementara selalu kurang dari 200 untuk UCTSAT.

[1] Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf, dan Bart Selman. "Pencarian UCT gaya Monte-carlo untuk kepuasan boolean." Dalam AI * IA 2011: Kecerdasan Buatan Sekitar Manusia dan Di Luar, hlm. 177-188. Springer Berlin Heidelberg, 2011.

Juho
sumber
-4

DPLL tidak secara spesifik menentukan pemesanan variabel-kunjungan dan ada banyak penelitian menarik yang melihat strategi serangan pemesanan variabel optimal. beberapa di antaranya dimasukkan ke dalam logika pemilihan variabel dalam algoritma SAT. dalam beberapa hal penelitian ini adalah pendahuluan karena menunjukkan bahwa urutan serangan variabel yang berbeda menyebabkan kendala sekuensial yang berbeda (yang sangat berkorelasi dengan kekerasan misalnya), dan menyusun heuristik atau strategi paling efektif untuk mengeksploitasi wawasan yang tampaknya kunci ini tampaknya menjadi pada tahap awal penelitian.

ay
sumber
4
Apakah Anda mengerti bahwa saya telah meminta algoritma yang tidak didasarkan pada DPLL ?
Anonim
2
Apakah Anda mengerti apa artinya "berbasis" ? Memberitahu Anda : jangan gunakan pertanyaan saya untuk mengomentari apa pun yang Anda ingin komentari!
Anonim
7
Anda sendiri mengatakan mereka berbasis DPLL. bagi saya sepertinya ini seperti mengatakan bahwa aturan pivot yang berbeda untuk simpleks memberi Anda sebuah algoritma yang bukan algoritma simpleks
Sasho Nikolov
7
Saya setuju dengan Sasho. Juga, penelitian tentang heuristik pemesanan variabel pasti tidak dalam tahap awal. Pentingnya telah disadari sejak lama (bayangkan konsekuensi dari ramalan yang sempurna), dan banyak waktu telah dihabiskan untuk menganalisisnya. Heuristik nilai pemesanan menjadi lebih menarik pada pemecah CSP, dan untuk beberapa alasan, saya tidak berpikir penelitian tentang mereka sama boomingnya dengan pemesanan variabel.
Juho
4
Untuk lebih spesifik, penelitian awal tentang heuristik pemesanan variabel kembali ke 70-an. Jika Anda tertarik, saya dapat menggali referensi yang relevan untuk Anda.
Juho