×

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.

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