We describe a unified, lazy, declarative framework for solving constraint satisfaction problems,
an important subclass of combinatorial search problems. These problems are both
practically significant and computationally hard. Finding solutions involves combining good
general-purpose search algorithms with problem-specific heuristics. Conventional imperative
algorithms are usually implemented and presented monolithically, which makes them hard
to understand and reuse, even though new algorithms often are combinations of simpler
ones. Lazy functional languages, such as Haskell, encourage modular structuring of search
algorithms by separating the generation and testing of potential solutions into distinct functions
communicating through an explicit, lazy intermediate data structure. But only relatively
simple search algorithms have been treated this way in the past. Our framework uses a generic
generation and pruning algorithm parameterized by a labeling function that annotates search
trees with conflict sets. We show that many advanced imperative search algorithms, including
conflict-directed backjumping, backmarking, minimal forward checking, and fail-first dynamic
variable ordering, can be obtained by suitable instantiation of the labeling function. More
importantly, arbitrary combinations of these algorithms can be built by simply composing
their labeling functions. Our modular algorithms are as efficient as the monolithic imperative
algorithms in the sense that they make the same number of consistency checks, and most
of our algorithms are within a constant factor of their imperative counterparts in runtime
and space usage. We believe our framework is especially well-suited for experimenting to find
good combinations of algorithms for specific problems.
Learning variable ordering heuristics for solving Constraint Satisfaction Problems
