Proseminar
SAT-Solving: Theory, Tools and Applications
News
- Zeitplan und Themenverteilung sind fertig. Informationen für welche Themen Gutachten anzufertigen sind, kommen per Email an die Gutachter (Einseitig anonyme Gutachten).
- Vorbesprechung am Freitag, 22. April um 15:30 im Raum MI00.09.038 (Turing), Anwesenheitspflicht da hier die Themenvergabe stattfindet.
Inhalt
In diesem Proseminar werden Themen aus dem Bereich SAT-Solving behandelt. Wir werden die grundlegende Theorie hinter SAT-Solvern (DPLL, Resolution), die verfügbaren Implementierungen (zB MiniSAT, Lingeling), sowie Anwendungen aus verschiedenen Bereichen (zB Model-Checking, Planning) behandeln.Ablauf
Ausarbeitung und Vortrag
Jeder Teilnehmer wählt ein Thema aus, und erstellt zu dem Thema eine Ausarbeitung (ca 10 Seiten im LaTeX article format) und einen Vortrag (genau 25 Minuten + 5 Minuten Diskussion).
Implementierung
Zu den meisten Themen gibt es außerdem eine Implementierungsaufgabe. Dazu soll ein Programm erstellt werden, das ausreichend dokumentiert ist, damit die Gutachter (s.u.) es kompilieren und ausführen können. Die Ausarbeitung und der Vortrag sollen auch auf die Lösung dieser Aufgabe eingehen.Hinweis: Die Themen ohne Implementierungsaufgabe sind etwas anspruchsvoller, und eine gute Bearbeitung erfordert eine umfangreichere Literaturrecherche.
Gutachten
Außerdem ließt jeder Teilnehmer die Ausarbeitungen und Implementierungen von zwei weiteren Teilnehmern, und gibt Feedback in Form eines Gutachtens (ca 1 Seite) dazu. Die Gutachten sollten sich hauptsächlich auf den Inhalt konzentrieren, wobei nicht erwartet wird, dass vom Gutachter weitere Recherche an den Quellen betrieben wird. Wichtig sind z.B. gute Strukturierung des Themas, schlüssige Argumentation und leicht verständliche Darstellung von Sachverhalten, die der Leser auch dann nachvollziehen kann, wenn er oder sie die Quelle dazu nicht gelesen hat. Rechtschreibung und Grammatik sind weniger wichtig, es macht aber natürlich Sinn, auch solche Fehler im Gutachten zu erwähnen. Eine Zusammenfassung des Themas ist nicht nötig. Die äußere Form des Gutachtens ist den Teilnehmern überlassen. Sowohl Stichpunkte als auch Fließtext sind in Ordnung.Anwesenheit
Anwesenheit aller Teilnehmer bei allen Vorträgen ist erwünscht!Sprache
Die Vorträge und Ausarbeitungen können, falls beim Thema nicht anders angegeben, wahlweise auf Deutsch oder Englisch sein. Das meiste Material zu den Themen ist auf Englisch.Note
Die Note setzt sich wie folgt zusammen: 20% Rezensionen + 40% Vortrag + 40% Ausarbeitung+ImplementierungTipps
Bei der Recherchearbeit können Dienste wie Google Scholar dabei helfen, wissenschaftliche Veröffentlichungen zu finden. Anschließend kann mit Hilfe von eAccess darauf zugegriffen werden. Dieser Schritt ist meist notwendig, da die Verlage oft hohe Kosten für den Download dieser Veröffentlichungen veranschlagen.
Zeitplan
Die Vorträge finden immer Freitags von 10:15 bis 11:45 im Raum MI00.09.038 (Turing) statt.
Die Ausarbeitungen und Implementierungen sind zwei Wochen vorher per Email an den Betreuer UND an Peter Lammich abzugeben.
Die Gutachten sind spätestens bis zum Vortrag fertigzustellen und per Email an Peter Lammich abzugeben.
Innerhalb einer Woche nach dem Vortrag darf eine überarbeitete Version der Ausarbeitung und Implementierung (basierend auf den Gutachten und Feedback im Vortrag) abgegeben werden, per Email an den Betreuer UND an Peter Lammich.
Teilnehmer | Thema | Betreuer | Vortrag | Deadline Ausarbeitung |
---|---|---|---|---|
Carina Bacherer | Eq-Checking 11 | Eugen Zalinescu (English) | 8.7 | 1.7 |
Christian Backs | CDCL 2 | Peter Lammich | 10.6 | 27.5 |
Ivan Baumann | Planen 10 | Peter Lammich | 8.7 | 24.6 |
David Damerow | Sortiernetzwerke 12 | Peter Lammich | 15.7 | 1.7 |
Julian Düring | DPLL 1 | Julian Brunner | 10.6 | 27.5 |
Kempec Halk | MAXSAT 7 | Peter Lammich | 1.7 | 17.6 |
Pierre Krack | MiniSAT 4 | Peter Lammich | 24.6 | 10.6 |
Micha Müller | BMC 9 | Eugen Zalinescu (English) | 8.7 | 24.6 |
Joshua Mutius | PROLOG 14 | Lars Hupel | 17.6 | 3.6 |
Philip Offtermatt | BDDs 13 | Remy (English) | 17.6 | 3.6 |
Ardit Selfo | Puzzles 8 | Peter Lammich | 1.7 | 17.6 |
Merih Berkay Sümer | GSAT 3 | Peter Lammich | 24.6 | 10.6 |
Themen
Liste mit Themenvorschlägen- DPLL-basierte SAT-Solver
Das DPLL-verfahren ist ein Standard-Verfahren zur Lösung von SAT-Problemen, und die Grundlage der meisten modernen SAT-Solver. In diesem Vortrag soll das DPLL-Verfahren und einige einfache Optimierungen vorgestellt werden, wie zB back-jumping, clause-learning, oder variable-selection Heuristiken.
Implementierung: Ein einfacher DPLL-Solver, der SAT-Probleme im DIMACS-CNF Format akzeptiert
Startpunkte:- Harrison, Handbook of Practical Logic and Automated Reasoning, Kapitel 2.9
- Biere et al, Handbook of Satisfiability, Kapitel 3
- Conflict Driven Clause Learning
CDCL ist die Weiterentwicklung von DPLL, die tatsächlich in modernen SAT-Solvern zum Einsatz kommt. In diesem Vortrag sollen die wichtigsten Techniken und Datenstrukturen von modernen SAT-Solvern erläutert werden.
Implementierung: Keine Startpunkte: Biere et al, Handbook of Satisfiability, Kapitel 4
- Unvollständige/Randomisierte Algorithmen
Inhalt: GSAT und WalkSAT
Implementierung: Einfacher GSAT-Solver, Eingabe in DIMACS-CNF
Startpunkte:- Biere et al, Handbook of Satisfiability, Kapitel 6,
- http://www.cs.rochester.edu/u/kautz/walksat/
- Tools: MiniSAT
MiniSAT ist ein moderner SAT-Solver. Es ist eine minimalistische, aber trotzdem konkurrenzfähige Implementierung eines modernen SAT-Solvers. Dieser Vortrag soll einen Überblick über das MiniSAT-Tool (und evtl. MiniSAT+) und dessen Benutzung geben.
Implementierung: Löser für einfaches Puzzle (Vorschlag: n-queens) direkt über die MiniSAT-API (Ohne Umweg über DIMACS-Format).
- Tools: Lingeling Lingeling ist ein weiterer moderner SAT-Solver. Er basiert ebenfalls auf CDCL, und benutzt zusätzlich eine Reihe von Preprocessing-Techniken. Außerdem existiert eine parallele Version, in der mehrere Solver mit unterschiedlichen Konfigurationen für die Heuristiken nebeneinander laufen, und untereinander gewisse Informationen austauschen. In diesem Vortrag soll Lingeling beschrieben werden, und ein Überblick über die wichtigsten Techniken gegeben werden. Implementierung: Löser für einfaches Puzzle (Vorschlag: n-queens) direkt über die API von Lingeling (Ohne Umweg über DIMACS-Format).
- Erweitert: Satisfiability Modulo Theories
Die Idee von SMT Solvern ist es, einen SAT-Solver mit zusätzlichen (entscheidbaren) Theorien zu kombinieren.
Dadurch können deutlich komplexere Probleme modelliert werden (zB lineare Ungleichungen), oder Probleme können kompakter dargestellt werden (zB Bitvektoren).
Dieser Vortrag soll einen Überblick über SMT und die wichtigsten Tools (Z3, CVC4, ...) geben.
Implementierung: Löser für einfaches Puzzle (Vorschlag: n-queens) über SMT-Lib oder z3-API.
Startpunkte: Biere et al, Handbook of Satisfiability, Kapitel 12 - Erweitert: MAX-SAT
Das MAXSAT Problem ist eine Generalisierung des SAT-Problems, bei dem eine Belegung gefunden werden soll, die möglichst viele Klauseln erfüllt.
Dadurch kann es für diverse Optimierungsprobleme eingesetzt werden.
Dieser Vortrag soll eine kurze Einführung in MAXSAT geben, und Techniken zur Lösung von MAXSAT mittels SAT-Solvern vorstellen
(Iterativ, Kodierung von "Cardinality-Constraints", evtl. Core-Guided).
Implementierung: Einfacher MAX-SAT Solver basierend auf linearer/binärer Suche und einem SAT-Solver (zB MiniSAT+).
Startpunkte: Morgado et al.: Iterative and core-guided MaxSAT solving: A survey and assessment - Anwendung: SAT-Solver zum Lösen von Puzzles
SAT Solver eignen sich sehr gut, um bekannte Puzzle, wie zB Sudoku, zu lösen. Dieser Vortrag soll einen Überblick über das Lösen von Sudoku mit SAT-Solvern geben, und die verwendeten Kodierungstechniken vorstellen.
Implementierung:Sudoku-Löser
Startpunkte:- Kwon, Jain: Optimized CNF encodings for Sudoku Puzzles
- Pfeiffer et al., A Sudoku-Solver for Large Puzzles using SAT
- Anwendung: SAT-Solver für Bounded Model-Checking
Beim Bounded Model Checking werden Fehler gesucht, die innerhalb einer bestimmten Grenze (zB Anzahl von Ausführungsschritten) auftreten. Solche Methoden sind zwar in der Regel nicht vollständig, können aber in der Praxis viele Fehler finden, auch in Anwendeungsgebieten, in denen das vollständige Problem unentscheidbar ist, wie zum Beispiel Software Model Checking. Das CBMC-Tool ist ein bounded Model Checker für ANSI-C Programme, der als Backend einen SAT-Solver benutzt. Sein Hauptanwendungsgebiet liegt im Bereich der eingebetteten Systeme. In diesem Vortrag soll CBMC vorgestellt werden. Implementierung:Live-Demo von CBMC während der Präsentation - Anwendung: SAT-Solver für Planen
Automatisches Planen wird im Bereich der künstlichen Intelligenz schon lange erforscht. Hierbei geht es darum, in einem bestimmten System (Domäne) einen kostenoptimalen Plan zum Erreichen eines vorgegebenen Ziels zu finden. In letzter Zeit wurden SAT-Solver erfolgreich zum Lösen von Planungsproblemen eingesetzt. Dieser Vortrag soll eine Einführung in die Verwendung von SAT-Solvern für Planen anhand der bekannten "blocks-world" Domäne geben.
Implementierung: Einfacher Löser für blocks-world Probleme
Startpunkte: Kautz, Selman: Planning as Satisfiability und (weiterführend) Kautz, Selman: Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search - Anwendung: SAT-Solver für Equivalence-Checking
Äquivalenzprüfung ist das Problem festzustellen, ob sich zwei gegebene Schaltkreise gleich verhalten. Es kann eingesetzt werden, um zum Beispiel eine Implementierung gegen eine abstraktere Spezifikation zu prüfen, oder sicherzustellen, das sich eine neue Version eines Schaltkreises gleich verhält wie das Original. Dieser Vortrag soll eine Übersicht über Äquivalenzprüfung für Schaltkreise mit Hilfe von SAT-Solvern geben.
Startpunkte: Weaver: Slides on Equivalence Checking - Anwendung: SAT-Solver zur Synthese von Sortiernetzwerken
Ein Sortiernetzwerk besteht aus einer Reihe von Compare-And-Swap Operationen, die auf ein Array von Eingabeelementen angewendet werden, so dass es am Ende sortiert ist. SAT-Solver können dazu benutzt werden, um optimale Sortiernetzwerke zu erzeugen. Dieser Vortrag soll eine kurze Einführung in Sortiernetzwerke geben, und die Techniken vorstellen, um optimale Sortiernetzwerke mit Hilfe von SAT-Solvern zu erzeugen.
Implementierung: Synthesizer für Sortiernetzwerke, basierend auf SAT-Solver (zB Minisat)
Startpunkte:- Morgenstern, Schneider: Synthesis of Parallel Sorting Networks using SAT Solvers
- (weiterführend) Bubndala, Zavotny: Optimal Sorting Networks
- Related: Binary Decision Diagrams
BDDs speichern Boolesche Funktionen (Abbildungen von n Wahrheitswerten auf einen Wahrheitswert) mit Hilfe einer Graphstruktur. Diese erlaubt in vielen Fällen eine wesentlich kompaktere Darstellung als eine Wahrheitstafel (die 2^n Zeilen braucht). BDDs unterstützen dabei diverse Operationen, um Funktionen zu kombinieren und zu modifizieren. Dieser Vortrag soll eine Einführung in BDDs und die gängigsten Optimierungen und Implementierungstechniken geben. Implementierung: Einfaches BDD-Paket + Testfälle
Startpunkte: - Related: Horn-Clauses and Prolog
Inhalt: Horn-Klauseln, Beschreibung von Prolog
PROLOG ist eine Logik-basierte Programmiersprache, mit der sich viele Probleme, zB aus dem Bereich der KI, kompakt beschreiben lassen. Prolog basiert auf dem Konzept von Horn-Klauseln. Dieser Vortrag soll einen Überblick über PROLOG geben.
Implementierung: Löser für einfaches Puzzle (Vorschlag: n-queens?) in Prolog.
Startpunkte:- Einführung in Prolog, zB: Clocksin, Mellish: Programming in Prolog
- Harrison, Handbook of Practical Logic and Automated Reasoning, Kapitel 3.14
- Related: Natürliches Schließen
Natürliches Schließen ist ein Beweiskalkül für Aussagenlogik, dh eine Reihe von Regeln, durch deren Anwendung man Aussagenlogische Formeln beweisen kann. Dieser Vortrag soll eine Einführung in diesen Beweiskalkül geben.
Implementierung: Natural Deduction Proof Checker
Startpunkt: Huth, Ryan: Logic in Computer Science: Modelling and reasoning about systems. Kapitel 1.2