|
| | | |
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. |
(from crpit.com)
(local if available)
|
|