The Hidden Logic of SudokuDenis BerthierOnline SupplementsOn the notion of a strong Tbackdoor

© 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 republished or reposted 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:
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 Tbackdoor. 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 TBACKDOORRemember 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 Tbackdoor 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 Tbackdoor size of a puzzle P is the minimum k such that P has a Tbackdoor 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 Singlesbackdoor size 3. It was indeed the first example of a puzzle with Singlesbackdoor size 3. Before, it was conjectured that the maximum Singlesbackdoor size was 2. We now know a little dozen of puzzles with Singlesbackdoor 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 SuperHidden} (+ {XYWing, XYZWing} ) (If XYWing and XYZWing 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 NRCZTbackdoors 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 NRCZTbackdoor size 1. I conjecture that the maximal NRCZTbackdoor size for any puzzle is 1. In the sequel, I shall concentrate on the following NRCZTbackdoor: {r6c2=6} is an NRCZTbackdoor for EasterMonster. The problem with this notion of a Tbackdoor 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 rccell, 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 rncell, 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 cncell, 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 bncell, 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 TrialandError(T) focused on nrc". Remarks:  this definition respects the supersymmetries 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 Tbackdoor of size k for a puzzle P if: 1) D forms a Tbackdoor 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 TrialandError(T) focused on nrc". It can be shown that {r6c2=6} is NOT a strong NRCZTbackdoor for EasterMonster. This should be compared to the following result: EasterMonster can be solved in NRCZT plus "depth one TrialandError(NRCZT)", where "depth one TrialandError(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 TrialandError(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 Tbackdoor. 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 Tbackdoor 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 Tbackdoors. It shows that n6r6c2 is an NRCZTbackdoor but not a strong NRCZTbackdoor for EasterMonster (EM). Combined with the fact that EM can be solved with depthone T&E(NRCZT), this may leave the impression that the notion of a strong Tbackdoor, 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 TBACKDOORStephen 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 NRCZTbackdoor 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 NRCZTbackdoor 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 NRCZTbackdoor for EM (solvesdkgrid (strcat ?*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 nrcztwhip[2] b5n6{r5c6 r4c5}  r2n6{c5 .} ==> r5c9 <> 6 nrcztwhip[4] r8n1{c5 c3}  r6n1{c3 c7}  r4n1{c8 c5}  r2n1{c5 .} ==> r7c6 <> 1 nrcztwhip[5] r2n1{c5 c7}  r6n1{c7 c3}  r6n7{c3 c9}  r8n7{c9 c4}  r8n1{c4 .} ==> r4c5 <> 1 nrcztwhip[6] c2n2{r5 r3}  b2n2{r3c6 r2c5}  r2n6{c5 c9}  b6n6{r4c9 r4c8}  c8n1{r4 r3}  b2n1{r3c6 .} ==> r5c8 <> 2 nrcztwhip[6] r2n6{c5 c9}  r4n6{c9 c8}  c8n7{r4 r9}  c4n7{r9 r8}  r8n2{c4 c7}  b6n2{r4c7 .} ==> r8c5 <> 6 nrcztwhip[7] r9c2{n4 n8}  r7c2{n8 n1}  r8c3{n1 n5}  r8c7{n5 n2}  c8n2{r7 r4}  c8n7{r4 r9}  r8c9{n7 .} ==> r8c1 <> 4 nrctchain[7] r8c1{n6 n5}  b1n5{r3c1 r1c3}  r1n4{c3 c7}  r8c7{n4 n2}  c8n2{r7 r4}  c8n7{r4 r9}  c4n7{r9 r8} ==> r8c4 <> 6 hiddensingleinrow r8 ==> r8c1 = 6 nrcztwhip[7] r6n7{c3 c9}  r8n7{c9 c4}  r8n1{c4 c5}  r8n2{c5 c7}  c8n2{r7 r4}  r4n1{c8 c7}  r2n1{c7 .} ==> r6c3 <> 1 nrcchain[2] b3n1{r3c8 r2c7}  r6n1{c7 c6} ==> r3c6 <> 1 interaction column c6 with block b5 for number 1 ==> r5c4 <> 1 nrcztwhip[4] r2n2{c1 c5}  r2n1{c5 c7}  r6n1{c7 c6}  b5n2{r6c6 .} ==> r5c1 <> 2 nrcztwhip[5] b2n2{r3c6 r2c5}  r2n1{c5 c7}  r6n1{c7 c6}  r6n2{c6 c7}  r4n2{c8 .} ==> r3c1 <> 2 nrcztwhip[5] c2n2{r5 r3}  b2n2{r3c6 r2c5}  r2n1{c5 c7}  r6n1{c7 c6}  b5n2{r6c6 .} ==> r5c7 <> 2 nrctchain[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 hxyztrnchain[5] r4n6{c8 c9}  r2n6{c9 c5}  r2n1{c5 c7}  r4n1{c7 c3}  r4n7{c3 c8} ==> r4c8 <> 2 hiddensingleincolumn c8 ==> r7c8 = 2 nrcztwhip[2] c2n2{r5 r3}  c6n2{r3 .} ==> r5c4 <> 2 nakedsingle ==> r5c4 = 6 hxytcnchain[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 xwinginrows n3{r3 r9}{c5 c8} ==> r1c5 <> 3 nrcchain[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 (solvesdkgrid (strcat ?*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 nrcztwhip[2] b5n1{r5c6 r4c5}  r2n1{c5 .} ==> r5c7 <> 1 nrcztwhip[4] c2n6{r9 r5}  c4n6{r5 r1}  r2n6{c5 c9}  r6n6{c9 .} ==> r9c6 <> 6 nrcztwhip[6] c2n2{r5 r3}  b2n2{r3c6 r2c5}  r2n6{c5 c9}  b6n6{r6c9 r4c8}  c8n1{r4 r3}  b2n1{r3c6 .} ==> r5c8 <> 2 nrcztwhip[6] r2n1{c5 c7}  r4n1{c7 c8}  c8n7{r4 r9}  c4n7{r9 r8}  r8n2{c4 c7}  b6n2{r4c7 .} ==> r8c5 <> 1 nrcztwhip[7] c3n1{r8 r7}  b7n9{r7c3 r9c1}  b7n5{r9c1 r8c1}  r8c7{n5 n2}  c8n2{r7 r4}  c8n7{r4 r9}  r8c9{n7 .} ==> r8c3 <> 4 nrcztwhip[7] c8n2{r7 r4}  r6n2{c7 c1}  r2n2{c1 c5}  r2n6{c5 c9}  b6n6{r6c9 r5c8}  c8n1{r5 r3}  b2n1{r3c6 .} ==> r7c6 <> 2 nrcztwhip[2] c2n2{r5 r3}  c6n2{r3 .} ==> r5c4 <> 2 nrctchain[5] r5c4{n1 n6}  c6n6{r5 r1}  c8n6{r1 r4}  c8n7{r4 r9}  c4n7{r9 r8} ==> r8c4 <> 1 hiddensingleinrow r8 ==> r8c3 = 1 nrcztwhip[6] c2n6{r9 r5}  c2n2{r5 r3}  b2n2{r3c6 r2c5}  r8c5{n2 n4}  r4c5{n4 n1}  r5c4{n1 .} ==> r9c5 <> 6 nrcztwhip[5] c4n7{r8 r9}  c8n7{r9 r4}  c8n2{r4 r7}  r8n2{c7 c5}  b8n6{r8c5 .} ==> r8c4 <> 5 nrcztwhip[7] r1n4{c7 c3}  b1n5{r1c3 r3c1}  r8c1{n5 n6}  r8c5{n6 n2}  c4n2{r7 r3}  c2n2{r3 r5}  c2n6{r5 .} ==> r8c7 <> 4 nrcztwhip[7] r5c4{n1 n6}  c6n6{r6 r1}  c8n6{r1 r4}  c8n7{r4 r9}  c4n7{r9 r8}  c4n2{r8 r7}  c8n2{r7 .} ==> r3c4 <> 1 nrcztwhip[7] c6n6{r5 r1}  c8n6{r1 r4}  c8n7{r4 r9}  c4n7{r9 r8}  b8n6{r8c4 r8c5}  r8n2{c5 c7}  c8n2{r7 .} ==> r5c4 <> 6 nakedsingle ==> r5c4 = 1 nrcchain[6] r2n6{c9 c5}  r2n1{c5 c7}  r4n1{c7 c8}  c8n2{r4 r7}  r8c7{n2 n5}  b6n5{r5c7 r5c9} ==> r5c9 <> 6 nrcztwhip[6] c2n2{r5 r3}  b2n2{r3c6 r2c5}  r2n1{c5 c7}  c8n1{r3 r4}  c8n6{r4 r1}  r2n6{c9 .} ==> r5c2 <> 6 hiddensingleincolumn c2 ==> r9c2 = 6 nrcchain[5] r8n6{c5 c4}  r8n7{c4 c9}  c8n7{r9 r4}  r4n1{c8 c7}  r2n1{c7 c5} ==> r2c5 <> 6 hiddensingleinrow r2 ==> r2c9 = 6 nrctchain[5] b6n1{r4c7 r4c8}  c8n7{r4 r9}  r8n7{c9 c4}  r8n6{c4 c5}  r8n2{c5 c7} ==> r4c7 <> 2 nrcztwhip[3] b9n2{r8c7 r7c8}  r4n2{c8 c1}  r2n2{c1 .} ==> r8c5 <> 2 hxytrnchain[4] r2n2{c1 c5}  r2n1{c5 c7}  r4n1{c7 c8}  r4n2{c8 c1} ==> r6c1 <> 2, r5c1 <> 2, r3c1 <> 2 nrcchain[4] c8n7{r4 r9}  r8n7{c9 c4}  r8n2{c4 c7}  c8n2{r7 r4} ==> r4c8 <> 6 hiddensingleinblock b6 ==> r5c8 = 6 nrcchain[3] b4n2{r5c2 r4c1}  b4n6{r4c1 r6c1}  r6c6{n6 n2} ==> r5c6 <> 2 nakedsingle ==> r5c6 = 4 nrcchain[3] r4n4{c3 c1}  r8c1{n4 n5}  c3n5{r7 r1} ==> r1c3 <> 4 hiddensingleinrow r1 ==> r1c7 = 4 nrcchain[3] r9n4{c1 c5}  r8c5{n4 n6}  r4n6{c5 c1} ==> r4c1 <> 4 singles ==> r4c3 = 4, r6c3 = 7 xychain[4] r5c2{n2 n8}  r7c2{n8 n4}  r8c1{n4 n5}  r8c7{n5 n2} ==> r5c7 <> 2 singles ==> r5c2 = 2, r2c1 = 2 nrcchain[3] c6n2{r3 r6}  r4n2{c5 c8}  c8n1{r4 r3} ==> r3c6 <> 1 hiddensingleincolumn c6 ==> r7c6 = 1 nrcchain[3] r3n1{c8 c5}  c5n9{r3 r1}  r1c8{n9 n3} ==> r3c8 <> 3 hxyrnchain[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 CNCELL 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 nrcztwhips of length 7. 2.3) Thirdly, EM+r6c2=2 is IMPOSSIBLE (solvesdkgrid (strcat ?*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 nrcztwhip[4] c2n6{r9 r5}  c4n6{r5 r1}  r2n6{c5 c9}  r6n6{c9 .} ==> r9c6 <> 6 nrcztwhip[4] r8n1{c5 c3}  r6n1{c3 c7}  r4n1{c8 c5}  r2n1{c5 .} ==> r7c6 <> 1 nrcztwhip[5] r2n1{c5 c7}  r6n1{c7 c3}  r6n7{c3 c9}  r8n7{c9 c4}  r8n1{c4 .} ==> r4c5 <> 1 nrcztwhip[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 nrcztwhip[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 nrcztwhip[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 nrcztwhip[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 nrcztwhip[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 nrcztwhip[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 nrcztwhip[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 nrcztwhip[6] c2n6{r9 r5}  c2n1{r5 r7}  r8c3{n1 n5}  c1n5{r9 r3}  r3n4{c1 c9}  b9n4{r7c9 .} ==> r9c2 <> 4 nrcztwhip[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 nrcztwhip[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: nrcztwhip[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 nrcztwhip[7] c4n7{r8 r9}  b8n6{r9c4 r8c5}  b8n1{r8c5 r7c4}  r5c4{n1 n6}  c6n6{r6 r1}  c8n6{r1 r4}  c8n7{r4 .} ==> r8c4 <> 2 nrcztwhip[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 nrcztwhip[3] r2n1{c7 c5}  r8n1{c5 c3}  r4n1{c3 .} ==> r6c7 <> 1 nrcztwhip[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 hxyztrnchain[4] r8n2{c5 c7}  r4n2{c7 c8}  r4n1{c8 c7}  r2n1{c7 c5} ==> r2c5 <> 2 hiddensingleinrow r2 ==> r2c1 = 2 nrcztwhip[5] r4n1{c8 c7}  b6n2{r4c7 r5c8}  b6n6{r5c8 r4c9}  r2n6{c9 c5}  r2n1{c5 .} ==> r4c8 <> 7 singles ==> r9c8 = 7, r8c4 = 7 hxyrnchain[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 hxyrnchain[4] r4n6{c8 c9}  r2n6{c9 c5}  r2n1{c5 c7}  r4n1{c7 c8} ==> r4c8 <> 2 xwinginrows n2{r4 r8}{c5 c7} ==> r7c5 <> 2, r3c5 <> 2 hxyrnchain[4] r2n6{c5 c9}  r4n6{c9 c8}  r4n1{c8 c7}  r2n1{c7 c5} ==> r2c5 <> 8, r2c5 <> 3 hxyrnchain[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 nakedpairsinacolumn c5{r2 r8}{n1 n6} ==> r3c5 <> 1, r1c5 <> 6 xwinginrows n6{r5 r9}{c2 c4} ==> r1c4 <> 6 nrctchain[2] c2n4{r3 r7}  r8n4{c3 c9} ==> r3c9 <> 4 hiddensingleinblock b3 ==> r1c7 = 4 nrcchain[3] c5n1{r2 r8}  b8n6{r8c5 r9c4}  r5c4{n6 n1} ==> r3c4 <> 1 xwingincolumns n1{c2 c4}{r5 r7} ==> r7c3 <> 1, r5c3 <> 1 hiddenpairsinarow r5{n1 n6}{c2 c4} ==> r5c2 <> 8 nrcchain[3] b8n1{r7c4 r8c5}  b2n1{r2c5 r3c6}  c6n2{r3 r7} ==> r7c4 <> 2 singles ==> r7c6 = 2, r3c4 = 2 nrcztwhip[3] c2n8{r7 r3}  r3n4{c2 c1}  r4c1{n4 .} ==> r9c1 <> 8 xyztchain[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 hiddensingleincolumn c7 ==> r5c7 = 5 interaction block b8 with row r9 for number 5 ==> r9c1 <> 5 nakedpairsinablock b9{r7c8 r9c7}{n3 n9} ==> r7c9 <> 9, r7c9 <> 3 nakedpairsinacolumn c7{r6 r9}{n3 n9} ==> r2c7 <> 3 nrcchain[2] c7n9{r6 r9}  b7n9{r9c1 r7c3} ==> r6c3 <> 9 nrctchain[2] r2n3{c3 c9}  b6n3{r6c9 r6c7} ==> r6c3 <> 3 nrcchain[3] r9n5{c6 c4}  b8n6{r9c4 r8c5}  b2n6{r2c5 r1c6} ==> r1c6 <> 5 nrcchain[3] r4c1{n8 n4}  r9c1{n4 n9}  c3n9{r7 r5} ==> r5c3 <> 8 xyztchain[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 nrcchain[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 nrcchain[2] b8n8{r7c5 r9c6}  r1n8{c6 c3} ==> r7c3 <> 8 interaction block b7 with column c2 for number 8 ==> r3c2 <> 8 nakedsingle ==> r3c2 = 4 xychain[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 RNCELL 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 nrcztwhip[13]. 2.4) Fourthly, EMS+r6c2=7 is IMPOSSIBLE (Notice "EMS" and not "EM") (solvesdkgrid (strcat ?*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) hiddensingleincolumn c3 ==> r2c3 = 7 nakedtripletsinarow r5{c2 c4 c8}{n6 n2 n1} ==> r5c9 <> 6, r5c7 <> 2, r5c7 <> 1, r5c6 <> 6, r5c6 <> 2, r5c6 <> 1 nakedsingle ==> r5c6 = 4 nakedtripletsinacolumn c5{r2 r4 r8}{n1 n2 n6} ==> r9c5 <> 6, r7c5 <> 2, r7c5 <> 1, r3c5 <> 2, r3c5 <> 1, r1c5 <> 6 nakedtripletsinarow r5{c2 c4 c8}{n6 n2 n1} ==> r5c3 <> 1, r5c1 <> 6, r5c1 <> 2 nrcztwhip[3] r2n8{c9 c1}  r1c2{n8 n4}  r3n4{c2 .} ==> r3c9 <> 8 nrcztwhip[4] c2n6{r9 r5}  b5n6{r5c4 r4c5}  r6n6{c6 c9}  r2n6{c9 .} ==> r9c6 <> 6 nrcztwhip[4] r8n1{c5 c3}  r6n1{c3 c7}  r4n1{c8 c5}  r2n1{c5 .} ==> r7c6 <> 1 nrcztwhip[5] c8n7{r4 r9}  c6n7{r9 r1}  r1n6{c6 c4}  r9n6{c4 c2}  r5n6{c2 .} ==> r4c8 <> 6 nrcztwhip[6] b9n2{r8c7 r7c8}  r5n2{c8 c2}  c2n6{r5 r9}  b8n6{r9c4 r8c5}  r8n1{c5 c3}  c2n1{r7 .} ==> r8c4 <> 2 nrcztwhip[4] c2n2{r3 r5}  c4n2{r5 r7}  r8n2{c5 c7}  r6n2{c7 .} ==> r3c6 <> 2 nrcztwhip[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 nrcztwhip[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 nrcztwhip[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 nrcchain[3] b5n6{r4c5 r6c6}  r1n6{c6 c8}  r5n6{c8 c2} ==> r4c1 <> 6 nrctchain[3] r5c4{n2 n1}  b8n1{r7c4 r8c5}  c5n2{r8 r2} ==> r3c4 <> 2 hiddensingleinrow r3 ==> r3c2 = 2 nrcztwhip[3] c5n4{r7 r9}  c7n4{r9 r1}  c2n4{r1 .} ==> r7c9 <> 4 hxyrnchain[4] r9n6{c4 c2}  r5n6{c2 c8}  r1n6{c8 c6}  r1n7{c6 c4} ==> r9c4 <> 7 nrcztwhip[5] r2n2{c6 c5}  b2n6{r2c5 r1c6}  c8n6{r1 r5}  r5n2{c8 c4}  r6c6{n2 .} ==> r2c6 <> 1 nrcchain[2] r2n1{c7 c5}  c6n1{r3 r6} ==> r6c7 <> 1 nrctchain[7] c9n4{r3 r8}  r8n7{c9 c4}  c4n6{r8 r9}  c2n6{r9 r5}  c2n1{r5 r7}  r8c3{n1 n5}  c1n5{r9 r3} ==> r3c1 <> 4 hiddensingleinrow r3 ==> r3c9 = 4 nrcztwhip[4] c1n4{r8 r4}  c1n2{r4 r6}  b4n6{r6c1 r5c2}  c2n1{r5 .} ==> r7c2 <> 4 nrctchain[6] r9n6{c4 c2}  c2n4{r9 r1}  c2n8{r1 r7}  b7n1{r7c2 r8c3}  r8c5{n1 n2}  r7c6{n2 n5} ==> r9c4 <> 5 nrcztwhip[3] r8c9{n5 n7}  r9n7{c8 c6}  b8n5{r9c6 .} ==> r7c9 <> 5 nrcztwhip[6] c8n6{r1 r5}  c2n6{r5 r9}  c4n6{r9 r8}  r8n7{c4 c9}  r9c8{n7 n3}  r9c4{n3 .} ==> r1c8 <> 9 xyzchain[3] r1c8{n3 n6}  r2c9{n6 n8}  r2c1{n8 n3} ==> r2c7 <> 3 nrctchain[5] r2c1{n3 n8}  b3n8{r2c9 r1c7}  r2c7{n8 n1}  r4c7{n1 n2}  c1n2{r4 r6} ==> r6c1 <> 3 nrcztwhip[5] r2c1{n3 n8}  r5c1{n8 n9}  b7n9{r9c1 r7c3}  r7c9{n9 n3}  r2n3{c9 .} ==> r3c1 <> 3 nrcztwhip[6] r7c9{n3 n9}  c8n9{r7 r3}  r9c8{n9 n7}  c6n7{r9 r1}  r1n6{c6 c8}  c8n3{r1 .} ==> r9c7 <> 3 nrcztwhip[5] r3n3{c4 c8}  r1c8{n3 n6}  r5n6{c8 c2}  r9n6{c2 c4}  r9n3{c4 .} ==> r1c5 <> 3 nrctchain[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 nakedpairsinarow r2{c1 c9}{n3 n8} ==> r2c7 <> 8 nakedsingle ==> r2c7 = 1 nrctchain[3] r7c9{n9 n3}  c8n3{r9 r3}  b3n9{r3c8 r1c7} ==> r9c7 <> 9 hxytcnchain[4] c1n2{r6 r4}  c1n4{r4 r9}  c7n4{r9 r8}  c7n2{r8 r6} ==> r6c6 <> 2 singles ==> r5c4 = 2, r5c8 = 1 nrcchain[3] r7c4{n5 n3}  r9n3{c5 c8}  r9n7{c8 c6} ==> r9c6 <> 5 interaction block b8 with row r7 for number 5 ==> r7c3 <> 5 nrcchain[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 RNCELL r1n3 LEVEL = NRCZT11, MOST COMPLEX RULE = NRCZT11 This ends the announced proof that n6r6c2 is a strong NRCZTbackdoor for EMS. 