Satisfiability, Boolean Modeling and Computation
|Tue 12-14||B222||Matti Järvisalo||19.01.2016-03.03.2016|
|Thu 12-14||B222||Matti Järvisalo||19.01.2016-03.03.2016|
|Tue 10-12||B119||Jeremias Berg||25.01.2016—04.03.2016|
Boolean satisfiability (SAT), despite being an archetypical NP-complete problem, has today become a central paradigm for exactly solving various important computationally hard problems. This success is based on recent breakthroughs in practical implementations of decision procedures for SAT, i.e., SAT solvers, that are today used as core procedures in various industrial and AI applications, ranging from automated hardware and software verification, planning, and scheduling, to data analysis and automated mathematical theorem proving.
This 5-credit course gives an up-to-date coverage of central computational aspects of SAT, focusing on techniques that are important for modern real-world applications of SAT. Topics include: basics of propositional logic and computation; modern SAT solver algorithms and search techniques; preprocessing; modelling real-world problems as SAT; building complex SAT-based procedures for Boolean optimization and other search problems beyond NP.
Prerequisites: Students are assumed to have good background on algorithms, computation, and artificial intelligence from the suitable bachelor's-level courses in computer science. Knowledge of propositional logic is an asset. The course is primarily intended for algorithmically/mathematically oriented master's-level students and postgraduate students. Students majoring in mathematics interested in real-world applications of formal logic are also encouraged to attend.
Completing the course
The course consists of weekly lectures (4 h per week) and and six weekly tutorial sessions. Active participation in the lectures and tutorials is encouraged, as the final exam is based solely on the lectures and tutorials. In order to pass the course, students will need to independently solve a set of tutorial exercises and pass a final exam.
Literature and material
The course material consists of the lectures, lecture slides, and the tutorials. The course is not based on any single book, and it is not necessary to purchase a book in order to successfully complete the course.
- January 19: Introduction, basic concepts, background on propositional logic. Standard CNF translation. [pdf]
- January 21: Background on complexity. Complete algorithms for SAT: DPLL, SAT solvers and resolution proof systems. [pdf]
- January 26: Complete algorithms for SAT: CDCL. [pdf]
- January 28: Preprocessing. Inprocessing. [pdf]
- February 2: Boolean modeling. [pdf]
- February 4: Incremental SAT solving. Minimal unsatisfiability I. [pdf]
February 9: Minimal unsatisfiability II: MUS extraction. [pdf]
Note: no lectures during February 11-18
- February 23: Boolean optimization: Maximum satisfiability I. [pdf]
- February 25: Maximum satisfiability II: Algorithms. [pdf]
- March 1: Counterexample guided abstraction refinement. Quantified Boolean formulas. Course summary. [pdf]
- March 3: "All questions answered"
Tutorials and Home Assignments
The weekly home assignment problems are included in the tutorial sheets. The deadline for returning solutions to the weekly home assignments is by the beginning of the tutorial session each week. More information is provided in the problem sheet for Tutorial 1.
- January 26 [pdf]
- February 2 [pdf]
- February 9 [pdf]
- February 16 [pdf]
- February 23 [pdf]
- March 1 [pdf]
Further Reading and Material
The topics considered on the course are based on recent developments in the field. As such, there is currently no suitable textbook available that would cover the contents of the course. However, various tutorial presentations (some with video recordings) as well as some surveys on topics covered on this course are available online. Some of these are listed here. Feel free to suggest additional links!
- SAT-SMT Summer School materials: 2011 (slides), 2012 (slides and videos), 2013 (slides), 2014 (slides), 2015 (slides)
- Theory and Practice of SAT Solving Dagstuhl materials: all, including: CDCL and SAT encodings, MaxSAT, proof systems and SAT solving
- Theoretical Foundations of Applied SAT Solving BIRS: videos, slides
- EPFL Basic Training Camp 2013 materials, including SAT-based planning, minimal unsatisfiability
Individual recent tutorials on SAT and related topics:
- SAT solving: Boolean Satisfiability Solving
- MUS: Practical Algorithms for MUS Extraction
- AAAI tutorial on SAT in AI
- SAC tutorial on Satisfiability: Algorithms, Applications and Extensions
- Modern SAT Solvers: part A, part B
- Understanding Modern SAT Solvers
- AAAI tutorial on Beyond Traditional SAT Reasoning (QBF, Model counting, Sampling)
- SAT-based model checking