From Constraints to Resolution Rules, Part I: Conceptual Framework

TL;DR

This paper introduces a logical framework for formulating resolution rules in constraint satisfaction problems, exemplified by Sudoku, to enable structured, pattern-based solutions beyond traditional search methods.

Contribution

It provides a formal logical foundation for defining resolution rules and theories in CSPs, emphasizing the concept of candidates and structured reasoning.

Findings

Defines the notion of candidates with logical status

Introduces the concepts of resolution rules and theories

Uses Sudoku as a concrete example

Abstract

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.