Finite domain propagation solvers effectively represent the possible values of variables by a set of choices which can be naturally modelled as Boolean variables. In this paper we describe how we can mimic a finite domain propagation engine, by mapping propagators into clauses in a SAT solver. This immediately results in strong nogoods for finite domain propagation. But a naive static translation is impractical except in limited cases. We show how we can convert propagators to lazy clause generators for a SAT solver. The resulting system can solve scheduling problems significantly faster than generating the clauses from scratch, or using Satisfiability Modulo Theories solvers with difference logic. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Ohrimenko, O., Stuckey, P. J., & Codish, M. (2007). Propagation = Lazy clause generation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4741 LNCS, pp. 544–558). Springer Verlag. https://doi.org/10.1007/978-3-540-74970-7_39
Mendeley helps you to discover research relevant for your work.