Einheitsresolution (Unit Propagation)

Tritt eine Einheitsklausel ${\displaystyle \psi }$ auf, so muss ihr einziges Literal wahr sein. Weise dem Literal den entsprechenden Wahrheitswert zu und entferne alle Klauseln, die ${\displaystyle \psi }$ enthalten. Entferne Vorkommen des Literals ${\displaystyle \lnot \psi }$ aus allen Klauseln.

In der Praxis führt Einheitsresolution oft dazu, dass wiederum Einheitsklauseln erzeugt werden und somit der naive Suchraum signifikant verkleinert wird.

Pure Literal Elimination

Kommt ein Literal als pures Literal vor, so kann ihm ein Wert zugewiesen werden, sodass alle Klauseln, die das Literal enthalten, wahr werden. Entferne diese Klauseln.

Der Algorithmus zusammengefasst im Pseudocode:

function DPLL(F : set of clauses)
    # Konsistent bedeutet, es kommt ausschließlich ¬l oder l vor
    if F is a consistent set of literals then
        # Hier können zusätzlich die Literale zurückgegeben werden
        return true;
    if F contains an empty clause then
        return false;
    for every unit clause {l} in F do
        F ← unit-propagate(l, F);
    for every literal l that occurs pure in F do
        F ← pure-literal-assign(l, F);
    l ← choose-literal(F);

    # Mit Kurzschlussauswertung für das Oder
    return DPLL({F : l = true}) or DPLL({F : l = true}); #

Dabei wenden unit-propagate(l, F) und pure-literal-assign(l, F) die beiden Regeln entsprechend an und geben die vereinfachte Formel zurück.

Die Effizienz von DPLL hängt sehr stark von der Auswahl des Literals ${\displaystyle l}$ (Branching Literal) ab. Für manche Instanzen kann diese Wahl den Unterschied zwischen konstanter und exponentieller Laufzeit ausmachen. Darum definiert DPLL vielmehr eine ganze Familie von Algorithmen, die unterschiedliche Heuristiken für die Wahl von ${\displaystyle l}$ verwenden.

Die Probleme von DPLL können in drei Punkten zusammengefasst werden:

1. Die Entscheidungen für Branching Literals werden naiv getroffen.
2. Aus Konflikten wird nichts gelernt, außer dass die aktuelle (partielle) Variablenbelegung zu einem Konflikt führt. Dabei lassen sich mehr Informationen über die Ursache des Konfliktes extrahieren und so große Teile des Suchraumes ausschließen.
3. Backtracking springt nur jeweils eine Ebene im Suchbaum nach oben, was zu einem sehr großen Suchraum führt.

In der Praxis werden diese Probleme gelöst durch

1. Heuristiken, z. B. in einem Look-Ahead-Solver
2. Clause Learning (CDCL)
3. Backjumping (CDCL)

Backjumping und Clause Learning

Bei CDCL findet das Backtracking nicht mehr chronologisch statt, sondern es werden Ebenen des Suchbaumes übersprungen. Außerdem werden Informationen über Variablenbelegungen, die in Kombination einen Konflikt verursachen, als Klausel der Klauselmenge hinzugefügt.

• Backtracking ohne Backjumping
• Backtracking mit Backjumping

Um Backjumping zu ermöglichen merkt sich CDCL, welche Zuweisungen von Wahrheitswerten zu Variablen willkürlich waren und welche Zuweisungen durch Unit Propagation erzwungen wurden. In der Praxis funktioniert das mittels eines Implikationsgraphen.

Ein Implikationsgraph ist ein gerichteter, azyklischer Graph ${\displaystyle G=(V,E)}$. Jeder Knoten ${\displaystyle v\in V}$ besteht dabei aus einem Tupel ${\displaystyle (x\in \{false,true\},\ d)}$ oder einem Element ${\displaystyle c}$. Während das Tupel für eine Zuweisung von wahr oder falsch für ein Literal ${\displaystyle x}$ auf Ebene ${\displaystyle d}$ des Suchbaumes steht, steht ${\displaystyle c}$ für einen aufgetretenen Konflikt. Ein Konflikt tritt auf, wenn ein Literal gleichzeitig den Wert wahr und den Wert falsch annehmen müsste.

Wenn der Algorithmus ein Literal willkürlich mit einem Wahrheitswert belegt, wird der entsprechende Knoten ${\displaystyle v}$ mit dem Tupel, das diese Zuweisung repräsentiert, zu ${\displaystyle G}$ hinzugefügt. Erzwingt diese Zuweisung durch Unit Propagation eine weitere Zuweisung, so wird ein weiterer Knoten ${\displaystyle w}$ und eine Kante ${\displaystyle e=(v,w)}$ zum Graphen hinzugefügt.

Im Folgenden ein Beispiel mit der Formel: (${\displaystyle x_{1}}$ ∨ ${\displaystyle x_{4}}$) ∧ (${\displaystyle x_{1}}$ ∨ ${\displaystyle \lnot x_{3}}$ ∨ ${\displaystyle \lnot x_{8}}$) ∧ (${\displaystyle x_{1}}$ ∨ ${\displaystyle x_{8}}$ ∨ ${\displaystyle x_{12}}$) ∧ (${\displaystyle x_{2}}$ ∨ ${\displaystyle x_{11}}$) ∧ (${\displaystyle \lnot x_{7}}$ ∨ ${\displaystyle \lnot x_{3}}$ ∨ ${\displaystyle x_{9}}$) ∧ (${\displaystyle \lnot x_{7}}$ ∨ ${\displaystyle x_{8}}$ ∨ ${\displaystyle \lnot x_{9}}$) ∧ (${\displaystyle x_{7}}$ ∨ ${\displaystyle x_{8}}$ ∨ ${\displaystyle \lnot x_{10}}$) ∧ (${\displaystyle x_{7}}$ ∨ ${\displaystyle x_{1}}$ ∨ ${\displaystyle \lnot x_{12}}$)

• Implikationsgraph nach dem 8. Schritt
• Implikationsgraph mit Konflikt

1. Wähle ${\displaystyle x_{1}}$ willkürlich und belege es (wieder willkürlich) mit false.
2. Unit Propagation erzwingt eine Belegung von ${\displaystyle x_{4}}$ mit true. Damit wird die Klausel (${\displaystyle x_{1}}$ ∨ ${\displaystyle x_{4}}$) wahr.
3. Wähle ${\displaystyle x_{3}}$ und belege es mit true.
4. Unit Propagation erzwingt nun die Belegung von ${\displaystyle x_{8}}$ mit false (wegen ${\displaystyle x_{1}}$ = false). Die Klausel (${\displaystyle x_{1}}$ ∨ ${\displaystyle \lnot x_{3}}$ ∨ ${\displaystyle \lnot x_{8}}$) wird wahr.
5. Unit Propagation erzwingt die Belegung von ${\displaystyle x_{12}}$ mit true (wegen ${\displaystyle x_{8}}$ = false). Die Kausel (${\displaystyle x_{1}}$ ∨ ${\displaystyle x_{8}}$ ∨ ${\displaystyle x_{12}}$) wird wahr.
6. Wähle ${\displaystyle x_{2}}$ und belege es mit false.
7. Unit Propagation erzwingt nun die Belegung von ${\displaystyle x_{11}}$ mit true. Die Klausel (${\displaystyle x_{2}}$ ∨ ${\displaystyle x_{11}}$) wird wahr.
8. Wähle ${\displaystyle x_{7}}$ und belege es mit true. Die Klauseln (${\displaystyle x_{7}}$ ∨ ${\displaystyle x_{8}}$ ∨ ${\displaystyle \lnot x_{10}}$) und (${\displaystyle x_{7}}$ ∨ ${\displaystyle x_{1}}$ ∨ ${\displaystyle \lnot x_{12}}$) werden wahr.
9. Ein Konflikt tritt auf für ${\displaystyle x_{9}}$. Unit Propagation muss die Klauseln (${\displaystyle \lnot x_{7}}$ ∨ ${\displaystyle \lnot x_{3}}$ ∨ ${\displaystyle x_{9}}$) ∧ (${\displaystyle \lnot x_{7}}$ ∨ ${\displaystyle x_{8}}$ ∨ ${\displaystyle \lnot x_{9}}$) erfüllen, die inzwischen zu ${\displaystyle x_{9}}$ ∧ ${\displaystyle \lnot x_{9}}$ reduziert wurden. Der Konfliktknoten ${\displaystyle c}$ wird in den Implikationsgraphen eingefügt.

Der Algorithmus analysiert nun den Konflikt mithilfe des Implikationsgraphen und entscheidet, welche Klausel gelernt werden soll und zu welchem Entscheidungslevel im Suchbaum zurückgesprungen werden soll. In Frage kommende Klauseln heißen conflict clause und sollen verhindern, dass die Fehlentscheidung des Algorithmus, die zum Konflikt geführt hat, wiederholt wird. Eine solche conflict clause wird zur Klauselmenge hinzugefügt. Das maximale Entscheidungslevel der Variablen aus der conflict clause bestimmt das Entscheidungslevel für das Backjumping.

Eine abstrakte Beschreibung von CDCL im Pseudocode sieht wie folgt aus:

function CDCL(F : set of clauses)
    G <- Implikationsgraph();
    if unit-propagate(F, G) findet Konflikt then
        return false;

    level ← 0;
    while F hat nicht zugewiesene Variablen do
        level ← level + 1;
        choose-literal(F, G);

        while unit-propagate(F, G) findet Konflikt do
            # Ermittle Ebene für Backjump und zu lernende Klausel
            (d, c) ← analyzeConflict(G);

            # Lerne
            F ← F ∪ {c};

            # Wenn der Konflikt nicht aufgelöst werden kann
            if d < 0 then
                return false;
            else
                backjump(F, d);
                level ← d;
    return true;

Dabei aktualisieren unit-propagate(F, G) und choose-literal(F, G) jeweils entsprechend den Implikationsgraphen. Die Funktion analyzeConflict(G) wird durch die Strategie des clause learning bestimmt.

Conflict Clauses

Um eine conflict clause zu ermitteln untersucht man Schnitte im Implikationsgraphen. Ein Schnitt generiert eine conflict clause genau dann, wenn er den Graph so in zwei Hälften partitioniert, dass eine Hälfte (die decision side) alle decision nodes enthält und die andere Hälfte den Konfliktknoten. Die decision nodes sind dabei die willkürlichen Entscheidungen, die zum Konflikt geführt haben.

Aus dem Implikationsgraphen wird ersichtlich, dass z. B. für ${\displaystyle x_{3}}$ und ${\displaystyle x_{7}}$ eine willkürliche Entscheidung getroffen wurde, aber die Entscheidung für die Belegung von ${\displaystyle x_{8}}$ eine Konsequenz aus der Entscheidung für die Belegung von ${\displaystyle x_{1}}$ und ${\displaystyle x_{3}}$ war. Die Knoten für ${\displaystyle x_{1}}$, ${\displaystyle x_{3}}$, ${\displaystyle x_{7}}$ sind also die decision nodes.

Ein Beispiel für einen Schnitt, der eine conflict clause generiert, ist ein Schnitt durch die eingehenden Kanten des Konfliktknotens (roter Schnitt in der Abbildung). Die Knoten auf der decision side repräsentieren die Ursache des Konfliktes, nämlich ${\displaystyle x_{3}\land x_{7}\land \lnot x_{8}\implies Konflikt}$. Durch Kontraposition erhält man ${\displaystyle \lnot Konflikt\implies \lnot x_{3}\lor \lnot x_{7}\lor x_{8}}$, ein Beispiel für eine conflict clause. Eine andere Möglichkeit stellt der blaue Schnitt durch die ausgehenden Kanten der decision nodes dar. Er generiert die conflict clause ${\displaystyle \lnot x_{1}\lor x_{3}\lor x_{7}}$. Diese Variante wurde in Rel_sat implementiert, einem der ersten CDCL SAT-Solver. Eine fortgeschrittene Variante wird von der Implementierung GRASP eingesetzt.

Two Watched Literals (TWL, 2WL)

Es bleibt das Problem, Einheitsklauseln für die Unit Propagation und Konflikte effizient zu finden. Lange Zeit haben Solver dafür die Anzahl Literale, die in einer Klausel noch nicht mit Wahrheitswerten belegt worden sind, mitgezählt. Wenn sich dieser Zähler von 2 auf 1 ändert wendet man Unit Propagation an. Da uns der genaue Wert des Zählers aber eigentlich nicht interessiert, sondern wir nur wissen müssen, wann sich die Zahl auf eins ändert, verfolgen wir nicht die Klauseln selbst, sondern jeweils zwei Literale pro Klausel – die two watched literals. TWL ist also eine Datenstruktur, die die Suche nach Konflikten oder Einheitsklauseln beschleunigt.

Jede Klausel, die noch nicht erfüllt ist, besitzt zwei watched literals. Die Information wird dabei nicht von den Klauseln gespeichert, sondern von den Literalen selbst. Jeder Literal ${\displaystyle l}$ besitzt also eine Liste mit Klauseln, in denen er vorkommt. Diese Klauseln werden in einer Liste verkettet, der watch list.

Die TWL einer Klausel erfüllen folgende Invariante:

„Solange kein Konflikt gefunden wurde darf ein watched literal nur false sein, solange der andere watched literal true ist und alle unwatched literals false sind.“

Die Invariante führt dazu, dass die Belegung eines unwatched literals mit einem Wahrheitswert niemals zu einer unit propagation oder einem Konflikt führen wird. Wenn wir nun aber einem watched literal ${\displaystyle l}$ einen Wahrheitswert zuweisen, müssen wir eventuell die Invariante reparieren, unit propagation anwenden oder einen Konflikt auflösen. Betrachten wir die Klauseln, in denen die Negation von ${\displaystyle l}$, also ${\displaystyle \lnot l}$ vorkommt. Diese können durch die watch list effizient gefunden werden. Wir verfahren für diese wie folgt:

1. Ist der andere watched literal der Klausel true, müssen wir nichts tun.
2. Ist einer der unwatched literals ${\displaystyle l'}$ der Klausel nicht false, wählen wir ${\displaystyle l'}$ als watched literal, der ${\displaystyle \lnot l}$ ersetzt.
3. Ist der andere watched literal ${\displaystyle l'}$ für diese Klausel noch nicht mit einem Wahrheitswert belegt, führe unit propagation für ${\displaystyle l'}$ durch. Ansonsten ist ${\displaystyle l'}$ false und ein Konflikt wurde gefunden.

TWL wurde für den SAT-Solver Chaff entwickelt, um die unit propagation in der Praxis zu optimieren.

Random Restart

Random Restarts setzen alle Variablenbelegungen zurück und starten die Suche mit einer anderen Reihenfolge der Variablenbelegung neu. Damit wird das Problem umgangen, dass manche dieser Zuweisungsreihenfolgen zu sehr viel länger andauernden Berechnungen mit vielen Konflikten führen, während geeignete Reihenfolgen das Problem schneller lösen. Dabei werden gelernte Klauseln und die aktuell zugewiesenen Werte der Variablen übernommen. Wann ein Restart durchgeführt wird bestimmt eine Strategie, z. B. fixed nach n Konflikten, in Abständen, die einer Reihe wie der geometrischen Reihe folgen oder dynamisch, wenn sich Konflikte beginnen zu häufen. Restart-Strategien sind häufig an eine bestimmte Klasse von Instanzen angepasst und aggressivere Strategien haben sich in vielen Fällen als effizient herausgestellt.