From Constraints to Resolution Rules, Part I: Conceptual Framework
  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.
