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