Mendukung struktur data untuk pencarian lokal SAT

20

WalkSAT dan GSAT adalah algoritma pencarian lokal yang terkenal dan sederhana untuk memecahkan masalah kepuasan Boolean. Pseudocode untuk algoritma GSAT disalin dari pertanyaan Menerapkan algoritma GSAT - Bagaimana memilih literal mana yang akan dibalik? dan disajikan di bawah ini.

procedure GSAT(A,Max_Tries,Max_Flips)
  A: is a CNF formula
  for i:=1 to Max_Tries do
    S <- instantiation of variables
    for j:=1 to Max_Iter do
      if A satisfiable by S then
        return S
      endif
      V <- the variable whose flip yield the most important raise in the number of satisfied clauses;
      S <- S with V flipped;
    endfor
  endfor
  return the best instantiation found
end GSAT

Di sini kita membalik variabel yang memaksimalkan jumlah klausa yang puas. Bagaimana ini dilakukan secara efisien? Metode naif adalah membalik setiap variabel, dan untuk setiap langkah melalui semua klausa dan menghitung berapa banyak dari mereka yang puas. Bahkan jika suatu klausa dapat ditanyakan untuk kepuasan dalam waktu konstan, metode naif akan tetap berjalan dalam waktu , di mana adalah jumlah variabel dan jumlah klausa. Saya yakin kita bisa melakukan yang lebih baik, maka pertanyaannya:HAI(VC)VC

Banyak algoritma pencarian lokal membalik tugas variabel yang memaksimalkan jumlah klausa yang puas. Dalam praktiknya, dengan struktur data apa operasi ini didukung secara efisien?

Ini adalah sesuatu yang saya rasa seperti buku teks yang sering kali dihilangkan. Salah satu contohnya adalah buku Russell & Norvig yang terkenal .

algorithms data-structures satisfiability Juho
sumber
Nah, orang-orang ini membangunnya di perangkat keras. Rupanya , pendekatan probabilistik dan heuristik lebih populer; yang akan menyarankan bahwa Anda memang tidak dapat memilih variabel "terbaik" (hanya serakah, setelah semua) dengan cepat, atau bahwa pilihan ini tidak baik secara umum.
Raphael
@ Raphael Mungkin Anda benar bahwa seseorang tidak dapat memilih dengan sangat cepat, tetapi saya tidak akan berani mengatakan "pilihannya tidak baik secara umum". Mungkin saya salah mengerti maksud Anda, tetapi saya cukup yakin memilih variabel "benar" memiliki dampak besar. Terima kasih, saya akan menggali sedikit lebih dalam. Saya pikir salah satu penulis slide yang Anda tautkan (Hoos) memiliki buku tentang subjek tersebut.
Juho
Yang "benar" akan optimal, tetapi adakah alasan untuk percaya bahwa yang memaksimalkan sekarang adalah yang benar? Bagaimanapun, masalahnya tidak bisa dipecahkan oleh keserakahan (kanonik).
Raphael

Jawaban:

9

Struktur data yang dibutuhkan adalah daftar kejadian , daftar untuk setiap variabel yang berisi klausa tempat variabel masuk Daftar ini dibangun sekali, ketika CNF pertama kali dibaca. Mereka digunakan dalam langkah 3 dan 5 di bawah ini untuk menghindari pemindaian seluruh rumus CNF untuk menghitung klausa yang puas.

Algoritma yang lebih baik daripada membalik setiap variabel adalah:

  1. Buat daftar hanya variabel yang muncul di klausa yang tidak puas.
  2. Pilih variabel dari daftar ini.x
  3. Hitung berapa banyak klausa yang berisi dipenuhi.x
  4. Balik .x
  5. Hitung berapa banyak klausa yang berisi dipenuhi.x
  6. Batalkan .x
  7. Kurangi hasil langkah 3 dari langkah 5 dan catat untuk .x
  8. Ulangi langkah 2-7 untuk variabel-variabel lainnya yang ditemukan pada langkah 1.
  9. Balikkan variabel dengan angka tertinggi yang dicatat pada langkah 7.

Referensi untuk struktur data (sering juga dikenal sebagai daftar adjacency) adalah sebagai contoh Lynce dan Marques-Silva, Struktur Data yang Efisien untuk Backtracking SAT solver, 2004.

Kyle Jones
sumber