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

Question

Walksat und Gsat sind bekannte und einfache lokale Suchalgorithmen zur Lösung des booleschen Zufriedenheitsproblems. Der Pseudocode für den GSAT -Algorithmus wird aus der Frage kopiert Implementierung des GSAT -Algorithmus - Wie kann ich ausgewählt werden, welches wörtliche zum Flip? und unten präsentiert.

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 zufriedenen Klauseln maximiert. Wie wird das effizient gemacht? Die naive Methode besteht darin, jede Variable und für jeden Schritt durch alle Klauseln umzudrehen und zu berechnen, wie viele von ihnen zufrieden sind. Selbst wenn eine Klausel in konstanter Zeit nach Erfreulichkeit abfragt werden könnte, würde die naive Methode immer noch in $ O (VC) $ Time laufen, wobei $ v $ die Anzahl der Variablen und $ C $ die Anzahl der Klauseln ist. Ich bin sicher, wir können es besser machen, daher die Frage:

Viele lokale Suchalgorithmen drehen die Zuordnung der Variablen, die die Anzahl der zufriedenen Klauseln maximiert. Mit welchen Datenstrukturen wird dieser Vorgang in der Praxis effizient unterstützt?

Ich habe das Gefühl, dass Lehrbücher oft weglassen. Ein Beispiel ist sogar das berühmte Russell & Norvig Book.

Answer 1

Die erforderliche Datenstruktur ist eine Liste auftreten, Eine Liste für jede Variable, die die Klauseln enthält, in der die Variable auftritt. Diese Listen werden einmal erstellt, wenn der CNF zum ersten Mal gelesen wird. Sie werden in den folgenden Schritten 3 und 5 verwendet, um das Scannen der gesamten CNF -Formel zu vermeiden, um zufriedene Klauseln zu zählen.

Ein besserer Algorithmus als das Umdrehen jeder Variablen ist:

1. Erstellen Sie eine Liste nur der Variablen, die in den unbefriedigten Klauseln auftreten.
2. Wählen Sie aus dieser Liste eine Variable $ x $.
3. Zählen Sie, wie viele Klauseln, die $ x $ enthalten, zufrieden sind.
4. Flip $ x $.
5. Zählen Sie, wie viele Klauseln, die $ x $ enthalten, zufrieden sind.
6. Unflep $ x $.
7. Subtrahieren Sie das Ergebnis von Schritt 3 von Schritt 5 und zeichnen Sie es für $ x $ auf.
8. Wiederholen Sie die Schritte 2-7 für den Rest der in Schritt 1 gefundenen Variablen.
9. Drehen Sie die Variable mit der in Schritt 7 aufgezeichneten höchsten Zahl.

Eine Referenz für die Datenstruktur (häufig auch als Adjazenzliste bezeichnet) ist beispielsweise Lynce und Marques-Silva, Effiziente Datenstrukturen für Backtracking SAT Solvers, 2004.