Modelling for Lazy Clause Generation

Ohrimenko, O. and Stuckey, P.

    Lazy clause generation is a hybrid SAT and finite domain propagation solver that tries to combine the advantages of both: succinct modelling using finite domains and powerful nogoods and back- jumping search using SAT technology. It has been shown that it can solve hard scheduling problems significantly faster than SAT or standard finite do- main propagation alone. This new hybrid opens up many choices in modelling problems because of its dual representation of problems as both fi- nite domain and SAT variables. In this paper we investigate some of those choices. Arising out of the modelling choices comes a novel combina- tion of bounds representation and domain prop- agation which creates a form of propagation of disjunctions. We show this novel modelling ap- proach can outperform more standard approaches on some problems.
Cite as: Ohrimenko, O. and Stuckey, P. (2008). Modelling for Lazy Clause Generation. In Proc. Fourteenth Computing: The Australasian Theory Symposium (CATS 2008), Wollongong, NSW, Australia. CRPIT, 77. Harland, J. and Manyem, P., Eds. ACS. 27-37.
pdf (from crpit.com) pdf (local if available) BibTeX EndNote GS