Satisfiability Checking

Lecture · Bachelor / Master

Winter Term 2026/2027

Teachers: Erika Ábrahám, Jasper Nalbach, Valentin Promies

Contact

Important information

The contact email address for this lecture is . Note that emails regarding the lecture sent to other email addresses will not be answered.

The number of participants is limited for this lecture.

News and materials can be found in the corresponding Moodle learning room. For additional information see also the information on RWTHonline.

Background

Different approaches in computer science are based on encoding certain problems by logical formulas, such that the solutions to the logical formula encode the solutions to the original problem. To achieve these solutions, we need some tools (solvers) to check the satisfiability of logical formulas.

Propositional satisfiability is the problem of determining, for a formula of propositional logic, whether there is an assignment of truth values to its variables for which that formula evaluates to true. In the 90’s, a technology called SAT solving has become impressively powerful, being able to check the satisfiability of huge real-world propositional logic problems with millions of clauses.

Based on this success, the question raised whether these technologies could be somehow extended to check also quantifier-free first-order logic formulas over different theories for satisfiability. This would be very helpful as a lot of real-world problems cannot be conveniently encoded in propositional logic. This was the motivation for the development of so-called Satisfiability Modulo Theories (SMT) solvers.

Contents

In this course we review the algorithmic background of these developments for propositional logic and different theories, with a main focus an arithmetic theories. The lecture covers the following topics:

• Propositional logic, first-order logic theories, decidability results
• SAT solving to solve the propositional satisfiability problem
• Eager SMT solving for

• equality logic with uninterpreted functions and
• bitvector arithmetic
  • Lazy SMT solving for
• equality logic with uninterpreted functions,
• linear real arithmetic (using the Fourier-Motzkin variable elimination and the simplex algorithm),
• linear integer arithmetic (using the branch-and-bound method),
• non-linear real arithmetic (using interval constraint propagation, subtropical satisfiability, the virtual substitution and the cylindrical algebraic decomposition methods)

Materials

For learning you can use the book

Daniel Kroening and Ofer Strichman: Decision Procedures: An Algorithmic Point of View , Springer-Verlag, Berlin, 2008.

which is available in the computer science library, the lecture slides and the lecture notes that will be made available via Moodle.

Evaluations of past years

• WS 25/26: Evaluation
• WS 24/25: Evaluation
• WS 23/24: Evaluation
• WS 22/23: Evaluation
• WS 20/21: Evaluation
• WS 19/20: Evaluation
• WS 18/19: Sabbatical
• WS 17/18: Evaluation
• WS 16/17: Evaluation
• WS 15/16: Evaluation
• WS 14/15: Evaluation
• WS 12/13: Lecturer Lecture
• WS 11/12: Lecturer Lecture
• WS 10/11: Lecturer Lecture