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 t..