News  (16/02/2026): 

1. Course Schedule (DIAG Via Ariosto 25, Rome):

Days: Mon 13 -20-27/04/2026 and Mon 04/05/2025

Room:  A222 

Time: 10:00-14:00

Zoom link:  SAT-Solving

2. If you plan to attend the course (even in presence)  please write me an email so that I can share material and communications for all easily.

Teacher: Nicola Galesi -  Sapienza Università di Roma - Departement of Computer, Control and Management Engineering "Antonio Ruberti" (DIAG).

Abstract: The satisfiability problem (SAT) is the problem to determine whether a given a formula in propositional logic has a satisfying assignment or not. This is a problem  of central importance to both the theory of computer science and the practice of automatic theorem proving and proof search. For theoretical computer science, SAT is the canonical NP-complete problem. In contrast, for practical theorem proving,  SAT is the core method for encoding and solving problems. Quite surpirisingly , state-of-the-art algorithms for deciding satisfiability - so-called SAT solvers - can handle real-world instances involving hundreds of thousands or even millions of variables. SAT solvers can often run in (close to) linear time and  it is no surprise that most companies doing software or hardware verification are now using SAT solvers. Many SAT solvers are openly  available from academia or the industry and can be used as a black box with a simple input/output language developed at DIMACS.

The current state-of-the art SAT solvers are based on Resolution (DPLL algorithm) and the so called cLimitations of SAT-solversonflict-driven clause learning (CDCL) extensions of DPLL.  Some solvers also incorporate elements of algebraic reasoning like  Gaussian eliminationand  geometric reasoning based on integer programming. 

The course aim is to introduce the student to the the theoretical foundations of SAT-solving: (1) understanding Resolution and the core engines of modern SAT-solvers, i.e. DPLL algorithm and  CDCL heuristic; (2) understanding  the theoretical limitations of such solvers studying the interactions between SAT-solving and Proof Complexity, i.e.  the theory of the efficiency of proving theorems; (3) A brief glimpse inside other geometric heuristics to approach SAT-solving.

Topics:

1. SAT  problem 

   1. Complexity

   2. PTIME cases of SAT

   3. Encoding problems as a SAT problem.HW-verification & SAT.

   4. SAT & UNSAT

   5. Local search ALgorithms for SAT (Schöning algorithm)

2. Architecture of modern SAT-Solvers (CDCL)

   1. Davis-Putnam (DPLL) Algorithm 

   2.  Restarting

   3. Clause Learning

   4. Pre- & In-Processing

   5. Other SAT solvers

3. Limitations of SAT solvers

   1. SAT & UNSAT

   2. Resolution and DPLL algorithm

   3. Proof Complexity and lower bounds for proof size

   4. Proof Logging 

Prerequisites:  No specific topic is required to take the course: basic (undergrad level)  knowledge in Logic, Discrete Math, Combinatorial Optimization and Complexity theory may be helpful but not necessary. 

Evaluation: A  final presentatio n of a research paper (or part of it, if too long) concerning the  topics of the course with a final question-&-answer session.