Modelling for lazy clause generation

Abstract

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..