News  (31/01/2025): 

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

Days: Wed 19/03,  Wed 26/03,   Wed 02/04,  Wed  09/04,  Wed 16/04

Room:  A5 17:00-20:00

Zoom link:  Students enrolled in the course and not coming in the room are invited to write me in order to receive the Zoom link.

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 conflict-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.

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.