TY  - CPAPER
AU  - Feydy, T
AU  - Stuckey, PJ
Y2  - 2014/05/21
Y1  - 2009/01/01
SN  - 3642042430
SN  - 978-3-642-04243-0
SN  - 0302-9743
UR  - http://hdl.handle.net/11343/26741
AB  - 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.
LA  - English
PB  - SPRINGER-VERLAG BERLIN
KW  - Computer Software not elsewhere classified; Computer Software and Services not elsewhere classified
T1  - Lazy Clause Generation Reengineered
DO  - 10.1007/978-3-642-04244-7_29
IS  - PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING
VL  - 5732
SP  - 352-366
L1  - /bitstream/handle/11343/26741/117718_5686.pdf?sequence=1&isAllowed=n
ER  -