From Constraints to Resolution Rules, Part I: Conceptual Framework
This work addresses the need for constructive or pattern-based solutions in CSPs when blind search is not feasible, though it appears incremental as it builds on existing CSP techniques.
The paper tackles the problem of constraint satisfaction problems (CSPs) by introducing a logical framework for defining resolution rules and theories, using Sudoku as an example, but does not report concrete numerical results.
Many real world problems naturally appear as constraints satisfaction problems (CSP), for which very efficient algorithms are known. Most of these involve the combination of two techniques: some direct propagation of constraints between variables (with the goal of reducing their sets of possible values) and some kind of structured search (depth-first, breadth-first,...). But when such blind search is not possible or not allowed or when one wants a 'constructive' or a 'pattern-based' solution, one must devise more complex propagation rules instead. In this case, one can introduce the notion of a candidate (a 'still possible' value for a variable). Here, we give this intuitive notion a well defined logical status, from which we can define the concepts of a resolution rule and a resolution theory. In order to keep our analysis as concrete as possible, we illustrate each definition with the well known Sudoku example. Part I proposes a general conceptual framework based on first order logic; with the introduction of chains and braids, Part II will give much deeper results.