Jan Elffers: Conflict-driven clause learning and pseudo-Boolean SAT solving

PRACTICALITIES

Lunch is served at 12:00 noon (register at this doodle  at the latest the Saturday before 13 September, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm.Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

ABSTRACT

Conflict-driven clause learning (CDCL) is the most popular method to solve the Boolean satisfiability (SAT) problem in practice. This approach is based on backtracking search and uses clause learning to avoid solving the same subproblem multiple times. I will present the core algorithm and a number of extensions and optimizations that are incorporated in modern SAT solvers. I will also present possible directions for future research aimed at improving the understanding of this method.

The pseudo-Boolean SAT problem is a generalization of SAT with linear constraints instead of disjunctive clauses. This area is much less well developed. One approach is to use an extension of CDCL with a modified implementation of clause learning to handle linear constraints. I will present this approach as well, and I will go through an example execution of the method on the pigeonhole principle. I will also outline some interesting research questions regarding pseudo-Boolean SAT solving.