SAT-Solving

Lehrveranstaltung mit SWS 2/2/0 (Vorlesung/Übung/Praktikum) in SS 2019

Dozent

Steffen Hölldobler

Tutor

Johannes Fichte

Umfang (SWS)

2/2/0

Module

Leistungskontrolle

Mündliche Prüfung

Information

Template slides in Beamer for presentations are online. You can find them here. Submission to the sudoku competition is open. Pls register on Easychair.

   Please register your group by Thursday July, 4th. Initial submissions should be done by July 9th and the submission closes on July, 31st.

Description

The propositional satisfiability problem (SAT) is a fundamental decision problem in computer science. It is the first problem to be known as NP-complete and unquestionably one of the most used problems to establish NP-hardness in modern computational complexity. Despite its academic importance and its use to easily encode fundamental problems and puzzles such as Hamiltonian path/cycle and sudoku, SAT allows for solving industrial problems, e.g., verifying computer hard- and software or crypthographic techniques. In the last two decades, SAT solvers have been significantly improved and their techniques go far beyond the original tree-based resolution approach (DPLL algorithm) from the 1960s.

In the lecture, we talk about theoretical foundations of SAT solving, present abstract solving algorithms, and structural properties that are exploited by modern SAT solvers. In addition, we look into implementations and related variants of the problem, for example MaxSAT, which is a generalization of SAT and asks to output the maximum number of clauses of a propositional formula (in CNF) that can be made satisfiable. MaxSAT can be used to find a „best“ solution or to obtain a smallest unsatisfiable subformula by using such a solver as an oracle and calling the solver multiple times. Finally, we discuss some ideas on parallel solving.

You will receive both theoretical as well as practical assignments, for example, constructing reductions to SAT and implementing algorithms.

Beschreibung

Das Erfüllbarkeitsproblem (SAT) der Aussagenlogik ist ein fundamentales Entscheidungsproblem der Informatik, und das repräsentative Problem der Komplexitätsklasse NP. Neben vielen akademischen Anwendungen, die sich auf SAT reduzieren lassen, gibt es auch industriell relevante Probleme, die gelöst werden können. Einige Beispiele sind das Lösen von Sudokus, das Lösen von Hamiltonion Path und Hamiltonian Cycle Problemen, aber auch die Verifikation von Hardware und Software. Selbst Attacken auf Crypthographie-Verfahren sind mit SAT möglich.

In den letzten zwei Jahrzehnten wurden SAT Solver -- Algorithmen die das Efüllbarkeitsproblem lösen -- wesentlich verbessert, und gehen weit über den DPLL Algorithmus der 1960er hinaus. Die Vorlesung präsentiert zum einen die theoretischen Grundlagen, auf denen SAT Solver aufbauen und führt Lösungsalgorithmen abstrakt ein und diskutiert Eigenschaften, die ausgenutzt werden können, um effiziente SAT Solver zu erhalten.

Auf der anderen Seite werden interna von SAT Solvern beleuchtet, und verwandte Anwendungen aufgezeigt. So kann mit MaxSAT -- der Optimierungsvariante des Erfüllbarkeitsproblems -- eine beste Lösung gefunden werden, oder durch mehrfaches Aufrufen eines Solvers eine kleinste unerfüllbare Teilformel gefunden werden. Die Varianten des Lösens werden ebenso diskutiert, wie das parallele Lösen des SAT Problems. Dabei wird auch auf die effiziente Implementierung geachtet.

In den Übungen werden sowohl theoretische als auch praktische Aufgabenstellungen gegeben. Es sollen sowohl Lösungsalgrithmen implementiert, als auch Probleme auf das SAT Problem reduziert werden.

Presentations on Applications in SAT

Schedule

Lecture (APB/E005): Mon 4. DS (13:00 - 14:30)
Tutorials (APB/E005): Wed 4. DS (13:00 - 14:30) starting from Wed April 10th
Guest Talk by Kuldeep Meel on Approximate Model Counting on April 9th (Tue), APB-2026, 13:30; Feel free to join

Assignments

2019-06-02: be ready to present the first assignment (papers)
Feel free to send me the slides beforehand
Groups:
- 5.6.2019:
  - Program Termination
  - Mining Association Rules (MAR)
  - Multi Agent Path Finding (MAPF)
- 17.6.2019
  - Bounded Model Checking
  - FPGA SAT
  - Bioinformatics
- 19.6.2019: Pythagorean Triples
- 10.7.2019: Cook-Levin Theorem

Lecture Slides

Exercises

Send me a mail to get access to a git repository with the sources of the exercise files
2019-04-10 Exercise 1
2019-04-17 Exercise 2
For first assignment pls consult the Online Poll
2019-04-24 (by Emma) Ex.2.4bc F_1and F_2; Ex. 2.6 + Exercise 3
2019-05-08 (by Emma) Presentations in Beamer. You can find an example here / Sudoku
2019-05-15 (by Emma) Ex 3
Sudoku Competition
2019-05-22 Dies Academicus
2019-05-29 Cont. Lecture
2019-06-05 Talks
2019-06-12 Holidays
2019-06-19 50 Years CS Celebration in Dresden
2019-06-26 Consultation on Sudoku Competition (Practical Questions)
2019-07-03 Sudoku Discussions, Hands on Exercises on Conflict Graphs