Fast Set Bounds Propagation Using a BDD-SAT Hybrid
Graeme Gange, Peter J Stuckey, Vitaly Lagoon
JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH | AI ACCESS FOUNDATION | Published : 2010
Binary Decision Diagram (BDD) based set bounds propagation is a powerful approach to solving set-constraint satisfaction problems. However, prior BDD based techniques incur 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. © 2010 AI Access Foundation.
Part of this work was published previously (Gange, Lagoon, & Stuckey, 2008). NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council.