A hybrid BDD and SAT finite domain constraint solver

Peter Hawkins, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

10 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationPractical Aspects of Declarative Languages - 8th International Symposium, PADL 2006, Proceedings
Pages103-117
Number of pages15
DOIs
Publication statusPublished - 1 Dec 2005
Externally publishedYes
Event8th International Symposium on Practical Aspects of Declarative Languages, PADL 2006 - Charleston, SC, United States of America
Duration: 9 Jan 200610 Jan 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3819 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Symposium on Practical Aspects of Declarative Languages, PADL 2006
Country/TerritoryUnited States of America
CityCharleston, SC
Period9/01/0610/01/06

Cite this