Jo Devriendt: How combinatorial solvers generate proofs

PRACTICALITIES

Lunch is served at 12:00 noon (register at this doodle  at the latest on Tuesday March 6, 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 1½-2 hours of more technical discussions.

ABSTRACT

A crucial idea behind Conflict-Driven Clause Learning SAT solvers is to interleave a) the search for a satisfying assignment with b) the construction of a proof of infeasibility. Though modern SAT solvers are the original and most straightforward exponent of this idea, all combinatorial solvers can be studied from this viewpoint. In this talk, we examine the landscape of modern combinatorial solvers, looking for patterns and differences in how they construct their proofs and how they combine this with their search routines. System families such as ASP, CP, SMT and MIP are investigated from a high-level point of view, while relevant algorithms are presented of individual systems such as IntSat, CutSat, Symmetric Explanation Learning and IDP.