Fast set bounds propagation using a BDD-SAT hybrid

DOI10.1613/JAIR.3014MaRDI QIDQ3579357zbMATH OpenOpenAlexWikidataFDO

Authors Graeme Gange, Peter J. Stuckey, V. Lagoon

Publication date 6 August 2010

Published in Journal of Artificial Intelligence Research (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.3846

zbMATH Keywords

Binary Decision DiagramSAT solver

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: 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.

Recommendations

• scientific article; zbMATH DE number 2243396
• Principles and Practice of Constraint Programming – CP 2004
• On the properties of combination set operations.
• Theory and Applications of Satisfiability Testing
• A BDD SAT solver for satisfiability testing: An industrial case study

Cited in

(7)

• STR3: a path-optimal filtering algorithm for table constraints
• On the properties of combination set operations.
• Exact stochastic constraint optimisation with applications in network analysis
• MDD propagators with explanation
• scientific article; zbMATH DE number 1956595 (Why is no real title available?)
• scientific article; zbMATH DE number 2243396 (Why is no real title available?)
• Principles and Practice of Constraint Programming – CP 2004

Describes a project that uses

Uses Software

• Cardinal
• MiniSat
• Chaff

This page was built for publication: Fast set bounds propagation using a BDD-SAT hybrid

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3579357)