Fast Set Bounds Propagation Using a BDD-SAT Hybrid
This work addresses efficiency issues in set-constraint solving for researchers and practitioners in constraint programming, though it appears incremental as it builds on prior BDD techniques.
The paper tackled the overhead of constructing and manipulating graphs in BDD-based set bounds propagation for set-constraint satisfaction problems by combining BDD-based propagators with a modern SAT solver, resulting in a solver that is highly competitive with existing propagation-based solvers.
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.