Extending Lazy Clause Generation to break symmetries and almost symmetries

October 30, 2012

Maria Garcia de la Banda


Extending Lazy Clause Generation to break symmetries and almost symmetries

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

Lazy Clause Generation is a powerful approach for reducing search in Constraint Programming. It works by recording the reasons that lead to failure (nogoods) and propagating them using SAT technology. Symmetry breaking is also a powerful approach for reducing search that works by ensuring the execution does not explore symmetric parts of the search space.

In this talk, I will first show how we can extend Lazy Clause Generation to break symmetries and how the more precise nogoods generated by a lazy clause solver allow our approach to exploit symmetries that cannot be exploited by any previous symmetry breaking method. Then, I will show how the method can easily be modified to exploit almost symmetries (that is, symmetries that would appear in the problem if a small set of constraints is removed) very effectively. This is significant because they appear in many real world problems and can be exploited to yield significant speedups.