FastSet BoundsPropagation Usinga BDD-SATHybrid.pdf

Journal of Artificial Intelligence Research 38 (2010) 307-338 Submitted 01/10; published 06/10 Fast Set Bounds Propagation Using a BDD-SAT Hybrid Graeme Gange ggange@.au Peter J. Stuckey pjs@.au National ICT Australia, Victoria Laboratory Department of Computer Science and Software Engineering The University of Melbourne, Vic. 3010, Australia Vitaly Lagoon lagoon@ Cadence Design Systems 270 Billerica Rd, Chelmsford, MA 01824, USA Abstract Binary Decision Diagram (BDD) based set bounds propagation is a powerful approach to solving set-constraint satisfaction problems. However, prior BDD based techniques in- cur the significant overhead of constructing and manipulating graphs during search. We present a set-constraint solver which combines BDD-based set-bounds propagators with the learning abilities of a modern SAT solver. Together with a number of improvements beyond the basic algorithm, this solver is highly competitive with existing propagation based set constraint solvers. 1. Introduction It is often convenient to model a constraint satisfaction problem (CSP) using finite set variables and set relationships between them. A common approach to solving finite domain CSPs is using a combination of backtracking search and a constraint propagation algorithm. The propagation algorithm attempts to enforce consistency on the values in the domains of the constraint variables by removing values from the domains of variables that cannot form part of a complete solution to the system of constraints. The most common level of consistency i