-
Notifications
You must be signed in to change notification settings - Fork 0
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.