Unterstützende Datenstrukturen für die lokale SAT-Suche

WalkSAT und GSAT sind bekannte und einfache lokale Suchalgorithmen zur Lösung des Problems der booleschen Erfüllbarkeit. Der Pseudocode für den GSAT-Algorithmus wird aus der Frage Implementieren des GSAT-Algorithmus kopiert. Wie wird ausgewählt, welches Literal umgedreht werden soll? und unten dargestellt.

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

Hier drehen wir die Variable, die die Anzahl der erfüllten Klauseln maximiert. Wie geht das effizient? Die naive Methode besteht darin, jede Variable und für jeden Schritt durch alle Klauseln zu drehen und zu berechnen, wie viele davon erfüllt werden. Selbst wenn eine Klausel in konstanter Zeit auf Erfüllbarkeit abgefragt werden könnte, würde die naive Methode immer noch in der Zeit) ausgeführt, wobei die Anzahl der Variablen und die Anzahl der Klauseln ist. Ich bin sicher, wir können es besser machen, daher die Frage:$O(VC)$$V$$C$

Viele lokale Suchalgorithmen kippen die Zuweisung der Variablen, wodurch die Anzahl der erfüllten Klauseln maximiert wird. Mit welchen Datenstrukturen wird diese Operation in der Praxis effizient unterstützt?

Ich habe das Gefühl, dass Lehrbücher dies oft auslassen. Ein Beispiel ist sogar das berühmte Russell & Norvig-Buch .

Die erforderliche Datenstruktur ist eine Ereignisliste , eine Liste für jede Variable, die die Klauseln enthält, in denen die Variable vorkommt. Diese Listen werden beim ersten Lesen der CNF einmal erstellt. Sie werden in den folgenden Schritten 3 und 5 verwendet, um zu vermeiden, dass die gesamte CNF-Formel durchsucht wird, um erfüllte Klauseln zu zählen.

Ein besserer Algorithmus als das Spiegeln jeder Variablen ist:

1. Erstellen Sie eine Liste nur der Variablen, die in den nicht erfüllten Klauseln vorkommen.
2. Wählen Sie eine Variable aus dieser Liste.$x$
3. Zählen Sie, wie viele Klauseln, die enthalten, erfüllt sind.$x$
4. spiegeln .$x$
5. Zählen Sie, wie viele Klauseln, die enthalten, erfüllt sind.$x$
6. Unflip .$x$
7. Subtrahieren Sie das Ergebnis von Schritt 3 von Schritt 5 und notieren Sie es für .$x$
8. Wiederholen Sie die Schritte 2 bis 7 für die restlichen Variablen in Schritt 1.
9. Klappen Sie die Variable mit der höchsten in Schritt 7 aufgezeichneten Nummer um.

Eine Referenz für die Datenstruktur (häufig auch als Adjazenzliste bezeichnet) sind beispielsweise Lynce und Marques-Silva, Efficient Data Structures for Backtracking SAT Solver, 2004.