Laurent Simon: Experimenting with CDCL SAT solvers and glue clauses

PRACTICALITIES

Lunch is served at 12:00 noon (please register at this doodle as soon as possible, but at the very latest on Saturday). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½-2 hours of more technical discussions.

ABSTRACT

Trying to tackle in practice NP-Complete problems was believed hopeless 20 years ago. However, with the introduction of Conflict Driven Clause Learning algorithms (CDCL for short) in the late 90's, we observed one of the most fascinating victories against hard problems. However, despite these impressive results, the underlying reasons for these successes are just partially known. We will begin this talk by presenting a set of experiments showing why SAT solvers are so hard to study in practice.

 

In a second part of the talk, we will focus on one of the many ingredients of SAT solvers: the concept of glue clauses and Literal Bock Distance. This measure for the quality of learnt clauses was introduced in 2009 and is now used in most of CDCL solvers.  However, despite its interest, this measure is not fully understood. We will present the concept of glue clauses, as it was stated five years ago, and develop new insights in what may explain its performance, for instance by trying to find correlations between blocks as stated in the LBD measure and communities.