Constraint Resolution Theories

A pure logic pattern-based perspective of solving Constraint Satisfaction Problems

Denis Berthier

26 euros    (paperback, 312 pages, Royal: 6.14" x 9.21" - 15.6 cm x 23.4 cm)

ISBN : 978-1-4478-6888-0
Lulu.com Publishers, October 2011

Support independent print-on-demand publishing, buy this book directly from Lulu

Keywords: Artificial Intelligence, Constraint Satisfaction, Constructive Logic, Logic Puzzles, Sudoku.

See also "Pattern-Based Constraint Satisfaction and Logic Puzzles", the revised and largely extended (484 p.) edition of this book, which now includes detailed applications to various popular logic puzzles.

 © Denis Berthier. All the material in this page and the pages it gives access to are the property of the author and may not be re-published or re-posted without his prior written permission.

    "Constraint Resolution Theories" introduces a pure logic (non algorithmic) perspective of the finite Constraint Satisfaction Problem (CSP), with emphasis on finding the "simplest" solution. Based on constructive logic, the resolution paradigm relies on the notion of a resolution rule: a logical formula in the condition-action form, where the condition is a pattern that has to be present in the current resolution state to justify the elimination of a candidate (i.e. a possible value of a CSP variable) in the action part. Defining a resolution theory as a fixed set of resolution rules, the book introduces several increasing sequences of such theories. Each of them carries its own notion of simplicity and allows to define a rating of CSP instances; it satisfies two main theorems: the confluence property (guaranteeing that the associated rating has good computational properties) and a correspondence with a form of structured search procedure without guessing (Trial-and-Error).

    The book includes a detailed case study of Sudoku with: counter-examples to questions about rules subsumption; unbiased statistics and classification results for the rating of instances; scope comparisons for various resolution theories. Other examples from n-Queens show that the same abstract pattern can appear in various guises in different CSPs.

Contents (pdf)

Introduction (pdf)
 
Final Remarks (pdf)

More results about the Sudoku CSP  (abstracts from and supplements to "The Hidden Logic of Sudoku")


Errata:
p. 202: S0 = BRT(CSP)
p. 202: Sn+1 = Sn + {rules for non degenerated Subsets of size n+1}
p. 203: W0+S0 = BRT(CSP)
p. 289, in the third last condition in the definition of a bi-whip[n]: replace the two occurrences of Vm by Vn
p. 289, after the first "Definition", read: "a bi-braid[n]" instead of: "a bi-Bn-braid"
p. 290: in the definition of a W-whip, replace all the occurrences of subscript n by subscript m.