Anleitung
Die Applikation ist in vier verschiedene Tabs gegliedert:
- Solver: Eigene Probleme können in Form einer KNF-Formel eingegeben und visualisiert/gelöst werden
- N-Damen: Visualisierung des N-Damen Problems
- Sudoku: Visualisierung des Lösens eines Sudokus
- Graphenfärbung: Visualisierung der Graphenfärbung
Um den DPLL-Algorithmus zu steuern gibt es vier Knöpfe:
- Step: Geht einen Schritt in den Algorithmus weiter
- Auto: Durchläuft automatisch den Algorithmus, bis eine Lösung gefunden wurde oder das Problem mit Erfüllbar ist
- Pause: Pausiert den automatischen Durchlauf des Algorithmus
- Reset: Setzt den Algorithmus zurück und stoppt den automatischen Durchlauf, falls aktiv
Unter den Knöpfen gibt es noch zwei Switches um die Heuristiken des DPLL Algorithmus jeweils zu aktivieren oder zu deaktivieren. Dabei gibt es folgende Heuristiken:
- Pure Literal: Reine Literale eliminieren
- Unit Propagation: Einheitsklauseln zu nutze machen
Mit einem Slider kann die Geschwindigkeit des automatisierten Durchlaufs angepasst werden
Der DPLL-Suchbaum zeigt immer den aktuellen Fortschritt des Algorithmus an. Dabei zeigt jeder Knoten eine Belegung einer Variable mit True oder mit False an. Ein Knoten entspricht dabei der Entscheidung des DPLL-Algorithmus. An den Blätter des Baumes steht dabei SAT oder UNSAT, wenn dies bereits entschieden werden kann, sonst steht dort nichts. Eine Verzweigung des Suchbaumes stellt dabei ein Backtracking Schritt des DPLL-Algorithmus dar. Wenn zwei Knoten mit einer gestrichelten Linie verbunden sind wurde dabei eine Heuristik angewandt.
Wenn man mit der Maus über einen Knoten hovert, bekommt man ein Tooltip mit den Informationen des Knotens angezeigt.
Mit einem Klick auf einen Knoten wird in einem Modal die KNF-Formel angezeigt. Dabei werden die Literale jeweils in den Farben angezeigt, welche die Belegung der Variablen repräsentiert. Die Klauseln sind dabei in einer Farbe hinterlegt, welche der Erfüllung der Klausel mit entsprechender Variablenbelegung entspricht. Dabei wird die Variablenbelegung vom angeklickten Knoten bis zur Wurzel des Suchbaumes verwendet. Dies entspricht der Variablenbelegung zu dem Zeitpunkt der Bestimmung des jeweiligen Knotens.
Im Interaktionsgraph werden Verbindungen zwischen Variablen angezeigt. Wenn zwei Variablen gemeinsam in einer Klausel vorkommen, wird dabei eine Verbindung angezeigt. Dadurch werden die Abhängigkeiten der Variablen in der KNF-Formel angezeigt. Während des Lösungsvorganges werden die Knoten in einer Farbe angezeigt, welche der aktuellen Belegung der Variablen entspricht.
Bei dem DPLL-Suchbaum und dem Interaktionsgraph kann beliebig gezoomt oder verschoben werden. Mit einem Klick auf das Icon in der linken oberen Ecke wird der Zoom und die Position zurückgesetzt. Zwischen den beiden Visualisierungsmethoden kann über den Knopf in der oberen rechten Ecke gewechselt werden.
Bei dem Solver Tab können eigene KNF-Formeln angegeben werden. Jedes Textfeld bzw. jede Zeile entspricht dabei einer Klausel. In einer Klausel werden die Literale mit einem Leerzeichen getrennt. Um für eine Negation wird das - Zeichen verwendet. Als Variable zugelassen sind alle Zeichen des Alphabets, Zahlen und Unterstriche.
Mit den Pfeiltasten kann zwischen den verschiedenen Textfeldern navigiert werden, mit Enter kann ein neues Textfeld für eine weitere Klausel hinzugefügt werden. Um eine Klausel zu entfernen kann Backspace am am Anfang eines Textfeldes genutzt werden. Das Einfügen einer Formel aus der Zwischenablage funktioniert dabei auch über mehrere Zeilen, um mehrere Klauseln auf einmal hinzufügen zu können.
Mit den Knopf links oberhalb der Eingaben kann zu einem normalen Textfeld gewechselt werden.
Bei dem N-Damen Problem wird ein Schachbrett der Größe NxN dargestellt. N kann dabei über einen Slider oberhalb des Schachbretts verändert werden. Dies funktioniert jedoch nur, wenn der Lösungsalgorithmus noch nicht gestartet worden ist.
Auf dem Schachbrett werden die Damen je nach Variablenbelegung angezeigt. Wenn eine Variable Wahr ist, wird eine Dame in schwarz angezeigt, wenn sie Falsch ist in rot. Wenn die Variable noch nicht entschieden ist, wird keine Dame angezeigt.
Bei dem Sudoku wird eine 4x4 Sudoku-Feld dargestellt. Mit einem klick auf ein Feld wird dieses markiert. Nun kann eine Zahl auf der Tastatur eingegeben werden um das Feld vorzubelegen. Um eine Zahl wieder zu entfernen kann die Backspace Taste verwendet werden. Dies funktioniert jedoch nur, wenn der Lösungsalgorithmus noch nicht gestartet worden ist.
Mit einem Slider kann dabei ein Verbose Modus aktiviert und deaktiviert werden. Ohne Verbose Modus werden nur die Zahlen in den Feldern angezeigt, welche von dem Lösungsalgorithmus als Wahr entschieden worden sind. Im Verbose Modus werden dabei auch noch die als Falsch entschiedenen Variablen in rot angezeigt.
Bei der Graphenfärbung wird eine Graph in einer Stern Form angezeigt. Dabei ist das Ziel den Graphen mit drei Farben einzufärben.
Bei N-Damen, Sudoku und der Graphenfärbung kann über einen Knopf in der linken unteren Ecke die zu dem Problem gehöhrende KNF-Formel in einem Modal angezeigt werden.