Obsługa struktur danych dla lokalnego wyszukiwania SAT

WalkSAT i GSAT są dobrze znanymi i prostymi lokalnymi algorytmami wyszukiwania służącymi do rozwiązania logicznego problemu satysfakcji. Pseudokod algorytmu GSAT jest kopiowany z pytania Implementacja algorytmu GSAT - Jak wybrać literał, który ma być odwrócony? i przedstawione poniżej.

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

Tutaj odwracamy zmienną, która maksymalizuje liczbę spełnionych klauzul. Jak to zrobić skutecznie? Naiwną metodą jest przerzucanie każdej zmiennej i dla każdego kroku przez wszystkie klauzule i obliczanie, ile z nich jest spełnionych. Nawet jeśli można by zapytać o klauzulę w celu uzyskania satysfakcji w stałym czasie, metoda naiwna nadal działałaby w czasie , gdzie jest liczbą zmiennych, a liczbą klauzul. Jestem pewien, że możemy zrobić lepiej, stąd pytanie: $O(VC)$ $V$ $C$

Wiele lokalnych algorytmów wyszukiwania zmienia przypisanie zmiennej, co maksymalizuje liczbę spełnionych klauzul. W praktyce, przy jakich strukturach danych ta operacja jest skutecznie obsługiwana?

Wydaje mi się, że podręczniki często pomijają. Jednym z przykładów jest nawet słynna książka Russella i Norviga .

algorithms data-structures satisfiability

— Juho
źródło

Cóż, ci goście budują to sprzętowo. Najwyraźniej podejścia probabilistyczne i heurystyczne są bardziej popularne; sugerowałoby to, że rzeczywiście nie można szybko wybrać „najlepszej” (w końcu jest to tylko chciwość) zmiennej lub że wybór ten ogólnie nie jest dobry.

— Raphael

@Raphael Może masz rację, że nie można jej wybrać bardzo szybko, ale nie odważyłbym się powiedzieć „wybór ogólnie nie jest dobry”. Może źle zrozumiałem twój punkt widzenia, ale jestem pewien, że wybranie „właściwej” zmiennej ma ogromny wpływ. Dzięki, zagłębię się trochę głębiej. Myślę, że jeden z autorów slajdów, które połączyłeś (Hoos), ma książkę na ten temat.

— Juho,

„Właściwy” byłby optymalny, ale czy istnieje powód, by sądzić, że ten, który maksymalizuje teraz, jest właściwy? W końcu problemu nie rozwiązuje chciwość (kanoniczna).

— Raphael

Potrzebną strukturą danych jest lista wystąpień , lista dla każdej zmiennej zawierająca klauzule, w których występuje zmienna. Listy te są budowane raz, gdy CNF jest czytany po raz pierwszy. Są one używane w krokach 3 i 5 poniżej, aby uniknąć skanowania całej formuły CNF w celu policzenia spełnionych klauzul.

Lepszym algorytmem niż odwracanie każdej zmiennej jest:

Zrób listę tylko zmiennych, które występują w niezadowolonych klauzulach.
Wybierz zmienną z tej listy. $x$
Policz, ile klauzul zawierających jest spełnione. $x$
Odwróć . $x$
Policz, ile klauzul zawierających jest spełnione. $x$
Odepnij . $x$
Odejmij wynik kroku 3 od kroku 5 i zapisz go dla . $x$
Powtórz kroki 2-7 dla pozostałych zmiennych znalezionych w kroku 1.
Odwróć zmienną o największej liczbie zarejestrowanej w kroku 7.

Odniesieniem do struktury danych (często znanej również jako lista sąsiedztwa) jest na przykład Lynce i Marques-Silva, Efficient Data Structures for Backtracking SAT solvers, 2004.

— Kyle Jones
źródło