Research Publications

Lazy clause generation is a powerful hybrid approach to com- binatorial optimization that combines features from SAT solving and fi- nite domain (FD) propagation. In lazy clause generation finite domain propagators are considered as clause generators that create a SAT de- scription 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 implementa- tion of lazy clause generation was constructed as a small 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 in- side 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.