Fast Set Bounds Propagation Using a BDD-SAT Hybrid

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.

• Type: Journal
• Year: 2010
• Where: JAIR
• Authors: Graeme Gange, Peter J. Stuckey, Vitaly Lagoon
• Keywords: Binary Decision Diagram, JAIR 2010, Modern Sat Solver, Set-constraint Satisfaction Problems