SAT Solvers and Their Applications in Trustworthy Computing
Special Topics in Formal Methods
Timings: Tuesday and Friday: 2-3.30 pm
What is this course about?
In this course, we will delve into the fascinating world of SAT solvers. SAT, or Boolean satisfiability, is a fundamental problem in computer science. At its core, the problem of Boolean satisfiability asks a simple question: given a Boolean formula, can we find an assignment of truth values to its variables that satisfies the formula? Boolean satisfiability is known to be NP-complete. However, modern SAT solvers offer efficient solutions capable of handling problems with tens of thousands of variables and millions of clauses in practical scenarios. The beauty of SAT solvers lies in their efficiency. They employ sophisticated algorithms and techniques to efficiently explore the vast space of possible variable assignments, searching for a satisfying assignment. In this course, we will discover the secret behind modern SAT solvers, called conflict-driven clause learning (CDCL). It's like having a super-smart helper who learns from mistakes to solve problems faster! We'll dive into how SAT solvers are used in real life, from explainable or certified AI, to verification and synthesis of automated systems, to optimization problems related to graphs.
Outline
- Modelling with propositional logic, constraints encodings.
- Basic of SAT solving, including overview of conflict-driven clause learning (CDCL), and modern heuristics.
- Recent applications: explainable and verifiable AI, verification and synthesis of automated systems, optimization problems related to graphs.
Prerequisites
Recommended but not essential: Discrete Mathematical Structures and Logic for Computer Science. It is required to have a basic knowledge of propositional logic, algorithms, and data structures, as well as familiarity with complexity theory (concepts like NP-completeness should not be unfamiliar), and proficiency in at least one programming language, such as Python.
To know more
- Handbook of Satisfiability (chapter 2 and 4): Edited by Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh.
- Solvers available from the SAT community can be found here. Moreover, a detailed documentation on SAT solvers's API in python (PySAT) can be found here.
- ACM article on (R)evoultion of SAT can be found here.