The New Sudoku Players' Forum

[denis_berthier]

Pattern-Based Constraint Satisfaction and Logic Puzzles

This is to announce the publication of my new book "Pattern-Based Constraint Satisfaction and Logic Puzzles".

This book develops a pure logic, pattern-based perspective of solving the finite Constraint Satisfaction Problem (CSP), with emphasis on finding the "simplest" solution.
It is the second, revised and largely extended edition of my previous book, "Constraint Resolution Theories". It relies on the same generalization to any finite Constraint Satisfaction Problem of the rules I first developed for Sudoku in "The Hidden Logic of Sudoku". As always in my approach, different ways of reasoning with the constraints are formalised by various families of "resolution rules", each of them carrying its own notion of simplicity.

A large part of this book is devoted to illustrating the power of the approach by applying it to various popular logic puzzles. It provides a unified view of how to model and solve them, even though they involve very different types of constraints: obvious symmetric ones in Sudoku, non-symmetric but transitive ones (inequalities) in Futoshiki, topological ones in Map colouring, either topological or geometric ones in Numbrix and Hidato, and even much more complex non-binary arithmetic ones in Kakuro. It also shows that the most familiar techniques for these puzzles can indeed be understood as mere application-specific presentations of the general rules.

Sudoku is used as the main example throughout the book, making it also an advanced level sequel to "The Hidden Logic of Sudoku", with: many examples of relationships among different rules and of exceptional situations; comparisons of the resolution potential of various families of rules; detailed statistics of puzzles hardness; analysis of extreme instances, i.e. of instances in T&E(2), and special rules for them.

More information about the book can be obtained at http://www.carva.org/denis.berthier/PBCS
In particular, you can download pdf versions of the Foreword, the Introduction and the Final Remarks.
The book is currently available only with my usual online publisher: Lulu.com (http://www.lulu.com/shop/denis-berthier/pattern-based-constraint-satisfaction-and-logic-puzzles/paperback/product-20516172.html), but it should be available on Amazon and other distributors in a few weeks.


What I plan to do in this thread is to highlight (shortly - I don't plan to re-write the book) the main advances I made since the publication of The Hidden Logic of Sudoku (Second Edition).

[denis_berthier]

Application to Sudoku, N-Queens, Futoshiki, Kakuro, Map colouring, Numbrix and Hidato


Perhaps the most visible advance since "The Hidden Logic of Sudoku (Second Edition)" is the generalisation of the chain patterns I introduced for Sudoku (whips, braids, g-whips, g-braids, S-whips, S-braids, ...) to any finite Constraint Satisfaction Problem. The generalisation includes the definitions and the general theory: the confluence property of all the T-braid resolution theories and the the simplest-first strategy it justifies, the "T&E(T) vs T-braids" theorem and the subsumption theorems.
All this was already described in several publications, including my previous book ("Constraint Resolution Theories" - CRT). But, apart from N-Queens, I hadn't yet explored in detail any radically different logic puzzle.

This is now done with "Pattern-Based Constraint Satisfaction and Logic Puzzles". In order to explore the practical consequences of the generalisation, I have chosen a set of logic puzzles with very different types of constraints: Sudoku, N-Queens, Futoshiki, Kakuro, Map colouring, Numbrix and Hidato and devoted a full chapter to each of them.

The resolution rules initially developed for Sudoku apply straightforwardly to all these puzzles. And this is true not only at an abstract logic level, but also at the implementation level of my general CSP-Rules solver.
The method of using redundant sets of CSP variables is also essential in all these puzzles. Recall that, in Sudoku, it consists of considering not only the "natural" 81 rc-cells but also the rn-, cn- and bn- cells, leading to a total of 324 CSP-variables. This extended set of CSP variables is represented by the Extended Sudoku Board first introduced in HLS.

Moreover, the experimental results tend to confirm those I obtained for Sudoku:
- in all these cases, whips have a very high resolution power,
- when whips and braids are activated, with whips given a higher priority than braids of same length, braids seldom appear in the resolution paths,
- g-whips are also a very general and useful pattern,
- Subsets are much weaker than whips of same size,
- when the W rating is finite, adding Subsets, g-whips, braids and/or g-braids very rarely changes the rating.

I write "tend to confirm", because, for lack of available generators for these puzzles, I had to rely on the instances I found on the Web and I can't give detailed statistical analyses as I did for Sudoku (anyway, I would probably have been too lazy to monitor again the same type of long calculations). Copying the instances from a web page and writing them in the proper format to feed CSP-Rules is very time-consuming, so that I could analyze only a few hundred instances for each type of puzzle. But, apart from a few trial cases, I systematically chose the hardest ones I could find on each website ("hardest" according to its own classification) and for each puzzle type I chose from different websites.
Finally, I think these results have some general degree of validity.

[denis_berthier]

Ratings, hard instances and patterns of proof


In "The Hidden Logic of Sudoku (Second Edition)", I had only the W classification of instances for a top-down generator. Later, we found that these generators have a strong bias. In "Constraint Resolution Theories", I published an unbiased classification, obtained with the controlled bias generator. For harder puzzles, I also had the Sp-braid classification of the known ones at that time.

"Pattern-Based Constraint Satisfaction and Logic Puzzles" now has the full B?B classification of all the (currently known) hardest puzzles. It shows that all these puzzles are in B7B, i.e. can be solved with B7-braids, which considerably re-enforces my old T&E(2) conjecture: all the 9x9 puzzles can be solved by at most 2 levels of T&E.

However, B-braids are complex patterns. I have defined another pattern B*-braids, relying on bi-braids.
A bi-braid is structurally much like a braid, except that:
- it is built on two candidates z1 and z2 instead of one
- and it concludes on their contradiction instead of its elimination.
Exists-bi-braid(z1, z2) is thus a constructive version of the general logical predicate nand(z1, z2) defined by not (and (z1, z2)).

Now, a B*-braid is defined like a braid, except that all the links between the target, left-linking, z- and t-candidates can be bi-braids instead of the direct elementary contradictions. Of course, it allows elimination of its target.

On the positive side of things, I have shown that being in T&E(2) is equivalent to being solvable by B-braids (my old T&E(2) vs B-braid theorem), but also that it is equivalent to being solvable by B*-braids. Moreover, it is equivalent to being solvable by B*-braids[1], which could also be called forcing bi-braids. As a result, if one "forgets" the complexity of the indirect contradictions (the inner bi-braids), any 9x9 puzzle can be solved by a pattern (a B*-braid) of pseudo-length one.

Of course, on the negative side of things, using such indirect contradictions as if they were elementary ones is cheating with complexity if one merely compares the pseudo-length of a B*-braid (that doesn't take into account the lengths of its inner bi-braids) with the length of a braid or a B-braid.

Although I've never seen any clear description of tagging, this should shed some light on what tagging is about: a calculation of some binary contradictions, i.e. a partial (in undefined ways) use of bi-braids as if they were ordinary links.


Global patterns of proof

These results raise the question of the global pattern of proof of a resolution path. I've dedicated a full chapter of "Pattern-Based Constraint Satisfaction and Logic Puzzles" to this topic.
Beware, here I'm not speaking of the pattern in the left-hand side of a resolution rule - this is a local pattern (chain, subset, ...) leading to some elimination(s). I'm speaking of the global resolution path.
The following is interesting mainly for puzzles in T&E(2), as a braids solution is available for those in T&E(1) .

In the usual approach, the resolution path is a sequence of assertions (A) and eliminations (E). Let us note it in the standard form of (E | A)* , where "|" means "one of" and "*" means any number of repetitions.

What B*-braids amount to is accepting another global pattern of proof that allows a third type of step: B (for bi-braid contradictions). The global pattern of proof becomes: (E | A | B)*.
Thus written, the difference may seem innocuous. But is has drastic consequences.
From a logical point of view, one can consider the A and E steps of the resolution path as theorems in the theory of the puzzle under consideration: such and such value is necessary/impossible. Allowing B steps amounts to allowing lemmas that will be used during the proofs of the theorems. One major question is: how does one count the complexity of these steps in the rating of a puzzle?

Indeed, this was the high level view. In practice, inner bi-braids may be limited to some predefined length and there can be some interplay between their length and that of the B*-braids. There are many different possibilities for regulating both types of lengths, but none that seems to be naturally preferable:
- I've already mentioned one with bi-braids of unrestricted length leading to a solution with only B*-braids[1];
- on the opposite side, one may look for a solution with the shortest possible inner bi-braids;
- one can also ask bi-braids and B*-braids to have the same max length,
- ...
Solutions based on B*-braids should therefore always make it clear which kind of combination is chosen.

[denis_berthier]

free pdf version

I've been asked many times to provide an electronic version of this book. I tried to do it in the epub format, but that was impossible (the epub format doesn't allow any reasonable formatting).

Therefore, I've finally decided to make a full pdf version available on my website: http://www.carva.org/denis.berthier/PBCS
and here http://arxiv.org/abs/1304.1628