Sudoku Players' Forum (clone)

denis_berthier wrote:

gsf wrote:

denis_berthier wrote:One says that 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".

I think that (2) might need to be parameterized on k
or there may not be many strong backdoors for k>1

If I understand "parameterized on k" as "depth depending on k", I fear the notion would become trivial. Anyway, the interesting case IMO is when T is a powerful theory and k=1.

for example let T=singles and backdoor size k=3
I think the probability of a strong backdoor is slim

My goal was having a strong definition that'd imply the backdoor is directly useful for focusing the search.

I don't understand that goal
with a backdoor in hand there is no need for a search -- you already have the solution

gsf wrote:

denis_berthier wrote:My goal was having a strong definition that'd imply the backdoor is directly useful for focusing the search.

I don't understand that goal
with a backdoor in hand there is no need for a search -- you already have the solution

As many of us, I think, I'm not interested in the solution, but in its proof. If I'm given a backdoor, I don't have a full proof of the solution. I consider the backdoor as an oracle 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 (e.g. because gsf has told me) 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).

Does your software (maybe with a few additions) allow you to search for strong T'-backdoors of size 1 (i.e. to check whether some of the T'-backdoors are strong T'-backdoors)? (Whatever you want to take as T' - but it has to be a sufficiently powerful theory).

ON THE USEFULNESS OF THE NOTION OF A STRONG T-BACKDOOR

Im my last posts, I may have been over pessimistic about strong backdoors.
I have shown 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 have left you (as it left me) on the impression that the notion of a strong T-backdoor, a priori interesting for guiding the search for a proof of the solution, was useless in practice.
I'll now show that it can indeed be useful.

Let EasterMonster+Steve (or EMS) be EasterMonster (or EM) after Steve's eliminations.

I shall 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 (there are still many different explanations of Steve's eliminations). 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.
(Notice that I haven't programmed any SR rule in SudoRules. To deal with EMS, I've just "manually" eliminated Steve's candidates at the start).

The proof goes as follows (remember that the candidates for cell r6c2 are n1 n2 n6 n7):
- n6c6r2 is an NRCZT-backdoor for EasterMonster (I've already given this proof in a previous post).
- 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 3 posts will give the details of these 3 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.

Firstly, let us show that EM+r6c2=1 is IMPOSSIBLE

(solve-sdk-grid (str-cat ?*GridsDir* "EasterMonster/EasterMonster+n1r6c2.sdk")
hidden singles ==> r1c2 = 7, r2c6 = 7
nrczt2-chain n1{r2c7 r2c5} - n1{r4c5 r4c8} ==> r5c7 <> 1
nrczt4-chain n6{r9c2 r5c2} - n6{r6c1 r6c9} - n6{r2c9 r1c8} - n6{r1c4 r8c4} ==> r9c6 <> 6
nrczt6-lr-lasso n2{r5c2 r3c2} - n2{r2c1 r2c5} - n6{r2c5 r2c9} - n6{r1c8 r4c8} - n1{r4c8 r3c8} - n1{r2c7 r2c5} ==> r5c8 <> 2
nrczt6-lr-lasso n1{r2c5 r2c7} - n1{r4c7 r4c8} - n7{r4c8 r9c8} - n7{r9c4 r8c4} - n2{r8c4 r8c7} - n2{r7c8 r4c8} ==> r8c5 <> 1
nrczt7-chain n1{r8c3 r7c3} - n9{r7c3 r9c1} - n5{r9c1 r8c1} - {n5 n7}r8c9 - n7{r9c8 r4c8} - n2{r4c8 r7c8} - {n2 n4}r8c7 ==> r8c3 <> 4
nrczt7-chain n4{r1c7 r1c3} - n5{r1c3 r3c1} - {n5 n6}r8c1 - n6{r9c2 r5c2} - n2{r5c2 r3c2} - n2{r2c1 r2c5} - {n2 n4}r8c5 ==> r8c7 <> 4
nrc4-chain {n5 n2}r8c7 - n2{r7c8 r4c8} - n7{r4c8 r9c8} - n7{r9c4 r8c4} ==> r8c4 <> 5
nrc5-chain n7{r8c4 r8c9} - n7{r9c8 r4c8} - n2{r4c8 r7c8} - {n2 n5}r8c7 - {n5 n1}r8c3 ==> r8c4 <> 1
hidden-single-in-a-row ==> r8c3 = 1
nrczt7-lr-lasso n2{r7c8 r4c8} - n2{r6c7 r6c1} - n2{r2c1 r2c5} - n6{r2c5 r2c9} - n6{r1c8 r5c8} - n1{r5c8 r3c8} - n1{r2c7 r2c5} ==> r7c6 <> 2
nrczt2-chain n2{r5c2 r3c2} - n2{r3c6 r6c6} ==> r5c4 <> 2
nrczt6-lr-lasso n6{r9c2 r5c2} - n2{r5c2 r3c2} - n2{r2c1 r2c5} - {n2 n4}r8c5 - {n4 n1}r4c5 - {n1 n6}r5c4 ==> r9c5 <> 6
nrczt7-lr-lasso {n1 n6}r5c4 - n6{r6c6 r1c6} - n6{r1c8 r4c8} - n7{r4c8 r9c8} - n7{r8c9 r8c4} - n2{r8c4 r7c4} - n2{r7c8 r4c8} ==> r3c4 <> 1
nrct8-chain n6{r9c2 r5c2} - n2{r5c2 r3c2} - n2{r2c1 r2c5} - n6{r2c5 r2c9} - n6{r1c8 r4c8} - n2{r4c8 r7c8} - n2{r8c7 r8c4} - n7{r8c4 r9c4} ==> r9c4 <> 6
row r9 interaction-with-block b7 ==> r8c1 <> 6
nrct5-chain {n4 n5}r8c1 - {n5 n2}r8c7 - n2{r7c8 r4c8} - n7{r4c8 r9c8} - {n7 n4}r8c9 ==> r8c5 <> 4
nrc4-chain n5{r5c9 r5c7} - {n5 n2}r8c7 - {n2 n6}r8c5 - n6{r2c5 r2c9} ==> r5c9 <> 6
nrct5-chain n7{r4c8 r9c8} - n7{r9c4 r8c4} - n6{r8c4 r8c5} - n2{r8c5 r8c7} - n2{r7c8 r4c8} ==> r4c8 <> 6
nrczt2-chain n6{r5c8 r1c8} - n6{r1c6 r6c6} ==> r5c4 <> 6
naked-single ==> r5c4 = 1
nrc4-chain n6{r5c8 r1c8} - n6{r2c9 r2c5} - n2{r2c5 r2c1} - n2{r3c2 r5c2} ==> r5c2 <> 6
hidden-single-in-a-column ==> r9c2 = 6
nrct4-chain n2{r2c1 r2c5} - {n2 n6}r8c5 - n6{r2c5 r2c9} - n6{r4c9 r4c1} ==> r4c1 <> 2
nrczt3-chain n2{r5c2 r3c2} - n2{r2c1 r6c1} - n2{r6c6 r5c6} ==> r5c7 <> 2
hxyt-rn5-chain {c1 c9}r8n4 - {c9 c4}r8n7 - {c4 c5}r8n6 - {c5 c9}r2n6 - {c9 c1}r4n6 ==> r4c1 <> 4
nrczt4-chain {n6 n8}r4c1 - {n8 n7}r4c9 - n7{r8c9 r8c4} - n6{r8c4 r8c5} ==> r4c5 <> 6
block b5 interaction-with-column c6 ==> r1c6 <> 6
nrc4-chain {n8 n5}r1c6 - n5{r1c3 r7c3} - {n5 n4}r8c1 - {n4 n8}r7c2 ==> r7c6 <> 8
nrc5-chain n6{r8c5 r8c4} - n7{r8c4 r9c4} - n7{r9c8 r4c8} - n1{r4c8 r4c7} - n1{r2c7 r2c5} ==> r2c5 <> 6
hidden singles ==> r2c9 = 6, ==> r5c8 = 6, r6c6 = 6, r4c1 = 6
x-wing-in-columns n2{r3 r5}{c2 c6} ==> r5c1 <> 2, r3c5 <> 2, r3c4 <> 2
column c4 interaction-with-block b8 ==> r8c5 <> 2
naked and hidden singles ==> r8c5 = 6, r1c4 = 6
column c4 interaction-with-block b8 ==> r7c5 <> 2
x-wing-in-columns n2{r3 r5}{c2 c6} ==> r3c1 <> 2
nrc3-chain n2{r4c5 r2c5} - n1{r2c5 r2c7} - n1{r4c7 r4c8} ==> r4c8 <> 2
naked and hidden singles ==> r7c8 = 2, r8c7 = 5, r8c1 = 4, r7c2 = 8, r8c9 = 7, r4c9 = 8, r8c4 = 2, r4c8 = 7, r4c3 = 4, r5c2 = 2, r3c2 = 4, r5c6 = 4, r4c5 = 2, r4c7 = 1, r3c8 = 1, r2c5 = 1, r7c6 = 1, r3c6 = 2, r2c1 = 2, r6c7 = 2, r1c7 = 4, r7c9 = 4, r7c5 = 3, r7c4 = 5, r9c6 = 8, r1c6 = 5, r9c5 = 4, r3c4 = 3, r3c9 = 9, r1c8 = 3, r2c7 = 8, r2c3 = 3, r9c8 = 9, r9c1 = 5, r3c1 = 8
GRID EasterMonster+n1r6c2 HAS NO SOLUTION : NO CANDIDATE FOR r1c3
;;; Notice that 46 values must be asserted (in addition to the 19 entries and to r6c2=1) before a contradiction is found.
;;; Notice that the hardest step uses only an nrczt7-lr-lasso.
;;; (Notice that Steve's eliminations would cover none of the hardest four eliminations here: at level N7.)

Secondly, let us show that EM+r6c2=2 is IMPOSSIBLE

(solve-sdk-grid (str-cat ?*GridsDir* "EasterMonster/EasterMonster+n2r6c2.sdk")
hidden singles ==> r1c2 = 7, r2c6 = 7
nrczt4-chain n6{r9c2 r5c2} - n6{r6c1 r6c9} - n6{r2c9 r1c8} - n6{r1c4 r8c4} ==> r9c6 <> 6
nrczt4-chain n1{r7c2 r5c2} - n1{r6c3 r6c7} - n1{r2c7 r2c5} - n1{r3c4 r8c4} ==> r7c6 <> 1
nrczt7-chain n1{r2c5 r2c7} - n1{r3c8 r5c8} - n1{r5c2 r7c2} - n1{r8c3 r6c3} - n7{r6c3 r6c9} - n7{r8c9 r8c4} - n1{r8c4 r8c5} ==> r4c5 <> 1
nrczt10-chain n6{r2c9 r1c8} - n6{r1c6 r6c6} - n6{r4c5 r4c1} - n6{r5c2 r9c2} - n6{r9c4 r8c4} - n7{r8c4 r8c9} - n7{r6c9 r6c3} - n1{r6c3 r6c7} - n1{r2c7 r2c5} - n6{r2c5 r2c9} ==> r5c9 <> 6
nrczt10-lr-lasso n6{r2c5 r2c9} - n6{r1c8 r5c8} - n6{r5c2 r9c2} - n6{r8c1 r8c4} - n7{r8c4 r9c4} - n7{r9c8 r4c8} - n2{r4c8 r4c7} - n1{r4c7 r4c3} - n1{r8c3 r8c5} - n2{r8c5 r8c4} ==> r4c5 <> 6
nrczt11-chain n2{r8c7 r7c8} - n2{r4c8 r4c5} - n4{r4c5 r5c6} - n2{r5c6 r3c6} - n1{r3c6 r6c6} - {n1 n6}r5c4 - n6{r6c6 r1c6} - n6{r1c8 r4c8} - n7{r4c8 r9c8} - n7{r8c9 r8c4} - n2{r8c4 r8c7} ==> r5c7 <> 2
nrczt11-chain n6{r9c2 r5c2} - n1{r5c2 r7c2} - {n1 n5}r8c3 - n5{r1c3 r3c1} - n4{r3c1 r3c9} - {n4 n7}r8c9 - n7{r9c8 r9c4} - n7{r9c8 r4c8} - n6{r4c8 r1c8} - n6{r1c4 r8c4} - {n6 n4}r8c1 ==> r9c2 <> 4
nrczt5-lr-lasso n4{r1c7 r1c3} - {n4 n8}r3c2 - {n8 n6}r9c2 - {n6 n5}r8c1 - n5{r3c1 r1c3} ==> r8c7 <> 4
nrczt10-lr-lasso n4{r1c7 r1c3} - {n4 n8}r3c2 - {n8 n3}r2c3 - {n3 n1}r2c7 - {n1 n2}r4c7 - {n2 n5}r8c7 - {n5 n1}r8c3 - {n1 n4}r7c2 - {n4 n6}r8c1 - {n6 n8}r9c2 ==> r1c7 <> 8
nrczt8-lr-lasso n6{r2c9 r2c5} - n6{r1c6 r5c6} - n6{r5c2 r9c2} - n6{r8c1 r8c4} - n7{r8c4 r8c9} - {n7 n8}r4c9 - n8{r5c7 r2c7} - n1{r2c7 r2c5} ==> r6c9 <> 6
nrczt12-chain n1{r2c7 r3c8} - n1{r4c8 r4c3} - n1{r5c2 r7c2} - n1{r7c4 r8c4} - n7{r8c4 r9c4} - n7{r9c8 r4c8} - n7{r6c9 r6c3} - n1{r6c3 r6c6} - n6{r6c6 r6c1} - n6{r4c1 r4c9} - n6{r2c9 r2c5} - n1{r2c5 r2c7} ==> r5c7 <> 1
;;; This is the second hardest step:
nrczt14-lr-lasso n5{r1c3 r3c1} - n2{r3c1 r2c1} - n3{r2c1 r2c3} - n8{r2c3 r3c2} - {n8 n6}r9c2 - {n6 n4}r8c1 - n4{r4c1 r4c5} - n4{r5c6 r5c2} - {n4 n1}r7c2 - {n1 n5}r8c3 - {n5 n7}r8c9 - n7{r9c8 r4c8} - n2{r4c8 r4c7} - {n2 n5}r8c7 ==> r1c3 <> 4
hidden-single-in-a-row ==> r1c7 = 4
nrczt11-lr-lasso n7{r8c4 r9c4} - n7{r9c8 r4c8} - n7{r6c9 r8c9} - n4{r8c9 r7c9} - n5{r7c9 r5c9} - n5{r5c7 r9c7} - {n5 n2}r8c7 - n2{r7c8 r5c8} - n6{r5c8 r4c9} - n6{r2c9 r2c5} - n6{r8c5 r9c5} ==> r8c4 <> 5
;;; This is the hardest step:
nrczt15-lr-lasso n1{r2c7 r2c5} - n1{r3c6 r5c6} - n1{r5c2 r7c2} - n1{r8c3 r8c4} - n7{r8c4 r9c4} - n7{r9c8 r4c8} - n7{r6c9 r8c9} - n4{r8c9 r7c9} - n4{r7c6 r9c6} - n4{r8c5 r4c5} - n2{r4c5 r4c7} - n2{r8c7 r8c5} - n6{r8c5 r8c1} - n6{r4c1 r4c9} - n6{r2c9 r2c5} ==> r6c7 <> 1
hxyt-rn6-chain {c1 c6}r6n6 - {c6 c3}r6n1 - {c3 c9}r6n7 - {c9 c4}r8n7 - {c4 c5}r8n1 - {c5 c1}r8n6 ==> r9c1 <> 6, r5c1 <> 6, r4c1 <> 6
row r4 interaction-with-block b6 ==> r5c8 <> 6
nrc3-chain {n8 n4}r4c1 - {n4 n2}r4c5 - n2{r2c5 r2c1} ==> r2c1 <> 8
hxyzt-rn5-chain {c8 c9}r4n6 - {c9 c5}r2n6 - {c5 c7}r2n1 - {c7 c3}r4n1* - {c3 c8}r4n7 ==> r4c8 <> 2
nrc2-chain n2{r7c8 r5c8} - n2{r4c7 r4c5} ==> r7c5 <> 2
nrczt5-lr-lasso n7{r8c4 r9c4} - n7{r9c8 r4c8} - n6{r4c8 r1c8} - n6{r2c9 r2c5} - n6{r8c5 r9c5} ==> r8c4 <> 1, r8c4 <> 2
x-wing-in-rows n2{r4 r8}{c5 c7} ==> r3c5 <> 2, r2c5 <> 2
hidden-single-in-a-row ==> r2c1 = 2
nrc4-chain n1{r6c6 r6c3} - n1{r8c3 r8c5} - n2{r8c5 r4c5} - n4{r4c5 r5c6} ==> r5c6 <> 1
nrc4-chain n1{r5c2 r7c2} - n1{r8c3 r8c5} - n2{r8c5 r4c5} - n2{r4c7 r5c8} ==> r5c8 <> 1
block b6 interaction-with-row r4 ==> r4c3 <> 1
hxy-rn4-chain {c8 c9}r4n6 - {c9 c5}r2n6 - {c5 c7}r2n1 - {c7 c8}r4n1 ==> r4c8 <> 7
hidden singles ==> r9c8 = 7, r8c4 = 7
hxy-rn4-chain {c5 c3}r8n1 - {c3 c6}r6n1 - {c6 c1}r6n6 - {c1 c5}r8n6 ==> r8c5 <> 4, r8c5 <> 2
hidden singles ==> r4c5 = 2, r5c8 = 2, r8c7 = 2, r5c6 = 4
hxy-cn4-chain {r1 r4}c8n6 - {r4 r3}c8n1 - {r3 r6}c6n1 - {r6 r1}c6n6 ==> r1c5 <> 6, r1c4 <> 6
x-wing-in-columns n6{r5 r9}{c2 c4} ==> r9c5 <> 6
nrc3-chain n1{r8c3 r8c5} - n6{r8c5 r9c4} - {n6 n1}r5c4 ==> r5c3 <> 1
hidden-pairs-in-a-row {n1 n6}r5{c2 c4} ==> r5c2 <> 8
nrczt3-chain {n8 n4}r4c1 - n4{r3c1 r3c2} - n8{r3c2 r7c2} ==> r9c1 <> 8
hxy-cn4-chain {r3 r4}c8n1 - {r4 r1}c8n6 - {r1 r6}c6n6 - {r6 r3}c6n1 ==> r3c5 <> 1, r3c4 <> 1
x-wing-in-columns n1{r5 r7}{c2 c4} ==> r7c5 <> 1
hidden-pairs-in-a-column {n1 n6}{r2 r8}c5 ==> r2c5 <> 8, r2c5 <> 3
x-wing-in-columns n1{r5 r7}{c2 c4} ==> r7c3 <> 1
nrc3-chain n2{r3c4 r7c4} - n1{r7c4 r8c5} - n1{r2c5 r3c6} ==> r3c6 <> 2
hidden singles ==> r3c4 = 2, r7c6 = 2
xyzt4-chain {n5 n8}r9c6 - {n8 n6}r9c2 - {n6 n3}r9c4 - {n3 n5}r1c4 ==> r7c4 <> 5
block b8 interaction-with-row r9 ==> r9c7 <> 5
hidden-single-in-a-column ==> r5c7 = 5
block b8 interaction-with-row r9 ==> r9c1 <> 5
naked-pairs-in-a-block {n3 n9}{r7c8 r9c7} ==> r7c9 <> 9, r7c9 <> 3
naked-pairs-in-a-column {n3 n9}{r6 r9}c7 ==> r2c7 <> 3
nrc2-chain n9{r7c3 r9c1} - n9{r9c7 r6c7} ==> r6c3 <> 9
nrczt2-chain n3{r2c3 r2c9} - n3{r5c9 r5c1} ==> r6c3 <> 3
nrc3-chain {n8 n4}r4c1 - {n4 n9}r9c1 - n9{r7c3 r5c3} ==> r5c3 <> 8
nrc3-chain n5{r9c6 r9c4} - n6{r9c4 r8c5} - n6{r2c5 r1c6} ==> r1c6 <> 5
xyzt4-chain {n9 n3}r5c3 - {n3 n8}r5c1 - {n8 n4}r4c1 - {n4 n9}r9c1 ==> r6c1 <> 9
row r6 interaction-with-block b6 ==> r5c9 <> 9
nrc3-chain n3{r2c3 r2c9} - {n3 n8}r5c9 - n8{r4c7 r2c7} ==> r2c3 <> 8
Naked and Hidden Singles ==> r2c3 = 3, r5c3 = 9, r9c1 = 9, r9c7 = 3, r7c8 = 9, r6c7 = 9, r3c9 = 9, r1c5 = 9, r9c5 = 4
nrc2-chain n8{r9c2 r9c6} - n8{r1c6 r1c3} ==> r7c3 <> 8
block b7 interaction-with-column c2 ==> r3c2 <> 8
naked and hidden singles ==> r3c2 = 4, r1c7 = 4, r2c1 = 2
xy3-chain {n8 n5}r1c3 - {n5 n3}r1c4 - {n3 n8}r3c5 ==> r3c1 <> 8
naked singles ==> r3c1 = 5, r1c3 = 8
nrc3-chain n5{r9c4 r1c4} - {n5 n6}r1c6 - n6{r6c6 r5c4} ==> r9c4 <> 6
naked singles ==> r9c4 = 5, r1c4 = 3, r3c5 = 8, r7c5 = 3, r3c6 = 1, r2c5 = 6, r1c6 = 5, r8c5 = 1
GRID EasterMonster+n2r6c2 HAS NO SOLUTION : NO CANDIDATE FOR r7c4

;;; Notice that 35 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 nrczt15-lr-lasso.
;;; Notice that Steve's eliminations would cover none of the hardest three eliminations here: r6c7<>1 (level N15), r1c3 <> 4 (level N14), r5c7 <> 1 (level N12),

Thirdly, let us show that EMS+r6c2=7 is IMPOSSIBLE (Notice EMS and not EM)

(solve-sdk-grid (str-cat ?*GridsDir* "EasterMonster/EasterMonster+Steve+n7r6c2.sdk")
hidden-single-in-a-column ==> r2c3 = 7
naked-triplets-in-a-row {n6 n2 n1}r5{c2 c4 c8} ==> r5c9 <> 6, r5c7 <> 2, r5c7 <> 1, r5c6 <> 6, r5c6 <> 2, r5c6 <> 1
naked-single ==> r5c6 = 4
naked-triplets-in-a-column {n6 n2 n1}{r2 r4 r8}c5 ==> r9c5 <> 6, r7c5 <> 2, r7c5 <> 1, r3c5 <> 2, r3c5 <> 1, r1c5 <> 6
naked-triplets-in-a-row {n6 n2 n1}r5{c2 c4 c8} ==> r5c3 <> 1, r5c1 <> 6, r5c1 <> 2
nrczt3-chain n4{r3c9 r1c7} - {n4 n8}r1c2 - n8{r2c1 r2c7} ==> r3c9 <> 8
nrczt4-chain n6{r9c2 r8c1} - n6{r6c1 r6c9} - n6{r4c8 r4c5} - n6{r2c5 r2c6} ==> r9c6 <> 6
nrczt4-chain n1{r7c2 r8c3} - n1{r6c3 r6c7} - n1{r4c8 r4c5} - n1{r2c5 r2c6} ==> r7c6 <> 1
nrczt5-chain n7{r4c8 r9c8} - n7{r9c6 r1c6} - n6{r1c6 r1c4} - n6{r9c4 r9c2} - n6{r5c2 r5c8} ==> r4c8 <> 6
nrczt6-lr-lasso n2{r8c7 r7c8} - n2{r5c8 r5c2} - n6{r5c2 r9c2} - n6{r8c1 r8c5} - n1{r8c5 r8c3} - n1{r4c3 r6c3} ==> r8c4 <> 2
nrczt4-chain n2{r3c2 r5c2} - n2{r6c1 r6c7} - n2{r8c7 r8c5} - n2{r7c4 r3c4} ==> r3c6 <> 2
nrczt9-chain n6{r1c8 r5c8} - n6{r5c2 r9c2} - n6{r8c1 r8c5} - n2{r8c5 r8c7} - n2{r7c8 r4c8} - {n2 n1}r4c5 - {n1 n8}r4c7 - n8{r5c9 r2c9} - n6{r2c9 r1c8} ==> r1c4 <> 6
nrczt11-chain n2{r8c5 r8c7} - n2{r7c8 r5c8} - n2{r5c2 r3c2} - n2{r3c4 r7c4} - n1{r7c4 r7c2} - n1{r5c2 r5c4} - n6{r5c4 r5c2} - n6{r9c2 r8c1} - {n6 n7}r8c4 - n7{r8c9 r4c9} - n6{r4c9 r4c5} ==> r4c5 <> 2
nrczt7-chain n2{r2c5 r8c5} - n2{r7c6 r7c8} - n2{r5c8 r5c2} - n1{r5c2 r7c2} - n1{r8c3 r8c4} - n6{r8c4 r9c4} - {n6 n2}r5c4 ==> r3c4 <> 2
hidden-single-in-a-row ==> r3c2 = 2
nrc3-chain {n6 n1}r5c2 - n1{r7c2 r7c4} - n2{r7c4 r5c4} ==> r5c4 <> 6
column c4 interaction-with-block b8 ==> r8c5 <> 6
nrc3-chain n6{r4c5 r2c5} - n6{r1c6 r1c8} - n6{r5c8 r5c2} ==> r4c1 <> 6
nrczt3-chain n4{r7c5 r9c5} - n4{r9c2 r1c2} - n4{r3c1 r3c9} ==> r7c9 <> 4
hxy-rn4-chain {c4 c6}r1n7 - {c6 c8}r1n6 - {c8 c2}r5n6 - {c2 c4}r9n6 ==> r9c4 <> 7
nrczt5-chain n2{r2c6 r2c5} - n6{r2c5 r1c6} - n6{r1c8 r5c8} - n2{r5c8 r5c4} - {n2 n1}r6c6 ==> r2c6 <> 1
nrc2-chain n1{r6c6 r3c6} - n1{r3c8 r2c7} ==> r6c7 <> 1
nrct7-chain n4{r3c9 r8c9} - n7{r8c9 r8c4} - n6{r8c4 r9c4} - n6{r9c2 r5c2} - n1{r5c2 r7c2} - {n1 n5}r8c3 - n5{r9c1 r3c1} ==> r3c1 <> 4
hidden-single-in-a-row ==> r3c9 = 4
xyzt5-chain {n4 n8}r1c2 - {n8 n3}r2c1 - {n3 n5}r3c1 - {n5 n6}r8c1 - {n6 n4}r9c2 ==> r7c2 <> 4
nrct6-chain n6{r9c4 r9c2} - n4{r9c2 r1c2} - n8{r1c2 r7c2} - n1{r7c2 r8c3} - {n1 n2}r8c5 - {n2 n5}r7c6 ==> r9c4 <> 5
nrczt5-chain {n5 n7}r8c9 - n7{r9c8 r9c6} - n7{r1c6 r1c4} - n5{r1c4 r3c4} - n5{r7c4 r7c6} ==> r7c9 <> 5
nrczt6-chain n6{r1c8 r5c8} - n6{r5c2 r9c2} - {n6 n3}r9c4 - {n3 n7}r9c8 - n7{r9c6 r1c6} - n6{r1c6 r1c8} ==> r1c8 <> 9
xyz3-chain {n3 n8}r2c1 - {n8 n6}r2c9 - {n6 n3}r1c8 ==> r2c7 <> 3
nrczt5-chain n3{r2c1 r2c9} - {n3 n9}r7c9 - n9{r7c3 r9c1} - {n9 n8}r5c1 - {n8 n3}r2c1 ==> r6c1 <> 3, r3c1 <> 3
nrczt6-chain {n3 n9}r7c9 - n9{r9c8 r3c8} - {n9 n8}r1c7 - n8{r2c9 r2c1} - n3{r2c1 r2c9} - n3{r1c8 r7c8} ==> r9c7 <> 3
nrczt5-chain {n3 n6}r1c8 - n6{r5c8 r5c2} - n6{r9c2 r9c4} - n3{r9c4 r9c8} - n3{r3c8 r3c4} ==> r1c5 <> 3
nrct5-chain {n6 n3}r9c4 - n3{r7c5 r3c5} - n9{r3c5 r3c8} - {n9 n7}r9c8 - n7{r9c6 r8c4} ==> r8c4 <> 6
hidden singles ==> r9c4 = 6, r8c1 = 6, r5c2 = 6, r1c8 = 6, r7c2 = 1
naked-pairs-in-a-row {n3 n8}r2{c1 c9} ==> r2c7 <> 8
naked-single ==> r2c7 = 1
nrct3-chain {n9 n3}r7c9 - n3{r9c8 r3c8} - n9{r3c8 r1c7} ==> r9c7 <> 9
hxyt-cn4-chain {r6 r4}c1n2 - {r4 r9}c1n4 - {r9 r8}c7n4 - {r8 r6}c7n2 ==> r6c6 <> 2
naked and hidden singles ==> r5c4 = 2, r5c8 = 1
nrc3-chain {n5 n3}r7c4 - n3{r9c5 r9c8} - n7{r9c8 r9c6} ==> r9c6 <> 5
block b8 interaction-with-row r7 ==> r7c3 <> 5
nrc3-chain n5{r1c3 r8c3} - {n5 n7}r8c9 - n7{r8c4 r1c4} ==> r1c4 <> 5
nrc3-chain {n7 n5}r8c9 - n5{r8c3 r9c1} - n9{r9c1 r9c8} ==> r9c8 <> 7
naked and hidden 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, r1c7 = 9, r5c7 = 8, r4c7 = 2, r6c7 = 3, r5c1 = 9, r6c1 = 2, r1c5 = 8, r3c5 = 9, r7c5 = 4, r9c5 = 3, r1c2 = 4, r9c2 = 8, r1c3 = 5
GRID EasterMonster+Steve+n7r6c2 HAS NO SOLUTION : NO CANDIDATE FOR r1c6

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

Edited last line 12/12/07: added the word "strong"

I realise I hadn't given the proof that n6r6c2 is an NRCZT-backdoor for EM (the proof I had given is another one).
Here it is.

(solve-sdk-grid (str-cat ?*GridsDir* "EasterMonster/EasterMonster+n6r6c2.sdk")
hidden singles ==> r1c2 = 7, r2c6 = 7
nrczt2-chain n6{r2c9 r2c5} - n6{r4c5 r4c8} ==> r5c9 <> 6
nrczt4-chain n1{r7c2 r5c2} - n1{r6c3 r6c7} - n1{r2c7 r2c5} - n1{r3c4 r8c4} ==> r7c6 <> 1
nrczt7-chain n1{r2c5 r2c7} - n1{r3c8 r5c8} - n1{r5c2 r7c2} - n1{r8c3 r8c4} - n7{r8c4 r8c9} - n7{r6c9 r6c3} - n1{r6c3 r6c6} ==> r4c5 <> 1
;;; hardest step:
nrct10-chain n1{r7c2 r5c2} - n2{r5c2 r3c2} - n2{r2c1 r2c5} - n1{r2c5 r2c7} - n1{r3c8 r4c8} - n7{r4c8 r9c8} - n7{r8c9 r8c4} - n2{r8c4 r8c7} - n2{r7c8 r5c8} - n2{r5c4 r7c4} ==> r7c4 <> 1
nrczt8-chain n6{r2c5 r2c9} - n6{r4c9 r4c8} - n7{r4c8 r9c8} - n7{r9c4 r8c4} - n1{r8c4 r7c5} - n1{r2c5 r2c7} - n1{r4c7 r4c3} - n1{r8c3 r8c5} ==> r8c5 <> 6
nrczt8-chain n2{r5c2 r3c2} - n2{r2c1 r2c5} - n1{r2c5 r2c7} - n1{r3c8 r4c8} - n6{r4c8 r1c8} - n6{r2c9 r2c5} - n6{r9c5 r4c5} - n6{r4c9 r5c8} ==> r5c8 <> 2
nrczt7-chain {n4 n8}r9c2 - {n8 n1}r7c2 - {n1 n5}r8c3 - {n5 n7}r8c9 - n7{r9c8 r4c8} - n2{r4c8 r7c8} - {n2 n4}r8c7 ==> r8c1 <> 4
nrct7-chain {n6 n5}r8c1 - n5{r3c1 r1c3} - n4{r1c3 r1c7} - {n4 n2}r8c7 - n2{r7c8 r4c8} - n7{r4c8 r9c8} - n7{r9c4 r8c4} ==> r8c4 <> 6
hidden-single-in-a-row ==> r8c1 = 6
nrczt8-chain n7{r8c4 r8c9} - n7{r9c8 r4c8} - n2{r4c8 r7c8} - {n2 n4}r8c7 - {n4 n1}r8c3 - n1{r7c2 r5c2} - n1{r5c8 r3c8} - n1{r3c4 r8c4} ==> r8c4 <> 5
nrczt9-chain n7{r6c3 r6c9} - n7{r8c9 r8c4} - n1{r8c4 r8c5} - n1{r2c5 r2c7} - n1{r4c7 r4c8} - n2{r4c8 r7c8} - n2{r8c7 r8c4} - n2{r3c4 r5c4} - {n2 n1}r6c6 ==> r6c3 <> 1
nrc2-chain n1{r3c8 r2c7} - n1{r6c7 r6c6} ==> r3c6 <> 1
column c6 interaction-with-block b5 ==> r5c4 <> 1
nrczt5-chain n2{r2c1 r2c5} - n1{r2c5 r2c7} - n1{r6c7 r6c6} - n2{r6c6 r6c7} - n2{r4c8 r4c1} ==> r5c1 <> 2, r3c1 <> 2
nrczt6-chain n2{r5c2 r3c2} - n2{r2c1 r2c5} - n1{r2c5 r2c7} - n1{r6c7 r6c6} - n2{r6c6 r7c6} - n2{r8c4 r8c7} ==> r5c7 <> 2
nrczt7-chain n2{r7c8 r4c8} - n7{r4c8 r9c8} - n7{r8c9 r8c4} - n1{r8c4 r3c4} - n2{r3c4 r5c4} - n2{r5c2 r3c2} - n2{r2c1 r2c5} ==> r7c5 <> 2
nrczt7-chain n2{r3c2 r5c2} - {n2 n6}r5c4 - {n6 n4}r4c5 - {n4 n1}r5c6 - n1{r6c6 r6c7} - n1{r2c7 r2c5} - {n1 n2}r8c5 ==> r3c5 <> 2
nrct6-chain n2{r7c8 r4c8} - n2{r6c7 r8c7} - n2{r8c5 r2c5} - n6{r2c5 r2c9} - n6{r1c8 r5c8} - {n6 n2}r5c4 ==> r7c4 <> 2
nrczt6-chain {n5 n3}r7c4 - {n3 n6}r1c4 - {n6 n2}r5c4 - n2{r5c2 r3c2} - {n2 n8}r3c6 - {n8 n5}r1c6 ==> r3c4 <> 5
nrczt7-chain n2{r7c8 r8c7} - n2{r8c5 r2c5} - n1{r2c5 r2c7} - n1{r3c8 r5c8} - n6{r5c8 r4c9} - n7{r4c9 r4c3} - n1{r4c3 r4c8} ==> r4c8 <> 2
hidden-single-in-a-column ==> r7c8 = 2
nrczt2-chain n2{r5c2 r3c2} - n2{r3c6 r6c6} ==> r5c4 <> 2
naked-single ==> r5c4 = 6
naked-pairs-in-a-column {n3 n5}{r1 r7}c4 ==> r9c4 <> 5, r9c4 <> 3
naked and hidden 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, r3c1 = 5, r9c7 = 5, r8c7 = 4, r8c3 = 5, r8c5 = 1, r3c4 = 1, 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
nrc2-chain n9{r7c3 r5c3} - n9{r6c1 r6c9} ==> r7c9 <> 9
…(Naked and Hidden Singles)…

174385962
293467158
586192734
451923876
928674315
367851249
719548623
635219487
842736591

Res rule for xyzt type chains modified:
delete requirement for chained cells to contain exactly one unlinked candidate. Add requirement for counting unlinked candidates. Add rule:
when count reaches zero, done. Modify chain link requirement - links must be only to some previous chain piece, with no regard to order required. Apply lnk rule regarding extra single candidate per chained cell to all extra candidates per chained cell.

Apply to hp chain: Start where one wishes, but let us start with 7c2:
A count change of +0 assumed uno.

7c2(2loc)[+1]-2c2(3loc)[+1][(total +2]-(6)c2-(1)c2
-(1r8)[+1,total +3]-(6)r8[-1,total +2]- (6)r8 -(2)r8-(7)r8-(7)c8-(2)c8-(1)c8-(6)c8-(6)r2[+1,total +3]-(1)r2[-1,total +2]-(1)r2
-(2)r2[-1;total 1]-(7)r2[-1;total:0] => r1c3<>7
In a similar fashion, one can use the same sets to eliminate the other candidates indicated by the hp loop.
Note that the structure required consideration of some of the same sis twice.

Advanatage: easily proven from existing tchain structure. Minor modification of existing res rules .
Disadvantages: ignores the circuity, thus requires multiple chains to achieve same result, decreases findability by ignoring groups.

Proof: many forms are possible, perhaps the easiest of which is to count extra truths per structure (that one is rather trivial, and presumed obvious). Another proof is simply: structure reduces to a strong inference set of t chains.

Note: I could be much more specific, but have left this structure a tad vague. The structure that I would prefer versus the unknowable preferences of others motivates this vagueness. Once one has settled upon a specific structure, specific proofs are much easier (of course).

Hypothesis:
If one minimizes the modified chain restrictions to their theoretical minimum, the set of eliminations (ignoring uniqueness) that this type of chain will miss should be null. The proof of this assertion could be complex, or as simple as complete axiomatic coverage.

Steve K wrote:Res rule for xyzt type chains modified:
delete requirement for chained cells to contain exactly one unlinked candidate.

There has never been any such restriction.

Steve K wrote:Add requirement for counting unlinked candidates. Add rule:
when count reaches zero, done. Modify chain link requirement - links must be only to some previous chain piece, with no regard to order required. Apply lnk rule regarding extra single candidate per chained cell to all extra candidates per chained cell.
Apply to hp chain: Start where one wishes, but let us start with 7c2:
A count change of +0 assumed uno.

Thus, you don't get chains but nets and you lose all the benefits of the linear chain structure.

Steve K wrote:Hypothesis:
If one minimizes the modified chain restrictions to their theoretical minimum, the set of eliminations (ignoring uniqueness) that this type of chain will miss should be null. The proof of this assertion could be complex, or as simple as complete axiomatic coverage.

Starting from xyzt chains, this conjecture is highly unlikely.
If you want it to be more likely, you'd have to start with the supersymmetric version, nrczt-chains, and get what I've called nrczt-nets.
Even so, there is no serious indication that you'd get a complete set of rules.

The second (and final) edition of my book "The Hidden Logic of Sudoku" has been published.
It is currently available only on Lulu.com (http://www.lulu.com/content/1352515) but it will also be on Amazon soon.

Main changes:
- the nrc notation is used throughout
- two new chapters on 3D chains (the first edition was published before I imagined the 3D chains)
- a discussion of the main concepts appearing in the book.
Further details on my Web pages: http://www.carva.org/denis.berthier/HLS/index.html

Families of resolution rules

I've already spoken of this, but, given the great variety of rules that have been proposed, it seems to me that I must say a little more.

First, let me state that I'm only speaking here of resolution rules and not of resolution techniques (see the difference in the second post of this thread).
Moreover, I'm considering only rules that can be considered as first order, i.e. whose logical formulation doesn't require quantifiers on subsets.

In my book, in this forum and in SudoRules, I have mainly been considering only four large families of resolution rules:
1) the elementary constraints propagation rules or ECP (direct contradictions along rows, columns and blocks),
2) the subset rules (Naked, Hidden and Super-Hidden (or fish) versions of Singles, Pairs, Triplets, Quads),
3) the elementary interaction rules (between rows and blocks and between columns and blocks),
4) the xy-to-nrczt (xy, hxy, xyt, hxyt, xyz, hxyz, xyzt, hxyzt, nrc, nrct, nrcz, nrczt) family of chain rules.

I've already shown the unity of the subset rules through symmetry and super-symmetry.
I've also shown why all the rules in the xy-to-nrczt family can be considered as generalisations of the basic xy-chain rule. This includes the basic NLs or AICs (basic meaning "with no ALSs". Although nrczt-chains subsume the whole family, the other chains are easier to find and should therefore not be forgotten. This family is organised in a pedagogical hierarchy.

In my book, I've also mentionned that the subset rules are extensions of the xy2 to xy4 patterns.
More precisely, any Naked-Quad which doesn't reduce to a Triplets has to be an extension of the "skeletal Naked-Quads" {1 2} - {2 3} - {3 4} - {4 1}, with all links identical - which is a special case of the xy4 chain.
Said otherwise, the general abstract pattern of a Naked-Quads is:
{1 2 (3) (4)} - {2 3 (4) (1)} - {3 4 (1) (2)} - {4 1 (2) (3)} with all links identical and parens meaning an optional candidate,
from which the general abstract patterns of a Hidden-Quads and a Super-Hidden-Quads (or Jellyfish) are easily obtained using symmetry and super-symmetry.

This shows that families 2 and 4 are very closely related. Moreover, I've shown in the "fully super-symmetric chains" thread that most (but not all) cases of the subset patterns are special cases of nrczt-chains.

What I want to stress now is that, in spite of being so close, families 2 and 4 require very different forms of reasoning:
- the standard proofs of the subset rules require considering the pattern globally; they don't proceed from one cell to the next;
- the proofs of the xy-to-nrczt rules follow the linear chain structure in such a way that each step doesn't anticipate on the future elements of the chain; I consider this non-anticipativeness as a key property of chains; it is what makes them useable in practice.

As they correspond to different forms of reasoning, the subsets and the nrczt-chains could be subsumed under a common pattern only if we accepted chains that anticipe on their future elements OR if we define a new type of pattern (see my next post).

DEFINITION of NRC-, NRCT- and NRCZT- NETS

Let it be clear that I don't like nets and I consider that the nrczt-nets I'm going to define below are not really useable patterns for a human player, at least in their most general form. But are the most general chains of ALSs (and other AAAAAHHHHAAAHHAAAHHHH LSs) really useable?
Anyway, as this may be a matter of taste and I already spoke of them several times, saying that it is easy to define them, the least I can do is give such a definition. Although this is intuitively obvious, we need a few technicalities if we want to formalise it unambiguously.

Remarks:
- as was the case for nrczt-chains, nrczt-nets do not rely on subsets and on links between subsets;
- given a candidate C, nrczt-chains were the most general first order chain patterns that could justify the elimination of C; nrczt-nets are the most general first order net patterns that can justify the elimination of C; ("first order" means not relying on subsets);
- the following definitions can be restricted to nrct or nrc nets; they can also be restricted to any of their 2D counterparts.


If you don't know the basics of graph theory, it may be appropriate to start by reading the following elementary introduction: http://en.wikipedia.org/wiki/Graph_%28mathematics%29


An nrczt-chain was defined as a sequence (i.e. a completely or linearly ordered set) of 2D-cells (each in either of the rc-, rn-, cn- or bn- spaces). It can also be seen as a sequence of (alternatively left and right linking) candidates, but the easiest way to generalise to nets is using the cell view.

Now, as an informal introduction to the following definitions, let me just say that they provide for the possibility for having several right linking candidates in some of the cells and they explain how they can be dealt with. This is very far in spirit from allowing subsets in chains (such as in Grouped NLs).

Definition: an oriented 2D-cell is a 2D-cell whose candidates are labelled according to the rules:
- it has one and only one left-linking candidate (or llc)
- it has one or more right-linking candidates (or rlc)
- it has zero or more additional candidates
(given a 2D-cell in a real puzzle, its candidates can be labelled in different ways as llc, rlc or additional, but a choice has to be made for a net to be completely specified; notice that, at this stage, additional candidates are NOT labelled as t or z)

Definition: a 3D-net is a partially ordered set (called a poset by mathematicians) of oriented 2D cells from any of the 2D-spaces, i.e. either rc-, rn-, cn- or bn- spaces (notice that, as I speak of a set and not a bag, these cells are different); this structure must satisfy the following conditions:
- if an oriented 2D-cell has more than one right-linking candidate, it is called branching,
- if an oriented 2D-cell has more than one immediate predecessor in the poset, it is called merging,
(notice that a cell can be both merging and branching)
- if an oriented 2D-cell has no predecessor in the poset it is called a source,
- if an oriented 2D-cell has no successor in the poset it is called a sink ,
- if an oriented 2D-cell is neither branching nor merging nor a source nor a sink, it is called regular,
- for every oriented 2D-cell C1 (but those in the sinks), each of its right-linking candidates has a unique distinguished nrc-link to the left linking candidate of an immediate successor of C1 in the poset;
(notice that any candidate may have several nrc-links (e.g; along a row and a block) to another given oriented 2D-cell , but one has to be chosen for a net to be completely specified);
(this is the main connectivity condition);
- if different right-linking candidates in possibly different oriented 2D-cells have their distinguished nrc-links pointing to the (unique) left-linking candidate of the same oriented 2D-cell C2, then C2 is a merging cell;
- notice that it is not necessary to add a condition on left-linking candidates being nrc-linked to right-linking ones: this is already part of the definition of 2D-cells;


With a 3D-net, one can associate a directed acyclic graph (DAG):
- edges: the edges of the graph are all the couples (oriented 2D-cell C, left-linking candidate of C) and (oriented 2D-cell C, right-linking candidate of C)
(instead of taking merely all the left- and all the right- linking candidates, these technicalities provide for the possibility for a candidate to appear several times, but only in different paths);
- vertices:
- for every oriented 2D-cell with left-linking candidate C1 and for each of its right-linking candidates C2, the graph has a vertex with head C1 and tail C2;
- for every oriented 2D-cell C, for each of its right-linking candidates C1 and for the distinguished nrc-link of C1 to an oriented 2D-cell C2, the graph has a vertex with head C1 and tail the left-linking candidate of C2;
- the graph has no vertex other than those defined in the above three clauses.
With these definitions, only left-linking candidates are merging points and branching occurs only with the existence of several right-linking candidates.
Notice that the additional candidates are not considred as belonging to this graph.

Definitions: a target of a 3D-net is any candidate that is nrc-linked to the left-linking candidates of all its sources and to all the right-linking candidates of all its sinks.

Remarks:
- as was the case for the other 2D- or 3D- chains I have introduced, the target does not belong to the net;
- a 3D-chain is a 3D-net with a single source, a single sink and no branching or merging; said otherwise, its branching factor is 1;
- 2D chains implied a restriction on their first cell: it had to be bilocal or bivalue (this is not an arbitrary restriction, it is a consequence of the 2D constraints); nrczt-chains somehow relax this restriction, as their first cell may contain additional z-candidates, although they are rarely needed in practice; with nrczt-nets, multiple right-linking candidates (branching) allow to use any cell as a first cell, and having a set of sources allows having several first cells.


Definition: path, maximal path, initial path. Given a 3D-net,
- a path between two left- or right- linking candidates C1 and Cn is any path in the associated graph;
- a maximal path is a path in the associated graph, between the left-linking candidate of a source and the right-linking candidate of a sink
- given a candidate C, an initial path to C is any path with head the left-linking candidate of a source and with tail C.
A path thus defined is a 3D-chain.
Given a path, a right-linking candidate in a cell that has more than one is called a branched candidate.

Given 2 candidates, in a 3D-chain there is a single path between them. But in a 3D-net, there may be 0, 1 or more paths beween them. This is the main structural difference between a chain and a net.
Given a candidate, there may be 1 or several initial paths to it.

As was the case for for 2D- or 3D- chains, only some types of 3D-nets are interesting (those that lead to a contradiction on the target). These conditions are generalisations of the condition on nrc(z)(t) chains: the nrc-bivalue (bivalue/bilocation) condition modulo the previous right-linking candidates and target.We just have to be careful when we formalise them.


Definition: an nrczt-net built on a candidate Z is a 3D-net admitting Z as a target (in the general sense defined above) and which satisfies the nrczt condition:
- for any cell in the net, for any right-linking candidate C in this cell, for ANY initial path to C, this 3D-chain would be an nrczt-chain or an nrczt-lasso if, at any branching point in this chain, we forgot the other right-linking candidates.
Notice that, as there may be several initial paths to C, each additional candidate may have different justifications along each of these paths (it may appear as a t-candidate in some paths and as a z-candidate in others). This is why additional candidates were not a priori labelled as t or z.

Theorem (nrczt-net theorem): given an nrczt-net based on a target Z, Z can be eliminated.


Notice that nrczt-nets are non-anticipative patterns.

Enough for one day.
In a next post, I'll prove that nrczt-nets (together with ECP and Singles) subsume all the rules defined in my book and programmed in SudoRules:
- Subsets (Naked, Hidden and Super-Hidden),
- elementary interactions row/block and column/block
- all the (h)xy(z)(t) and nrc(z)(t) chains

But, remember the first sentence of this post: this is not to mean that nrczt-nets should replace all the other patterns.

Edited 02/04/08: improved the definition of a 3D-net.
Edited 02/05/08: added the possibility of lassos in nrczt-nets.

nrczt-nets subsume basic interactions

As a first example, let me show how the basic interaction patterns can be re-written as nrczt-nets.

ROW INTERACTION WITH BLOCK (RiB):

First, the general pattern for a non-degenerate RiB (seen in standard rc-space) is:

Code: Select all

XXXXXX-----11-----12----(13)
            ?-------?-------?
            ?--------?-----?


the rightmost 9 cells are in the same block,
11, 12, 13 designate occurrences of the target value under consideration,
the 6 X's indicate that the target value is not allowed in the 6 cells of the row outside the block,
parens indicate an optional candidate,
? indicates a possible place for the target,
Rows and columns can be permuted.
Notice that at least two occurrences of the target value must occur in the row under consideration: otherwise, we'd have a Naked Single.


First case:

Code: Select all

XXXXXX-----11-----12----  X
            ?-------?-------?
            ?--------?-----?


subsumed by NRC1: {11 12}


Second case:

Code: Select all

XXXXXX-----11-----12----(13)
            ?-------?-------?
            ?--------?-----?


subsumed by the nrc-net (where "/" separates the candidates according to their label: llr / rlc / additional and branching is indicated by vertical alignment):

Code: Select all

{11 / 12
    / 13}


BLOCK INTERACTION WITH ROW (BiR)

First, the general pattern for a non-degenerate RiB (seen in standard rc-space) is (with the same conventions as above):

Code: Select all

X-------X-------X
X--------X----- X
11-----12----(13)-------------?-------


First case:

Code: Select all

-X-----X-----X-
-X-----X-----X-
-11----12-----X-----------Z


subsumed by NRC1: {11 12}


Second case:

Code: Select all

-X------X------X-
-X------X------X-
-11----12------13---------Z


subsumed by the nrc-net:

Code: Select all

{11 / 12
    / 13}


INTERACTIONS WITH COLUMNS
the result is obtained by rc symmetry.

NRCZT- NETS SUBSUME THE (NAKED, HIDDEN and SUPER-HIDDEN) SUBSET RULES

As Subset rules are obtained from each other by symmetry and super-symmetry, it is enough to prove the result for either the Naked, Hidden or Super-Hidden subsets.

For Pairs, we already know that Naked Pairs are subsumed by xy2-chains.


TRIPLETS
For triplets, let us choose the fishy pattern and prove that Super-Hidden Triplets (Swordfish) are subsumed by hxyzt-nets
We start from the general pattern for Swordfish-in-rows (seen in standard rc-space) :

Code: Select all

11---------12--------(13)

(21)-------22---------23

31-------(32)---------33

----------------------Z


The net we associate with this fish depends on the presence of optional candidate 32.
In each case, the hxyzt-rn-net has only two maximal paths; the branching factor is 2, the breadth is 2.

Code: Select all

{23 / 22} - {12 / 11 / (13*)} - {31 / 33 / (32#22)}
... / 21} - if 32 is present: {11 / 12 / (13*)} - {32 / 33 / (31#21)}
..........- if 32 is absent:  {31 / 33}


QUADS
For triplets, let us choose again the fishy pattern and that Super-Hidden Quads (Jellyfish) are subsumed by hxyzt-nets
We start from the general pattern for Jellyfish-in-rows (seen in standard rc-space) :

Code: Select all

11---------12--------(13)---------(14)

(21)-------22---------23---------(24)

(31)------(32)--------33----------34

41-------(42)--------(43)---------44

-------------------------------------Z


The hxyzt -rn-net we associate with the Jellyfish depends on the presence of several optional candidates.
It is more complex than for Swordfsih, with 6 maximal paths; the branching factor is 3, the breadth 6.

As is often the case, what's most difficult is taking into account the multiple cases associated with the presence or absence of the various optional candidates.
There are other possible nets. Here I've avoided using the optional candidates 14 and 24 as exit points for the chains.

Code: Select all

{34 / 33} - {23 / 22 / (24*)} - {12 / 11 / (14*) (13#33)} - {41 / 44 / (42#22) (43#33)}
................the next branch (in either of its two forms) is present if and only if 21 is present:
................/ 21 / (24*)} - if 42 is present: {11 / 12 / (14*) (13#33)} - {42 / 44 / (41#21) (42#12)}
..............................- if 42 is absent: {41 / 44 / (43#33)}

..../ 32} - {12 / 11 / (14*)} - if 43 is absent: {41 / 44 / (42#32)}
..............................- if 43 is present:
........................................- if 21 is present: {21 / 23 / 22#32 (24*)} - {43 / 44 / 41#11 (42#32)}
........................................- if 21 is absent: {41 / 44 / (42#32)}
.............................................................../ 43 /  (42#32)} - {23 / 22 / (24*)} lr-lasso on 32
.................the next branch (in either of its two forms) is present if and only if 13 is present:
................./ 13 / (14*)} - if 21 is present: {23 / 21 / 22#32 (24*)} - {41 / 44 / (42#22) ((43#13)}
...............................- if 21 is absent: {23 / 22 / (24*)} lr-lasso on 32

..../ 31} - if 43 and 42 are absent: {41 / 44}
..........- if either 42 or 43 is present:
...................- {11 / 12 / (14*)} - if 43 is present: {22 / 23 / (21#31) (24*)} - {43 / 44 / 41#31 (42#12)}
........................................- if 43 is absent but 42 is present: {42 / 44 / 41#31}
.........................the next branch (in either of its two forms) is present if and only if 13 is present:
........................ / 13 / (14*)} - if 42 is present: {23 / 22 / (21#31) (24*)} - {42 / 44 / 41#31 43#13}
.......................................- if 42 is absent (then 43 is present): {43 / 44 / 41#31}


(not easy with this software to put the branches at the right places!)

Notice the two cases of lassos really adding something to chains.

NRCZT- NETS SUBSUME (SASHIMI or not) FINNED FISH

Let me show this only for Jellyfish

We start from the general pattern for (sashimi) finned Jellyfish-in-rows (seen in standard rc-space) :

(this is an abstact pattern: rows and columns can be permuted)

Code: Select all

11---------12--------(13)--------(14)

(21)-------22---------23---------(24)

(31)------(32)--------33----------34

 41-------(42)-------(43)--------[44]--45--(46)

-----------------------------------Z


where [44] may be present or absent (the sashimi)
45 (and 46) is the fin
44, 45, 46 and Z are in the same block.

The net given for ordinary Jellyfish can easily be adapted to this case:
- replace any final link to 44 by a link to 45
- whenever necessary, consider 44 and/or 46 as z candidates.