CONSTRAINT RESOLUTION THEORIES
As I have mentioned long ago, most of what I have done for Sudoku can be generalised to any finite Constraint Satisfaction Problem (CSP). I have already given references to a few papers I've published on this topic. In the past few months and thanks to summer holidays, I had a little time to develop these ideas more extensively and in a more systematic way than can be done on a forum and I've now published a new book: "Constraint Resolution Theories" (
CRT in the sequel) about advanced resolution rules meaningful for any CSP.
Details about
CRT can be found on the part of my website dedicated to it:
http://www.carva.org/denis.berthier/CRT/ (permanent URL).
The following chapters are available in pdf format:
- table of contents:
http://www.carva.org/denis.berthier/CRT/ToC.pdf,
- introduction:
http://www.carva.org/denis.berthier/CRT/ch01-Introduction.pdf,
- final remarks:
http://www.carva.org/denis.berthier/CRT/ch12-Final-Remarks.pdf.
A third of
CRT is about the application of the general theory to Sudoku; there are also examples from n-Queens to illustrate how whips or Subsets can look in a different CSP.
I've been striving to make an electronic version; but I'm still having some trouble with the epub format.
WARNING: Being more general, the approach in this new book is also in some places more abstract and/or more formal than my previous book on Sudoku (
HLS). In particular, it includes detailed proofs of confluence.
I tried to make it self-contained by introducing basics in logic. Also, the chapters on concrete resolution rules (whips, ...) can be read without reading those on formal logic and the general resolution framework. But self-containment is seldom a fully achievable goal.
For the readers of
HLS or for those who have read my posts on this forum, here are a few indications about
how CRT is related to HLS :
1) About the general frameworkThe general formal logic framework introduced in
CRT, when applied to Sudoku, is globally the same as in
HLS. Only two slight differences appear: I now use Gentzen’s “natural logic†instead of Hilbert’s axioms; and, when dealing with the resolution states (formerly called “knowledge states†in
HLS), I refer to modal logic (the logic of necessitation) instead of epistemic logic (or logic of knowledge). None of these changes has any practical consequences; in particular, resolution theories should still be understood as theories in intuitionistic (or constructive) logic.
The definition of a resolution theory was slightly less precise in
HLS.
But the main difference with
HLS is that Sudoku is now considered as a CSP in a more systematic way than it was there; in particular:
- the cells in the Extended Sudoku Board are now explicitly interpreted as representations of CSP variables;
- the nrc notation introduced in
HLS2 as a convenient way of representing chains/whips/braids, now appears as an obvious special case of a natural notation for any CSP;
- basic interactions (“pointing†and “claimingâ€) are systematically written as instances of whip[1];
- Subsets rules are first formulated in a general way, meaningful for any CSP, in terms of CSP variables and transversal sets, before being re-expressed for Sudoku in the usual terms of numbers, rows, columns and blocks; Naked, Hidden and Super-Hidden (Fish) Subsets are not only related by symmetry as they were in
HLS; from the CSP point of view, they are now the very same rule, because the symmetries have been used at a higher level to introduce new CSP variables; (of course, this does not change anything for all practical purposes);
- the main change brought by this new perspective of Subsets is, it allows to introduce their “grouped†version (g-Subsets) as a natural generalisation (in the same way as several chain patterns have a grouped version) and to re-interpret the well-known Franken and Mutant Fish as g-Subsets.
2) New resolution rules and new ratings For the parts of
CRT specifically dedicated to the Sudoku CSP, they are very far from constituting a third edition of
HLS (none of the examples, specialised versions of resolution rules or independence theorems present in
HLS2 has been reproduced in
CRT). Indeed, these parts start where
HLS2 ended.
I first introduced most of the following patterns, resolution rules and/or topics (that were not in
HLS2) on this Forum in 2008. But in
CRT, most of them are now presented in the more general CSP framework (with a somewhat different, simpler terminology - see below):
- whips (which are a more synthetic view of both nrczt- chains and lassoes);
- braids, with a detailed proof of the confluence property of braid resolution theories;
- definition of the Trial-and-Error procedure (T&E) and proof of the “T&E vs braids†theorem;
- definition of the controlled bias generator; comparison of various kinds of generators; unbiased statistics for the W rating for a much larger sample than in
HLS; [detailed numerical results about the number of puzzles solved by each type of rule had been given in
HLS, but they were still based on the biased samples produced by the currently available generators];
- g-whips and g-braids; proofs of the associated confluence property and “gT&E vs g-braids†theorem;
- detailed subsumption theorems for whips and braids, showing that they capture “almost all†but not all the cases of Subset rules;
- Reversible Sp-chains, obtained by allowing the insertion of Subsets as right-linking objects in bivalue chains; proof that these chains are the same thing as grouped AICs or Nice Loops (but my definition does not involve the notion of a “restricted commonâ€); proof of the confluence property for the associated resolution theories;
- S
p-whips and S
p-braids, obtained by allowing the insertion of Subsets as right-linking objects in whips and braids; proofs of the associated confluence property and “T&E(S
p) vs S
p-braids†theorem; analysis of their scope;
- gS
p-Subsets, the “grouped†version of Subsets, a generalisation allowed by considering Subset patterns (S
p-subsets) from the general CSP point of view; they provide a new view of Franken and Mutant Fish;
- Reversible gS
p-chains, gS
p-whips and gS
p-braids, obtained by allowing the insertion of g-Subsets of maximum size p as right-linking objects in bivalue chains, whips and braids;
- W
p-whips and B
p-braids, obtained by allowing the insertion of whips / braids of maximal length p as right-linking objects in whips / braids; proofs of the associated confluence property and “T&E(B
p) vs B
p-braids†theorem;
- relation of B-braids with T&E(2), providing a finite BB rating for all the known minimal puzzles (including the recent ones generated by eleven).
3) New terminologyWith the introduction of rules with embedded patterns, the terminology I used in
HLS and on this forum was becoming more and more cumbersome. Here are the correspondences between the new one and the old one. I write them only for whips; of course, there are similar ones for braids.
Patterns:whips......nrczt-whips
g-whips......whips(BI)
S
p-whips......nrczt-whips(Subsets-p)
W
p-whips......nrczt-whips(Whips[p])
Ratings:W......pure nrczt rating
gW......pure nrczt-whip(BI) rating
S......Subsets rating
S+W......nrczt rating
SpW......nrczt-whip(Sp) rating
WpW......nrczt-whip(Wp) rating
BB......nrczt-braid(nrczt-braid) rating
