Skip to content
Log in
Review Open access

Lazy clause generation in retrospect

O. Ohrimenko Peter James Stuckey M. Codish
Jul 2026 · Constraints · 0 citations · 6 references

TL;DR

This review considers how LCG has been refined and expanded over the years since its invention, and how it is used in all most performant CP solvers.

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.

DOI Semantic Scholar
Read PDF

Similar papers

Conference 2026

From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming

This work presents the first systematic analysis of how leading LCG solvers maintain their SAT encodings, based on source-code inspection and developer correspondence, and proposes a native CDCL framework for CP, replacing SAT literals with atomic constraints, enabling conflict analysis, nogood learning, and nogood propagation directly at the CP level.

Imko Marijnissen, Maarten Flippo, Emir Demirovi'c · 0 citations

CaDiCaL 3.0

This system description reports on how Kissat’s award-winning techniques were adapted to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition, to support efficient linear proof production with hints.

Florian Pollitt, Mathias Fleury, Katalin Fazekas et al. · 0 citations
Nov 2005

Composing constraint solvers

Javier O. Blanco, M. Kesseler, G. Naumoski et al. · 79 citations · ⚡1