Constraint Satisfaction
Background on constraint satisfaction problems
The term constraint satisfaction problems (CSPs) represents a wide range of mathematical problems with numerous real-life applications. These problems can be described formally as consisting of
- a set of variables, V1, V2, ..., Vn
- a set of corresponding finite domains D1, D2, ..., Dn, such that vi є Di, 1 ≤ i ≤ n
- a set of constraints on the variables
Well known examples of CSPs are the Eight-Queen Puzzle or Sudoku. CSPs have many industrial applications such as scheduling, configuration, and placement problems. As such, it is also a fast-growing field of academic research, closely related to artificial intelligence and operations research.
In the real world, CSPs are often amended by optimization criteria. These can be given as a set of priorities (or 'soft constraints') or as one or more optimization functions.
There are two main approaches to solving CSPs: systematic search and stochastic local search.
Systematic search generally involves two alternate steps that are preformed iteratively until a solution is found, or until all possibilities have been exhausted. The first step enforces consistency among the variables, based on the constraints. This involves eliminating from the domains values that are not consistent with the constraints. The second step performs a choice, such as assigning a value to one of the variables. If, at any point during this process, one of the domains is reduced to an empty domain, the algorithm performs a backtrack or backjump to a previous stage.
Stochastic local search (SLS), chooses an initial assignment for the variables. The algorithm then seeks to improve the assignment by incremental changes to the assignment. It generally does so in two interleaved steps: at each iteration, the algorithm first finds a set of candidate improving assignments (or the 'neighborhood' of the assignment), and then the algorithm decides on a best assignment out of this neighborhood and switches into it. While all SLS algorithms use a cost function to determine the quality of assignments, the exact method of choosing the neighborhood of any given assignment is highly solver-specific.
A SAT problem (SAT is shorthand for 'Satisfiability') is a special case of a CSP where all variables are Boolean, and constraints are logical expressions over those variables. Typically, a SAT problem is expressed in conjunctive normal form (CNF), in which all constraints are disjunctions between variables. SAT solvers (whether systematic or stochastic) can employ special-purpose heuristics which make them extremely fast compared to general-purpose CSP solvers. Therefore, they can be of great value in cases when a CSP problem can be readily expressed as a SAT problem.
Each of the three approaches (systematic, stochastic local search, and SAT) has its benefits and drawbacks. SAT solvers can be very strong for problems that can be easily expressed as SAT problems (problems arising from logical circuit design are excellent examples). However, they are rather useless on problems which are expressed as a multitude of complex, non-logical constraints. In addition, it is not natural for SAT solvers to deal with optimization problems. Systematic CSP solvers are very good at solving complex problems, with many different types of constraints, provided that each of the constraints can be associated with a strong propagation algorithm. Stochastic local search solvers are most appropriate for complex problems which cannot be associated with good constraint propagation. Both systematic and SLS solvers have a good ability to cope with optimization problems. However, whereas systematic CSP and SAT solvers are typically complete (i.e., can prove that a problem does not have a solution), SLS solvers are usually incomplete.
Of course, for some problems, more than one of these approaches can be applied to gain maximum benefit of each. Such hybrid algorithms pose a technical challenge on one hand, but show great promise on the other hand.
Resources
- An excellent tutorial on constraint solving techniques (mainly systematic CSP): http://ktiml.mff.cuni.cz/~bartak/constraints/index.html
- A local-search tutorial based on 'Stochastic Local Search' by H. H. Hoos and T. Stutzle: http://www.sls-book.net/slides.html
- An extensive CSP benchmark library: http://www.csplib.org
- Other resources on CSP can be found at the official Association for Constraint Programming page: http://slash.math.unipd.it/cp
- An extensive reference to SAT tutorials and resources: http://www.satlive.org
- And of course: http://en.wikipedia.org/wiki/Constraint_satisfaction_problem