The Hidden Logic of Sudoku

The Hidden Logic of Sudoku

A new conceptual framework for solving Sudoku puzzles with pure logic

Denis Berthier

First edition: May 2007

Second edition: November 2007

Online Supplements

On the notion of a strong T-backdoor
and its application to Easter Monster

© 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.

EasterMonster (EM) is one of the most famous puzzles.
Discovered by JPF and published the 7th of April 2007 on the Sudoku Payer's Forum, it has long been considered as the hardest puzzle and it is still considered as one of the few hardest known puzzles:

100 090 006	000 400 000	002 050 700
050 000 000	903 070 850	000 000 040
700 030 002	000 009 000	600 080 001

In "The Hidden Logic of Sudoku" (HLS), I indicated that EasterMonster cannot be solved by any known set of resolution rules.
Of course, like any puzzle, it can always be solved using Recursive Trial and Error with Guessing (RTEG).

One question that arises for such exceptionally hard puzzles is: if we disallow guessing, can we somehow focus the Trial and Error search ?
In order to answer this question, I introduced the notion of a strong T-backdoor.

This was not included in HLS because it concerns exceptionnally hard puzzles, which I think are out of reach of a human solver.

1) THE NOTION OF A STRONG T-BACKDOOR

Remember the classical notion of a (singles) backdoor: a set D of different entries forms a (singles) backdoor for a puzzle P if, when the elements in D are added as entries to P, the puzzle thus obtained can be solved using only singles.

This notion can be extended in two directions.

First, there is the well known extension to any resolution theory T (i.e. to any set T of resolution rules): one says that a set D of k different entries forms a T-backdoor of size k for a puzzle P if:
- P can be solved within T (i.e. using only the rules in T, in particular without adding any explicit or disguised form of Trial and Error) after the k elements of D have been added to the entries of P,
- and no strict subset of D has this property.
The T-backdoor size of a puzzle P is the minimum k such that P has a T-backdoor of size k.

The usual notion of a backdoor is obtained with T = {rules for Singles (Naked or Hidden)}

It is known that EasterMonster has Singles-backdoor size 3. It was indeed the first example of a puzzle with Singles-backdoor size 3. Before, it was conjectured that the maximum Singles-backdoor size was 2. We now know a little dozen of puzzles with Singles-backdoor size 3.

In the sequel, I shall use the set of rules defined in HLS.
Let T0 = "the elementary rules" =
    {the elementary constraints propagation rules}
    + {the rules for elementary interactions between rows/columns and blocks}
     + {the rules for Singles, Pairs, Triplets, Quads - Naked, Hidden or Super-Hidden}
     (+ {XY-Wing, XYZ-Wing} )
(If XY-Wing and XYZ-Wing are present, this is called L4_0 in "The Hidden Logic of Sudoku". Putting these rules here or not is irrelevant for the definition of NRCZT, which subsumes them).

Let NRCZT = T0 + {the rules for nrczt whips}. Notice that no a priori length limit is put on the whips in NRCZT.

It can be shown that EasterMonster has (at least) the following NRCZT-backdoors of size 1: {r6c2=6} et {r9c6=6}. (I haven't checked if there are any others. For the first backdoor, see the proof below).
Moreover EasterMonster cannot be solved in NRCZT.
Therefore EasterMonster has NRCZT-backdoor size 1.
I conjecture that the maximal NRCZT-backdoor size for any puzzle is 1.
In the sequel, I shall concentrate on the following NRCZT-backdoor: {r6c2=6} is an NRCZT-backdoor for EasterMonster.

The problem with this notion of a T-backdoor is that it doesn't seem to be strong enough to give precise indications on the complexity of the initial puzzle, because it doesn't suppose that the elements in D can be proven in a well defined manner based on the rules in T. Said otherwise, proving that a backdoor is true may be as hard as solving the initial puzzle. Worse, there is no indication that trying to prove the backdoor is the simplest way for solving the puzzle. I therefore propose the following stronger definition.

First, given any candidate nrc, it may be the case that the truth of nrc cannot be proven in T, but that at least one of the following four cases is true:
- for any candidate n'rc with n'≠n (same rc-cell, different value), it can be proven in T that adding n'rc to the entries of P leads to a contradiction,
- for any candidate nrc' with c'≠c (same rn-cell, different column), it can be proven in T that adding nrc' to the entries of P leads to a contradiction,
- for any candidate nr'c with r'≠r (same cn-cell, different row), it can be proven in T that adding nr'c to the entries of P leads to a contradiction,
- for any candidate nr'c' with r'c'≠rc and in the same block as nrc (same bn-cell, different square in the block), it can be proven in T that adding nr'c' to the entries of P leads to a contradiction.
In this case, we shall say that nrc (or rc=n) can be proven in T plus "depth one Trial-and-Error(T) focused on nrc".

Remarks:
- this definition respects the super-symmetries of Sudoku (this wouldn't have been the case if we had restricted the definition to the first case among the four above);
- as the truth of nrc cannot be proven in T, this seems to be the best one can hope if one doesn't use rules not in T and one considers that D must play a central role in the solution.

Definition: a set D of k different data forms a strong T-backdoor of size k for a puzzle P if:
1) D forms a T-backdoor for P (in the sense defined above),
2) for any element rc=n in D, rc=n can be proven in T plus "depth one Trial-and-Error(T) focused on nrc".

It can be shown that {r6c2=6} is NOT a strong NRCZT-backdoor for EasterMonster.

This should be compared to the following result: EasterMonster can be solved in NRCZT plus "depth one Trial-and-Error(NRCZT)", where "depth one Trial-and-Error(T)" means there is a set E of candidates such that:
- it can be proven within T that each element of E, when added (separately) to the entries of P leads to a contradiction;
- P + {not nrc / for all the nrc in E} can be soved within T.

As a result, it may seem that using known backdoors for focusing the search for a solution is not a good idea and that this notion is useless. (Using extra information on a puzzle is always debatable, but in the present case it may also be useless). But see section II.

Each of the following additional candidates separately leads to an NRCZT contradiction, i.e. each of these contradictions can be independently proven within NRCZT: n8r2c1, n8r2c3, n6r4c1, n6r5c1, n1r6c2, n2r6c2, n4r7c2, n7r9c6, n1r4c8, n2r4c8, n6r4c8, n6r6c9.
Remarks:
- this list is not exhaustive; I haven't tried all the candidates, only a few that I felt might lead to something interesting;
- the proofs are of very different complexities (n7r9c6 requires nrczt18 lassos, n2r6c2 requires nrczt15 lassos, whereas n1r6c2 is done with nrczt7 lassos). 18 is the maximum length used in these proofs.

Eliminating the subset {n1r6c2 n2r6c2 n8r2c3 n7r9c6 n8r2c1 n1r4c8 n2r4c8 n6r4c8 n6r4c1} of the above list from the EM candidates is enough for solving EasterMonster in NRCZT12. (I haven't tried with other subsets, so this may not be the smallest). This entails that EasterMonster can be solved in NRCZT plus "depth one Trial-and-Error(NRCZT)".

Now, what do I want to do with backdoors? If I'm given a backdoor, I don't have a full proof of the solution. I consider the backdoor as an oracle (comprarable to the information on uniqueness) that I accept as a guide in my search for the solution but that I don't accept as a proof of it - as everybody knows, oracles are not always very trustworthy ;)
Suppose I want to find (and prove) the solution for EM using rules in some theory T (e.g. NRCZT). If EM could be solved entirely within T, I wouldn't care about backdoors. But this is not the case. (Remember this problem occurs only for the exceptionally hard puzzles, since NRCZT can solve 99,99% of the minimal puzzles - that's why I take EM as an example).
Suppose I know that n6r6c2 is a T'-backdoor for some theory T' (e.g. gsf's system). I'm not interested in T' but in T, which is "close" to T' (in some imprecise sense) and I'm able to prove within T that EM+n6r6c2 is also a T-backdoor. This means I've solved (not EM but) EM+n6r6c2 within T.
But I haven't yet solved EM: I still have to prove n6r6c2. As n6r6c2 can't be proven within T, I have to use T&E (or to define new rules and extend T, but that's another matter).
The notion of a strong T-backdoor is a natural one if I want to take advantage of the oracle for focusing this unavoidable use of T&E (the number of candidates that may be considered for T&E is a priori so big that some rational focusing should be useful).

The conclusion of this section may be over pessimistic about strong T-backdoors. It shows that n6r6c2 is an NRCZT-backdoor but not a strong NRCZT-backdoor for EasterMonster (EM). Combined with the fact that EM can be solved with depth-one T&E(NRCZT), this may leave the impression that the notion of a strong T-backdoor, a priori interesting for guiding the search for a proof of the solution, is useless in practice. I'll now show that it can indeed be useful.

2) THE PRACTICAL USEFULNESS OF THE NOTION OF A STRONG T-BACKDOOR

Stephen Kurhzhals has found a loop of subsets that allows a few eliminations on EM. I shall not state the rule here (indeed, the precise rule has never been stated formally; different interpretations of these eliminations have been given, see mine here).
I shall just list these eliminations and use them as such:
n7r1c3, n3r2c5, n8r2c5, n8r2c6, n2r3c, n4r5c2, n8r5c2, n3r5c8, n9r5c8, n5r8c4, n1r7c3, n4r8c5, n6r9c1
Let EasterMonster+Steve (or EMS) be EasterMonster (or EM) after Steve's rule has been applied and the associated eliminations done.

I shall now show that n6r6c2 is a strong NRCZT-backdoor for EasterMonster+Steve.

Another, weaker, way of stating this is as follows.
Let SR be Steve's rule - whatever it is. Let's say SR is the weakest rule that justifies Steve's eliminations.
Then n6r6c2 is a strong (NRCZT+SR)-backdoor for EasterMonster.
This statement is weaker than the first, because in the first statement, SR is used only once, whereas in the second it is a priori allowed to be used as often as necessary.

The proof goes as follows (remember that the candidates for cell r6c2 are n1 n2 n6 n7):
- n6c6r2 is an NRCZT-backdoor for EasterMonster;
- EM+n1r6c2 (and therefore also EMS+n1r6c2) can be shown within NRCZT to lead to a contradiction;
- EM+n2r6c2 (and therefore also EMS+n1r6c2) can be shown within NRCZT to lead to a contradiction;
- EMS+n7r6c2 (but not EM+n7r6c2) can be shown within NRCZT to lead to a contradiction.

The following four sections will give the details of these 4 proofs. The practical meaning of all this is that, after Steve's eliminations have been done, we can solve EM with only 3 eliminations by T&E focused on n6r6c2.

2.1) Firstly, n6r6c2 is an NRCZT-backdoor for EM

(solve-sdk-grid (str-cat ?*PuzzlesDir* "Monsters/EasterMonster/EasterMonster+n6r6c2.sdk"))
***** SudoRules version 13.7wter *****
1.......2.9.4...5...6...7...5.9.3.......7.....6.85..4.7.....6...3...9.8...2.....1
singles ==> r1c2 = 7, r2c6 = 7
nrczt-whip[2] b5n6{r5c6 r4c5} - r2n6{c5 .} ==> r5c9 <> 6
nrczt-whip[4] r8n1{c5 c3} - r6n1{c3 c7} - r4n1{c8 c5} - r2n1{c5 .} ==> r7c6 <> 1
nrczt-whip[5] r2n1{c5 c7} - r6n1{c7 c3} - r6n7{c3 c9} - r8n7{c9 c4} - r8n1{c4 .} ==> r4c5 <> 1
nrczt-whip[6] c2n2{r5 r3} - b2n2{r3c6 r2c5} - r2n6{c5 c9} - b6n6{r4c9 r4c8} - c8n1{r4 r3} - b2n1{r3c6 .} ==> r5c8 <> 2
nrczt-whip[6] r2n6{c5 c9} - r4n6{c9 c8} - c8n7{r4 r9} - c4n7{r9 r8} - r8n2{c4 c7} - b6n2{r4c7 .} ==> r8c5 <> 6
nrczt-whip[7] r9c2{n4 n8} - r7c2{n8 n1} - r8c3{n1 n5} - r8c7{n5 n2} - c8n2{r7 r4} - c8n7{r4 r9} - r8c9{n7 .} ==> r8c1 <> 4
nrct-chain[7] r8c1{n6 n5} - b1n5{r3c1 r1c3} - r1n4{c3 c7} - r8c7{n4 n2} - c8n2{r7 r4} - c8n7{r4 r9} - c4n7{r9 r8} ==> r8c4 <> 6
hidden-single-in-row r8 ==> r8c1 = 6
nrczt-whip[7] r6n7{c3 c9} - r8n7{c9 c4} - r8n1{c4 c5} - r8n2{c5 c7} - c8n2{r7 r4} - r4n1{c8 c7} - r2n1{c7 .} ==> r6c3 <> 1
nrc-chain[2] b3n1{r3c8 r2c7} - r6n1{c7 c6} ==> r3c6 <> 1
interaction column c6 with block b5 for number 1 ==> r5c4 <> 1
nrczt-whip[4] r2n2{c1 c5} - r2n1{c5 c7} - r6n1{c7 c6} - b5n2{r6c6 .} ==> r5c1 <> 2
nrczt-whip[5] b2n2{r3c6 r2c5} - r2n1{c5 c7} - r6n1{c7 c6} - r6n2{c6 c7} - r4n2{c8 .} ==> r3c1 <> 2
nrczt-whip[5] c2n2{r5 r3} - b2n2{r3c6 r2c5} - r2n1{c5 c7} - r6n1{c7 c6} - b5n2{r6c6 .} ==> r5c7 <> 2
nrct-chain[7] r5c4{n6 n2} - c2n2{r5 r3} - c6n2{r3 r7} - c8n2{r7 r4} - c5n2{r4 r2} - r2n1{c5 c7} - b6n1{r6c7 r5c8} ==> r5c8 <> 6
interaction row r5 with block b5 for number 6 ==> r4c5 <> 6
hxyzt-rn-chain[5] r4n6{c8 c9} - r2n6{c9 c5} - r2n1{c5 c7} - r4n1{c7 c3} - r4n7{c3 c8} ==> r4c8 <> 2
hidden-single-in-column c8 ==> r7c8 = 2
nrczt-whip[2] c2n2{r5 r3} - c6n2{r3 .} ==> r5c4 <> 2
naked-single ==> r5c4 = 6
hxyt-cn-chain[4] c4n2{r8 r3} - c2n2{r3 r5} - c2n1{r5 r7} - c4n1{r7 r8} ==> r8c4 <> 7
singles ==> r9c4 = 7, r8c9 = 7, r4c8 = 7, r6c3 = 7, r4c9 = 6, r1c8 = 6, r2c5 = 6, r9c6 = 6, r2c7 = 1, r5c8 = 1, r4c3 = 1, r7c2 = 1, r6c6 = 1, r2c1 = 2,r5c2 = 2, r5c6 = 4, r4c5 = 2, r4c7 = 8, r4c1 = 4, r8c4 = 2, r3c6 = 2, r8c5 = 1, r3c4 = 1, r3c1 = 5, r9c7 = 5, r8c7 = 4, r8c3 = 5, r3c9 = 4, r3c2 = 8, r2c3 = 3, r1c3 = 4, r2c9 = 8, r9c2 = 4, r7c5 = 4, r5c9 = 5, r6c7 = 2
x-wing-in-rows n3{r3 r9}{c5 c8} ==> r1c5 <> 3
nrc-chain[2] c3n9{r7 r5} - r6n9{c1 c9} ==> r7c9 <> 9
…(Naked and Hidden Singles)…
GRID EasterMonster+n6r6c2 SOLVED. LEVEL = NRCZT7, MOST COMPLEX RULE = NRCZT7
174385962
293467158
586192734
451923876
928674315
367851249
719548623
635219487
842736591

2.2) Secondly, EM+r6c2=1 is IMPOSSIBLE

(solve-sdk-grid (str-cat ?*PuzzlesDir* "Monsters/EasterMonster/EasterMonster+n1r6c2.sdk"))
***** SudoRules version 13.7wter *****
1.......2.9.4...5...6...7...5.9.3.......7.....1.85..4.7.....6...3...9.8...2.....1
singles ==> r1c2 = 7, r2c6 = 7
nrczt-whip[2] b5n1{r5c6 r4c5} - r2n1{c5 .} ==> r5c7 <> 1
nrczt-whip[4] c2n6{r9 r5} - c4n6{r5 r1} - r2n6{c5 c9} - r6n6{c9 .} ==> r9c6 <> 6
nrczt-whip[6] c2n2{r5 r3} - b2n2{r3c6 r2c5} - r2n6{c5 c9} - b6n6{r6c9 r4c8} - c8n1{r4 r3} - b2n1{r3c6 .} ==> r5c8 <> 2
nrczt-whip[6] r2n1{c5 c7} - r4n1{c7 c8} - c8n7{r4 r9} - c4n7{r9 r8} - r8n2{c4 c7} - b6n2{r4c7 .} ==> r8c5 <> 1
nrczt-whip[7] c3n1{r8 r7} - b7n9{r7c3 r9c1} - b7n5{r9c1 r8c1} - r8c7{n5 n2} - c8n2{r7 r4} - c8n7{r4 r9} - r8c9{n7 .} ==> r8c3 <> 4
nrczt-whip[7] c8n2{r7 r4} - r6n2{c7 c1} - r2n2{c1 c5} - r2n6{c5 c9} - b6n6{r6c9 r5c8} - c8n1{r5 r3} - b2n1{r3c6 .} ==> r7c6 <> 2
nrczt-whip[2] c2n2{r5 r3} - c6n2{r3 .} ==> r5c4 <> 2
nrct-chain[5] r5c4{n1 n6} - c6n6{r5 r1} - c8n6{r1 r4} - c8n7{r4 r9} - c4n7{r9 r8} ==> r8c4 <> 1
hidden-single-in-row r8 ==> r8c3 = 1
nrczt-whip[6] c2n6{r9 r5} - c2n2{r5 r3} - b2n2{r3c6 r2c5} - r8c5{n2 n4} - r4c5{n4 n1} - r5c4{n1 .} ==> r9c5 <> 6
nrczt-whip[5] c4n7{r8 r9} - c8n7{r9 r4} - c8n2{r4 r7} - r8n2{c7 c5} - b8n6{r8c5 .} ==> r8c4 <> 5
nrczt-whip[7] r1n4{c7 c3} - b1n5{r1c3 r3c1} - r8c1{n5 n6} - r8c5{n6 n2} - c4n2{r7 r3} - c2n2{r3 r5} - c2n6{r5 .} ==> r8c7 <> 4
nrczt-whip[7] r5c4{n1 n6} - c6n6{r6 r1} - c8n6{r1 r4} - c8n7{r4 r9} - c4n7{r9 r8} - c4n2{r8 r7} - c8n2{r7 .} ==> r3c4 <> 1
nrczt-whip[7] c6n6{r5 r1} - c8n6{r1 r4} - c8n7{r4 r9} - c4n7{r9 r8} - b8n6{r8c4 r8c5} - r8n2{c5 c7} - c8n2{r7 .} ==> r5c4 <> 6
naked-single ==> r5c4 = 1
nrc-chain[6] r2n6{c9 c5} - r2n1{c5 c7} - r4n1{c7 c8} - c8n2{r4 r7} - r8c7{n2 n5} - b6n5{r5c7 r5c9} ==> r5c9 <> 6
nrczt-whip[6] c2n2{r5 r3} - b2n2{r3c6 r2c5} - r2n1{c5 c7} - c8n1{r3 r4} - c8n6{r4 r1} - r2n6{c9 .} ==> r5c2 <> 6
hidden-single-in-column c2 ==> r9c2 = 6
nrc-chain[5] r8n6{c5 c4} - r8n7{c4 c9} - c8n7{r9 r4} - r4n1{c8 c7} - r2n1{c7 c5} ==> r2c5 <> 6
hidden-single-in-row r2 ==> r2c9 = 6
nrct-chain[5] b6n1{r4c7 r4c8} - c8n7{r4 r9} - r8n7{c9 c4} - r8n6{c4 c5} - r8n2{c5 c7} ==> r4c7 <> 2
nrczt-whip[3] b9n2{r8c7 r7c8} - r4n2{c8 c1} - r2n2{c1 .} ==> r8c5 <> 2
hxyt-rn-chain[4] r2n2{c1 c5} - r2n1{c5 c7} - r4n1{c7 c8} - r4n2{c8 c1} ==> r6c1 <> 2, r5c1 <> 2, r3c1 <> 2
nrc-chain[4] c8n7{r4 r9} - r8n7{c9 c4} - r8n2{c4 c7} - c8n2{r7 r4} ==> r4c8 <> 6
hidden-single-in-block b6 ==> r5c8 = 6
nrc-chain[3] b4n2{r5c2 r4c1} - b4n6{r4c1 r6c1} - r6c6{n6 n2} ==> r5c6 <> 2
naked-single ==> r5c6 = 4
nrc-chain[3] r4n4{c3 c1} - r8c1{n4 n5} - c3n5{r7 r1} ==> r1c3 <> 4
hidden-single-in-row r1 ==> r1c7 = 4
nrc-chain[3] r9n4{c1 c5} - r8c5{n4 n6} - r4n6{c5 c1} ==> r4c1 <> 4
singles ==> r4c3 = 4, r6c3 = 7
xy-chain[4] r5c2{n2 n8} - r7c2{n8 n4} - r8c1{n4 n5} - r8c7{n5 n2} ==> r5c7 <> 2
singles ==> r5c2 = 2, r2c1 = 2
nrc-chain[3] c6n2{r3 r6} - r4n2{c5 c8} - c8n1{r4 r3} ==> r3c6 <> 1
hidden-single-in-column c6 ==> r7c6 = 1
nrc-chain[3] r3n1{c8 c5} - c5n9{r3 r1} - r1c8{n9 n3} ==> r3c8 <> 3
hxy-rn-chain[4] r4n2{c5 c8} - r4n7{c8 c9} - r8n7{c9 c4} - r8n6{c4 c5} ==> r4c5 <> 6
singles ==> r4c5 = 2, r6c6 = 6, r4c1 = 6, r3c6 = 2, r6c7 = 2, r8c7 = 5, r8c1 = 4, r7c2 = 8, r3c2 = 4, r8c5 = 6, r8c9 = 7, r4c9 = 8, r4c7 = 1, r4c8 = 7, r8c4 = 2, r7c8 = 2, r3c8 = 1, r2c5 = 1, r2c7 = 8, r2c3 = 3, r9c4 = 7, r1c4 = 6, r9c5 = 4, r7c5 = 3, r7c4 = 5, r9c6 = 8, r1c6 = 5
GRID EasterMonster+n1r6c2.sdk HAS NO SOLUTION : NO CANDIDATE FOR FOR CN-CELL c3n5
LEVEL = NRCZT7, MOST COMPLEX RULE = NRCZT7

;;; Notice that 41 values must be asserted (in addition to the 19 entries and to r6c2=1) before a contradiction is found.
;;; Notice that the hardest steps use only nrczt-whips of length 7.

2.3) Thirdly, EM+r6c2=2 is IMPOSSIBLE

(solve-sdk-grid (str-cat ?*PuzzlesDir* "EasterMonster/EasterMonster+n2r6c2.sdk"))
***** SudoRules version 13.7wter *****
1.......2.9.4...5...6...7...5.9.3.......7.....2.85..4.7.....6...3...9.8...2.....1
singles ==> r1c2 = 7, r2c6 = 7
nrczt-whip[4] c2n6{r9 r5} - c4n6{r5 r1} - r2n6{c5 c9} - r6n6{c9 .} ==> r9c6 <> 6
nrczt-whip[4] r8n1{c5 c3} - r6n1{c3 c7} - r4n1{c8 c5} - r2n1{c5 .} ==> r7c6 <> 1
nrczt-whip[5] r2n1{c5 c7} - r6n1{c7 c3} - r6n7{c3 c9} - r8n7{c9 c4} - r8n1{c4 .} ==> r4c5 <> 1
nrczt-whip[8] r2n6{c9 c5} - b5n6{r4c5 r6c6} - b4n6{r6c1 r4c1} - r8n6{c1 c4} - r8n7{c4 c9} - r6n7{c9 c3} - r6n1{c3 c7} - r2n1{c7 .} ==> r5c9 <> 6
nrczt-whip[9] r2n6{c5 c9} - r6n6{c9 c1} - r8n6{c1 c4} - c4n7{r8 r9} - c8n7{r9 r4} - r4n2{c8 c7} - r4n1{c7 c3} - r8n1{c3 c5} - r8n2{c5 .} ==> r4c5 <> 6
nrczt-whip[10] b5n1{r5c4 r6c6} - b4n1{r6c3 r4c3} - c8n1{r4 r3} - b2n1{r3c6 r2c5} - r2n6{c5 c9} - r6n6{c9 c1} - r4n6{c1 c8} - r4n7{c8 c9} - r8n7{c9 c4} - r8n1{c4 .} ==> r5c7 <> 1
nrczt-whip[11] b9n2{r8c7 r7c8} - c6n2{r7 r3} - c4n2{r3 r8} - c5n2{r8 r4} - b5n4{r4c5 r5c6} - c6n1{r5 r6} - b5n6{r6c6 r5c4} - c6n6{r5 r1} - c8n6{r1 r4} - c8n7{r4 r9} - c4n7{r9 .} ==> r5c7 <> 2
nrczt-whip[11] r2n6{c9 c5} - r1n6{c6 c8} - r4n6{c8 c1} - r8n6{c1 c4} - r8n7{c4 c9} - r4c9{n7 n8} - r2c9{n8 n3} - r2c3{n3 n8} - c7n8{r2 r1} - b3n4{r1c7 r3c9} - r3c2{n4 .} ==> r6c9 <> 6
nrczt-whip[10] c2n1{r7 r5} - c4n1{r5 r3} - c8n1{r3 r4} - r6n1{c7 c6} - r6n6{c6 c1} - r4n6{c1 c9} - b6n7{r4c9 r6c9} - r8n7{c9 c4} - r8n6{c4 c5} - r2n6{c5 .} ==> r7c5 <> 1
nrczt-whip[11] r1n4{c7 c3} - b1n5{r1c3 r3c1} - r8c1{n5 n6} - c2n6{r9 r5} - c2n1{r5 r7} - r8c3{n1 n5} - r8c9{n5 n7} - r9n7{c8 c4} - c4n6{r9 r1} - c8n6{r1 r4} - c8n7{r4 .} ==> r8c7 <> 4
nrczt-whip[6] c2n6{r9 r5} - c2n1{r5 r7} - r8c3{n1 n5} - c1n5{r9 r3} - r3n4{c1 c9} - b9n4{r7c9 .} ==> r9c2 <> 4
nrczt-whip[9] r1n4{c7 c3} - r3c2{n4 n8} - b2n8{r3c6 r2c5} - r2n1{c5 c7} - r4c7{n1 n2} - r8c7{n2 n5} - c3n5{r8 r7} - b7n9{r7c3 r9c1} - b7n8{r9c1 .} ==> r1c7 <> 8
nrczt-whip[10] r2n2{c1 c5} - r2n6{c5 c9} - b3n8{r2c9 r3c9} - r4c9{n8 n7} - r8n7{c9 c4} - r8n2{c4 c7} - r4n2{c7 c8} - c8n6{r4 r5} - c8n1{r5 r3} - b2n1{r3c6 .} ==> r2c1 <> 8
;;; This is the hardest step:
nrczt-whip[13] r9c2{n6 n8} - r3c2{n8 n4} - r7c2{n4 n1} - r5c2{n1 n6} - c4n6{r5 r1} - c8n6{r1 r4} - c8n7{r4 r9} - c4n7{r9 r8} - r8n1{c4 c5} - r8n2{c5 c7} - c8n2{r7 r5} - c8n1{r5 r3} - b2n1{r3c6 .} ==> r9c5 <> 6
nrczt-whip[7] c4n7{r8 r9} - b8n6{r9c4 r8c5} - b8n1{r8c5 r7c4} - r5c4{n1 n6} - c6n6{r6 r1} - c8n6{r1 r4} - c8n7{r4 .} ==> r8c4 <> 2
nrczt-whip[9] r8n7{c4 c9} - r6n7{c9 c3} - r4n7{c3 c8} - r9n7{c8 c4} - b8n6{r9c4 r8c5} - r8n2{c5 c7} - c8n2{r7 r5} - c8n6{r5 r1} - r2n6{c9 .} ==> r8c4 <> 5, r8c4 <> 1
nrczt-whip[3] r2n1{c7 c5} - r8n1{c5 c3} - r4n1{c3 .} ==> r6c7 <> 1
nrczt-whip[6] r4n1{c7 c3} - r8n1{c3 c5} - r8n2{c5 c7} - c8n2{r7 r4} - r4n7{c8 c9} - b6n6{r4c9 .} ==> r5c8 <> 1
interaction block b6 with row r4 for number 1 ==> r4c3 <> 1
hxyzt-rn-chain[4] r8n2{c5 c7} - r4n2{c7 c8} - r4n1{c8 c7} - r2n1{c7 c5} ==> r2c5 <> 2
hidden-single-in-row r2 ==> r2c1 = 2
nrczt-whip[5] r4n1{c8 c7} - b6n2{r4c7 r5c8} - b6n6{r5c8 r4c9} - r2n6{c9 c5} - r2n1{c5 .} ==> r4c8 <> 7
singles ==> r9c8 = 7, r8c4 = 7
hxy-rn-chain[4] r8n6{c1 c5} - r8n1{c5 c3} - r6n1{c3 c6} - r6n6{c6 c1} ==> r9c1 <> 6, r5c1 <> 6, r4c1 <> 6
interaction row r4 with block b6 for number 6 ==> r5c8 <> 6
hxy-rn-chain[4] r4n6{c8 c9} - r2n6{c9 c5} - r2n1{c5 c7} - r4n1{c7 c8} ==> r4c8 <> 2
x-wing-in-rows n2{r4 r8}{c5 c7} ==> r7c5 <> 2, r3c5 <> 2
hxy-rn-chain[4] r2n6{c5 c9} - r4n6{c9 c8} - r4n1{c8 c7} - r2n1{c7 c5} ==> r2c5 <> 8, r2c5 <> 3
hxy-rn-chain[4] r8n6{c5 c1} - r6n6{c1 c6} - r6n1{c6 c3} - r8n1{c3 c5} ==> r8c5 <> 4, r8c5 <> 2
singles ==> r4c5 = 2, r5c8 = 2, r8c7 = 2, r5c6 = 4
naked-pairs-in-a-column c5{r2 r8}{n1 n6} ==> r3c5 <> 1, r1c5 <> 6
x-wing-in-rows n6{r5 r9}{c2 c4} ==> r1c4 <> 6
nrct-chain[2] c2n4{r3 r7} - r8n4{c3 c9} ==> r3c9 <> 4
hidden-single-in-block b3 ==> r1c7 = 4
nrc-chain[3] c5n1{r2 r8} - b8n6{r8c5 r9c4} - r5c4{n6 n1} ==> r3c4 <> 1
x-wing-in-columns n1{c2 c4}{r5 r7} ==> r7c3 <> 1, r5c3 <> 1
hidden-pairs-in-a-row r5{n1 n6}{c2 c4} ==> r5c2 <> 8
nrc-chain[3] b8n1{r7c4 r8c5} - b2n1{r2c5 r3c6} - c6n2{r3 r7} ==> r7c4 <> 2
singles ==> r7c6 = 2, r3c4 = 2
nrczt-whip[3] c2n8{r7 r3} - r3n4{c2 c1} - r4c1{n4 .} ==> r9c1 <> 8
xyzt-chain[4] r1c4{n5 n3} - r9c4{n3 n6} - r9c2{n6 n8} - r9c6{n8 n5} ==> r7c4 <> 5
interaction block b8 with row r9 for number 5 ==> r9c7 <> 5
hidden-single-in-column c7 ==> r5c7 = 5
interaction block b8 with row r9 for number 5 ==> r9c1 <> 5
naked-pairs-in-a-block b9{r7c8 r9c7}{n3 n9} ==> r7c9 <> 9, r7c9 <> 3
naked-pairs-in-a-column c7{r6 r9}{n3 n9} ==> r2c7 <> 3
nrc-chain[2] c7n9{r6 r9} - b7n9{r9c1 r7c3} ==> r6c3 <> 9
nrct-chain[2] r2n3{c3 c9} - b6n3{r6c9 r6c7} ==> r6c3 <> 3
nrc-chain[3] r9n5{c6 c4} - b8n6{r9c4 r8c5} - b2n6{r2c5 r1c6} ==> r1c6 <> 5
nrc-chain[3] r4c1{n8 n4} - r9c1{n4 n9} - c3n9{r7 r5} ==> r5c3 <> 8
xyzt-chain[4] r5c3{n9 n3} - r5c1{n3 n8} - r4c1{n8 n4} - r9c1{n4 n9} ==> r6c1 <> 9
interaction row r6 with block b6 for number 9 ==> r5c9 <> 9
nrc-chain[3] c9n9{r3 r6} - r6c7{n9 n3} - r5c9{n3 n8} ==> r3c9 <> 8
interaction block b3 with row r2 for number 8 ==> r2c3 <> 8
singles ==> r2c3 = 3, r5c3 = 9, r9c1 = 9, r9c7 = 3, r7c8 = 9, r6c7 = 9, r3c9 = 9, r1c5 = 9, r9c5 = 4
nrc-chain[2] b8n8{r7c5 r9c6} - r1n8{c6 c3} ==> r7c3 <> 8
interaction block b7 with column c2 for number 8 ==> r3c2 <> 8
naked-single ==> r3c2 = 4
xy-chain[3] r3c1{n5 n8} - r3c5{n8 n3} - r1c4{n3 n5} ==> r3c6 <> 5
singles ==> r1c4 = 5, r9c4 = 6, r8c5 = 1, r7c4 = 3, r7c5 = 8, r9c6 = 5, r3c5 = 3, r3c8 = 1
GRID EasterMonster+n2r6c2.sdk HAS NO SOLUTION : NO CANDIDATE FOR RN-CELL r2n1
LEVEL = NRCZT13, MOST COMPLEX RULE = NRCZT13

;;; Notice that 31 values must be asserted (in addition to the 19 entries and to r6c2=2) before a contradiction is found.
;;; Notice that for this we need an nrczt-whip[13].

2.4) Fourthly, EMS+r6c2=7 is IMPOSSIBLE (Notice "EMS" and not "EM")

(solve-sdk-grid (str-cat ?*PuzzlesDir* "Monsters/EasterMonster/EasterMonster+n7r6c2.sdk"))
***** SudoRules version 13.7wter *****
1.......2.9.4...5...6...7...5.9.3.......7.....7.85..4.7.....6...3...9.8...2.....1
(a specific rule eliminates Steve's candidates)
hidden-single-in-column c3 ==> r2c3 = 7
naked-triplets-in-a-row r5{c2 c4 c8}{n6 n2 n1} ==> r5c9 <> 6, r5c7 <> 2, r5c7 <> 1, r5c6 <> 6, r5c6 <> 2, r5c6 <> 1
naked-single ==> r5c6 = 4
naked-triplets-in-a-column c5{r2 r4 r8}{n1 n2 n6} ==> r9c5 <> 6, r7c5 <> 2, r7c5 <> 1, r3c5 <> 2, r3c5 <> 1, r1c5 <> 6
naked-triplets-in-a-row r5{c2 c4 c8}{n6 n2 n1} ==> r5c3 <> 1, r5c1 <> 6, r5c1 <> 2
nrczt-whip[3] r2n8{c9 c1} - r1c2{n8 n4} - r3n4{c2 .} ==> r3c9 <> 8
nrczt-whip[4] c2n6{r9 r5} - b5n6{r5c4 r4c5} - r6n6{c6 c9} - r2n6{c9 .} ==> r9c6 <> 6
nrczt-whip[4] r8n1{c5 c3} - r6n1{c3 c7} - r4n1{c8 c5} - r2n1{c5 .} ==> r7c6 <> 1
nrczt-whip[5] c8n7{r4 r9} - c6n7{r9 r1} - r1n6{c6 c4} - r9n6{c4 c2} - r5n6{c2 .} ==> r4c8 <> 6
nrczt-whip[6] b9n2{r8c7 r7c8} - r5n2{c8 c2} - c2n6{r5 r9} - b8n6{r9c4 r8c5} - r8n1{c5 c3} - c2n1{r7 .} ==> r8c4 <> 2
nrczt-whip[4] c2n2{r3 r5} - c4n2{r5 r7} - r8n2{c5 c7} - r6n2{c7 .} ==> r3c6 <> 2
nrczt-whip[9] r2n6{c6 c9} - c8n6{r1 r5} - c2n6{r5 r9} - b8n6{r9c4 r8c5} - r8n2{c5 c7} - c8n2{r7 r4} - r4c5{n2 n1} - r4c7{n1 n8} - c9n8{r5 .} ==> r1c4 <> 6
nrczt-whip[11] r8n2{c5 c7} - c8n2{r7 r5} - c2n2{r5 r3} - c4n2{r3 r7} - r7n1{c4 c2} - r5c2{n1 n6} - b7n6{r9c2 r8c1} - r8c5{n6 n1} - r8c4{n1 n7} - c9n7{r8 r4} - r4n6{c9 .} ==> r4c5 <> 2
nrczt-whip[6] c4n6{r8 r5} - b5n2{r5c4 r6c6} - b8n2{r7c6 r7c4} - r3n2{c4 c2} - r5c2{n2 n1} - r7n1{c2 .} ==> r8c5 <> 6
interaction block b8 with column c4 for number 6 ==> r5c4 <> 6
nrc-chain[3] b5n6{r4c5 r6c6} - r1n6{c6 c8} - r5n6{c8 c2} ==> r4c1 <> 6
nrct-chain[3] r5c4{n2 n1} - b8n1{r7c4 r8c5} - c5n2{r8 r2} ==> r3c4 <> 2
hidden-single-in-row r3 ==> r3c2 = 2
nrczt-whip[3] c5n4{r7 r9} - c7n4{r9 r1} - c2n4{r1 .} ==> r7c9 <> 4
hxy-rn-chain[4] r9n6{c4 c2} - r5n6{c2 c8} - r1n6{c8 c6} - r1n7{c6 c4} ==> r9c4 <> 7
nrczt-whip[5] r2n2{c6 c5} - b2n6{r2c5 r1c6} - c8n6{r1 r5} - r5n2{c8 c4} - r6c6{n2 .} ==> r2c6 <> 1
nrc-chain[2] r2n1{c7 c5} - c6n1{r3 r6} ==> r6c7 <> 1
nrct-chain[7] c9n4{r3 r8} - r8n7{c9 c4} - c4n6{r8 r9} - c2n6{r9 r5} - c2n1{r5 r7} - r8c3{n1 n5} - c1n5{r9 r3} ==> r3c1 <> 4
hidden-single-in-row r3 ==> r3c9 = 4
nrczt-whip[4] c1n4{r8 r4} - c1n2{r4 r6} - b4n6{r6c1 r5c2} - c2n1{r5 .} ==> r7c2 <> 4
nrct-chain[6] r9n6{c4 c2} - c2n4{r9 r1} - c2n8{r1 r7} - b7n1{r7c2 r8c3} - r8c5{n1 n2} - r7c6{n2 n5} ==> r9c4 <> 5
nrczt-whip[3] r8c9{n5 n7} - r9n7{c8 c6} - b8n5{r9c6 .} ==> r7c9 <> 5
nrczt-whip[6] c8n6{r1 r5} - c2n6{r5 r9} - c4n6{r9 r8} - r8n7{c4 c9} - r9c8{n7 n3} - r9c4{n3 .} ==> r1c8 <> 9
xyz-chain[3] r1c8{n3 n6} - r2c9{n6 n8} - r2c1{n8 n3} ==> r2c7 <> 3
nrct-chain[5] r2c1{n3 n8} - b3n8{r2c9 r1c7} - r2c7{n8 n1} - r4c7{n1 n2} - c1n2{r4 r6} ==> r6c1 <> 3
nrczt-whip[5] r2c1{n3 n8} - r5c1{n8 n9} - b7n9{r9c1 r7c3} - r7c9{n9 n3} - r2n3{c9 .} ==> r3c1 <> 3
nrczt-whip[6] r7c9{n3 n9} - c8n9{r7 r3} - r9c8{n9 n7} - c6n7{r9 r1} - r1n6{c6 c8} - c8n3{r1 .} ==> r9c7 <> 3
nrczt-whip[5] r3n3{c4 c8} - r1c8{n3 n6} - r5n6{c8 c2} - r9n6{c2 c4} - r9n3{c4 .} ==> r1c5 <> 3
nrct-chain[5] r9c4{n6 n3} - c5n3{r9 r3} - r3n9{c5 c8} - r9c8{n9 n7} - b8n7{r9c6 r8c4} ==> r8c4 <> 6
singles ==> r9c4 = 6, r8c1 = 6, r5c2 = 6, r1c8 = 6, r7c2 = 1
naked-pairs-in-a-row r2{c1 c9}{n3 n8} ==> r2c7 <> 8
naked-single ==> r2c7 = 1
nrct-chain[3] r7c9{n9 n3} - c8n3{r9 r3} - b3n9{r3c8 r1c7} ==> r9c7 <> 9
hxyt-cn-chain[4] c1n2{r6 r4} - c1n4{r4 r9} - c7n4{r9 r8} - c7n2{r8 r6} ==> r6c6 <> 2
singles ==> r5c4 = 2, r5c8 = 1
nrc-chain[3] r7c4{n5 n3} - r9n3{c5 c8} - r9n7{c8 c6} ==> r9c6 <> 5
interaction block b8 with row r7 for number 5 ==> r7c3 <> 5
nrc-chain[3] r8c9{n7 n5} - b7n5{r8c3 r9c1} - r9n9{c1 c8} ==> r9c8 <> 7
singles ==> r8c9 = 7, r8c4 = 1, r8c5 = 2, r2c5 = 6, r4c5 = 1, r6c6 = 6, r2c6 = 2, r4c9 = 6, r3c6 = 1, r6c3 = 1, r7c8 = 2, r4c8 = 7, r9c6 = 7, r1c4 = 7, r5c9 = 5, r2c9 = 8, r2c1 = 3, r5c3 = 3, r7c3 = 9, r7c9 = 3, r9c8 = 9, r3c8 = 3
GRID EasterMonster+n7r6c2.sdk HAS NO SOLUTION : NO CANDIDATE FOR RN-CELL r1n3
LEVEL = NRCZT11, MOST COMPLEX RULE = NRCZT11

This ends the announced proof that n6r6c2 is a strong NRCZT-backdoor for EMS.