Lazy clause generation reengineered

Thibaut Feydy, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

62 Citations (Scopus)


Lazy clause generation is a powerful hybrid approach to combinatorial optimization that combines features from SAT solving and finite domain (FD) propagation. In lazy clause generation finite domain propagators are considered as clause generators that create a SAT description of their behaviour for a SAT solver. The ability of the SAT solver to explain and record failure and perform conflict directed backjumping are then applicable to FD problems. The original implementation of lazy clause generation was constructed as a cut down finite domain propagation engine inside a SAT solver. In this paper we show how to engineer a lazy clause generation solver by embedding a SAT solver inside an FD solver. The resulting solver is flexible, efficient and easy to use. We give experiments illustrating the effect of different design choices in engineering the solver.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings
Number of pages15
ISBN (Print)3642042430, 9783642042430
Publication statusPublished - 2 Nov 2009
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2009 - Lisbon, Portugal
Duration: 22 Sep 200924 Sep 2009
Conference number: 15th (Conference Proceedings)

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5732 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Principles and Practice of Constraint Programming 2009
Abbreviated titleCP 2009
Internet address

Cite this