Proseminar

SAT-Solving: Theory, Tools and Applications

News

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+Implementierung

Tipps

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
  1. 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
  2. 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

  3. Unvollständige/Randomisierte Algorithmen
    Inhalt: GSAT und WalkSAT
    Implementierung: Einfacher GSAT-Solver, Eingabe in DIMACS-CNF
    Startpunkte:
  4. 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).

  5. 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).
  6. 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
  7. 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
  8. 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:
  9. 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
  10. 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
  11. 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
  12. 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:
  13. 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:
  14. 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:
  15. 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

Material und Links