@inproceedings{0560328220344403b06045abaadd5334,
title = "A hybrid BDD and SAT finite domain constraint solver",
abstract = "Finite-domain constraint solvers based on Binary Decision Diagrams (BDDs) are a powerful technique for solving constraint problems over finite set and integer variables represented as Boolean formulae. Boolean Satisfiability (SAT) solvers are another form of constraint solver that operate on constraints on Boolean variables expressed in clausal form. Modern SAT solvers have highly optimized propagation mechanisms and also incorporate efficient conflict-clause learning algorithms and effective search heuristics based on variable activity, but these techniques have not been widely used in finite-domain solvers. In this paper we show how to construct a hybrid BDD and SAT solver which inherits the advantages of both solvers simultaneously. The hybrid solver makes use of an efficient algorithm for capturing the inferences of a finite-domain constraint solver in clausal form, allowing us to automatically and transparently construct a SAT model of a finite-domain constraint problem. Finally, we present experimental results demonstrating that the hybrid solver can outperform both SAT and finite-domain solvers by a substantial margin.",
author = "Peter Hawkins and Stuckey, {Peter J.}",
year = "2005",
month = dec,
day = "1",
doi = "10.1007/11603023_8",
language = "English",
isbn = "3540309470",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "103--117",
booktitle = "Practical Aspects of Declarative Languages - 8th International Symposium, PADL 2006, Proceedings",
note = "8th International Symposium on Practical Aspects of Declarative Languages, PADL 2006 ; Conference date: 09-01-2006 Through 10-01-2006",
}