From constraints to resolution rules part I: Conceptual framework

Abstract

Many real world problems appear naturally 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. © Springer Science+Business Media B.V. 2010.