Fast Set Bounds Propagation Using a BDD-SAT Hybrid
Abstract
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.
Cite
Text
Gange et al. "Fast Set Bounds Propagation Using a BDD-SAT Hybrid." Journal of Artificial Intelligence Research, 2010. doi:10.1613/JAIR.3014Markdown
[Gange et al. "Fast Set Bounds Propagation Using a BDD-SAT Hybrid." Journal of Artificial Intelligence Research, 2010.](https://mlanthology.org/jair/2010/gange2010jair-fast/) doi:10.1613/JAIR.3014BibTeX
@article{gange2010jair-fast,
title = {{Fast Set Bounds Propagation Using a BDD-SAT Hybrid}},
author = {Gange, Graeme and Stuckey, Peter J. and Lagoon, Vitaly},
journal = {Journal of Artificial Intelligence Research},
year = {2010},
pages = {307-338},
doi = {10.1613/JAIR.3014},
volume = {38},
url = {https://mlanthology.org/jair/2010/gange2010jair-fast/}
}