Lazy Clause Generation Reengineered
AuthorFeydy, T; Stuckey, PJ
Source TitlePRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING
AffiliationComputer Science And Software Engineering
Document TypeConference Proceeding
CitationsFeydy, T. & Stuckey, P. J. (2009). Lazy Clause Generation Reengineered. SPRINGER-VERLAG BERLIN. Lisbon, PORTUGAL.
Access StatusThis item is currently not available from this repository
F1 - Full Written Papers Refereed
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 back-jumping 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.
KeywordsComputer Software not elsewhere classified; Computer Software and Services not elsewhere classified
- Click on "Export Reference in RIS Format" and choose "open with... Endnote".
- Click on "Export Reference in RIS Format". Login to Refworks, go to References => Import References