Lazy Clause Generation: Combining the Power of SAT and CP (and MIP?) Solving

Finite domain propagation solving, the basis of constraint programming (CP) solvers, allows building very high-level models of problems, and using highly specific inference encapsulated in complex global constraints, as well as programming the search for solutions to take into account problem structure. Boolean satisfiability (SAT) solving allows the construction of a graph of inferences made in order to determine and record effective nogoods which prevent the searching of similar parts of the problem, as well as the determination of those variables which form a tightly connected hard part of the problem, thus allowing highly effective automatic search strategies concentrating on these hard parts. Lazy clause generation is a hybrid of CP and SAT solving that combines the strengths of the two approaches. It provides state-ofthe-art solutions for a number of hard combinatorial optimization and satisfaction problems. In this invited talk we explain lazy clause generation, and explore some...

• Type: Journal
• Year: 2010
• Where: CPAIOR
• Authors: Peter J. Stuckey
• Keywords: Account Problem Structure, Combinatorial Optimization, CPAIOR 2010, Lazy Clause Generation, Operations Research