Sciweavers

Share
CPAIOR
2010
Springer

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

9 years 2 months ago
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...
Peter J. Stuckey
Added 10 Feb 2011
Updated 10 Feb 2011
Type Journal
Year 2010
Where CPAIOR
Authors Peter J. Stuckey
Comments (0)
books