Problem transformations and algorithm selection for CSPs
Barry Hurley, Barry O’Sullivan · International Joint Conference on Artificial Intelligence · 2013
A constraint satisfaction problem (CSP) provides a powerful paradigm to model a large number of practical problems such as scheduling, planning, vehicle routing, configuration, network design, routing and wavelength assignment. An instance of a CSP is represented by a set of variables, each of which can be assigned a value from its domain. The assignments to the variables must be consistent with a set of constraints, where each constraint limits the values that can be assigned to variables. Finding a solution to a CSP is typically done using systematic search, based on backtracking. Because the general problem is NP-Complete, systematic search algorithms have exponential worst-case run times, which has the effect of limiting the scalability of these methods. However, the development of effective heuristics and a wide variety of solvers means than many problems become tractable. Further progress has been made on algorithms that are tailored to a particular problem domain. These algorithms have been specifically designed and tuned to perform well on a single class of instances but may perform poorly on many other problem domains. This has led to the development of solver portfolios that exploit the variation among solvers to identify the best solver for a given instance. An overview of our current contributions in this field is given in Section 3. Another option is to translate the problem to an alternative representation, for example the satisfiability problem (SAT). Several polynomial-time transformations from CSP to SAT are known [Prestwich, 2009]. The practicality of using such transformations to solve CSPs using SAT has been demonstrated by the development of a number of SAT-based CSP solvers. Sugar, Azucar and CSP2SAT4J are three examples of such solvers which have proven to be highly competitive in the most recent CSP solver competition. Sugar [Tamura et al., 2009] encodes the CSP to SAT using a specific encoding, known as the order encoding. Azucar [Tanjo et al., 2012] is a related SATbased CSP solver that uses the compact order encoding. CSP2SAT4J [Le Berre and Lynce, 2008] uses static rules to choose either the direct or the support encoding for each constraint. However, each of these use a single predefined SAT solver to solve the encoded CSP instances.