Automated Reformulation of Constraint Satisfaction Problems

Abstract

A constraint satisfaction problem (CSP) consists of a set of variables {x 1, x2,..., xn}, a set of domains of values the variables can take and a set of constraints specifying which values the variables can take simultaneously. A solution to a CSP is an assignment of values to each of the variables from their domains such that no constraints are broken. They find widespread use in science and industry and can be extremely complicated, involving a large number of variables and complex constraints. CSP solvers allow users to specify CSPs in a particular syntax, and then search for solutions to the problem, normally using a configurable search approach. Correctly formulating CSPs is a skilled and time-consuming task. Moreover, once formulated, a CSP problem can take a large amount of processing time to solve. For these reasons, various methods have been devised to improve the effectiveness of CSP solving. One such method is to find additional information about the domain being studied and use this knowledge to reformulate the CSP solver to improve its effectiveness. In particular, when the domain of investigation is described by axioms in first-order logic then it may be possible to derive new theorems from those axioms. Such implied theorems are true for all instances of the domain and can therefore be added to the CSP formulation without loss of generality. Colton and Miguel (2001) used a machine learning system to discover new information about the problem domain of certain CSPs. Their approach was semi-automatic and significant aspects were performed manually. In particular, a skilled constraints programmer created the initial solver models and translated new information into constraints and a