Modelling for lazy clause generation

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.