Bart Bogaerts: Symmetry exploitation for combinatorial problems

PRACTICALITIES

 Lunch is served at 12:00 noon (register at this doodle  at the latest the Saturday before, 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

The presence of symmetry in combinatorial problems often poses problems to solvers. Consider for instance, the pigeonhole problem "do n pigeons fit in n-1 holes?". This problem can, already for 10 pigeons not be solved efficiently by most Boolean satisfiability (SAT) solvers. In this talk, we revisit three recent developments related to symmetry detection and exploitation, namely BreakID, Symmetric Explanation Learning (SEL) and local domain symmetry.

BreakID is a static symmetry breaking preprocessor for SAT and ASP (a QBF version is currently being developed). The main contribution of this work is that it intelligently chooses a set of generators of the symmetry group to break in order to optimize completeness of the symmetry breaking. Symmetric Explanation Learning (SEL), a dynamic symmetry exploitation algorithm for SAT, is based on the idea that the clause learning mechanism can be strengthened whenever a clause is learnt, also its symmetric variants can be learnt. Local domain symmetry is a type of symmetry of first-order theories. It generalizes interchangeable domain elements, is efficiently detectable, and can often be broken completely with a small set of symmetry breaking formulas.