Lazy clause generation in retrospect

Abstract

Lazy clause generation (LCG) is an approach to building constraint programming (CP) solvers that uses ideas from Boolean Satisfiability (SAT) solvers. Propagation in the CP solver is extended to explain itself, lazily creating explanation clauses. This allows SAT style conflict analysis to be used to create clausal nogoods that record the reason for failure, and avoid the same failure in the future. LCG has proven to be a highly effective architecture, used in all most performant CP solvers. In this review we consider how LCG has been refined and expanded over the years since its invention.