zbMATH — the first resource for mathematics

Fast set bounds propagation using a BDD-SAT hybrid. (English) Zbl 1210.68100
Summary: 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.

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
MiniSat; Chaff; Cardinal
PDF BibTeX Cite
Full Text: DOI