Daniel Le Berre: Integrating cutting planes in a modern SAT solver

Lunch is served at 12:00 noon (register at doodle.com/c65fxzai67p9kbqs by Friday Nov 22). 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

SAT solvers used in a daily basis in hardware or software verification are based on the so called "conflict driven clause learning (CDCL)" architecture. Such architecture is based on a proof system equivalent to full resolution. Resolution in that context is used to derive new clauses during conflict analysis. SAT solvers can easily be extended to deal with cardinality constraints and Pseudo-Boolean constraints while keep a resolution -based proof system. A major focus has been to study the translation of those constraints into CNF to reuse without modifications the current SAT solvers. Another approach is to extend the CDCL architecture to use cutting planes instead of Resolution on cardinality or pseudo Boolean constraints. The presentation will focus on the design of such kind of solver, from the specific properties of Pseudo-Boolean constraints to the design of a cutting planes based conflict analysis procedure. Some experimental results based on the implementation of such procedure available in Sat4j will conclude the talk.