Propagation = Lazy Clause Generation
Olga Ohrimenko, Peter Stuckey and Michael Codish
Proceedings of the 13th International Conference on
Principles and Practice of Constraint Programming,;
2007
Abstract:
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.Available: bibtex entry pdf
Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il