IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2012 > Extending Lazy Clause Generation to break symmetries and almost symmetries

Maria Garcia de la Banda

Tuesday, October 30, 2012

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

Maria Garcia de la Banda, Associate Research Professor, Monash University, Australia

Extending Lazy Clause Generation to break symmetries and almost symmetries

Abstract:

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.