Sudoku Players' Forum (clone)

NRCZT-CHAIN RULES SUBSUME "ALMOST ALL" NAKED, HIDDEN AND SUPER-HIDDEN SUBSET RULES

In my book and in this forum, I've already formulated several theorems about the subsumption of subset rules by nrczt-chain rules.
In the following three parts, I'll give further results, some logical and some statistical.

In the first part, I'll recall the exact subsumption theorems.
In the second part, I'll try to evaluate the practical scope of what, in the Naked, Hidden and Super-Hidden (fish) Subset rules, is not subsumed by nrczt-chains.
In the third part, I'll give a simple example.


PART 1) EXACT NRCZT SUBSUMPTION THEOREMS FOR SUBSET RULES.

Notations:
P = Pairs
T= Triplets
Q = Quadruplets
N = Naked
H = Hidden
SH = Super-Hidden (Fish)
In patterns, numbers 1, 2, 3,... stand for variables: n1, n2, n3,... if in rc-space; c1, c2, ... if in rn-space,....

The N theorems are proven directly; using symmetry and super-symmetry, the H and SH corollaries are straightforward consequences.


Pairs:
Theorem: XY2 is equivalent to NP.
Corollary: NRC2 (and therefore also NRCZT2) subsumes NP, HP and SHP.



Triplets:
As proven in my book, the general pattern for a non-degenerate NT is: rc/- {1 2 (3)} - {2 3 (1)} - {3 1 (2)} (where the 2 links are the same unit).
Parens indicate optional candidates.

Consider a candidate 1 in a cell belonging to the unit of the triplet but not to the triplet itself (i.e. a candidate that can be eliminated by NT in this unit)
Using the # and * symbols for the t- and z- candidates, the above pattern becomes the nrczt3-chain based on the chosen candidate:
rc/- {1 2 (3)} - {2 3 (1*)} - {3 1 (2#1)},
provided that candidate 3 is absent from the first cell.

Theorem: XYZT3 (and therefore also NRCZT3) eliminates any candidate 1 eliminated by a NT with pattern {1 2} - {2 3 (1)} - {3 1 (2)} (all links along the same unit)

Changing the order of the chain and/or renaming the candidates, if necessary, it appears that the only cases when we can't get an xyzt3-chain based on a candidate 1 eliminated by NT in the same unit correspond to the pattern {1 2 3} - {2 3 (1)} - {3 1 2)}
We thus get a better formulation:
Theorem: XYZT3 (and therefore also NRCZT3) eliminates any candidate eliminated by NT in a cell outside of the triplet provided that another of the 3 candidates in the triplet appears in only 2 cells of the triplet.
Theorem: HXYZT3(row) (and therefore also NRCZT3) eliminates any candidate eliminated by HT(row) in a cell of the hidden triplet provided that another of the 3 cells in the triplet doesn't contain one of the candidates in the triplet.
Theorem: SHXYZT3(row) (and therefore also NRCZT3) eliminates any candidate eliminated by Swordfish(row) in a column of the Swordfish outside of the 3 rows in the Swordfish provided that a cell of the Swordfish in one of the other 2 columns in the Swordfish doesn't contain the candidate of the Swordfish.



Quadruplets:
As proven in my book, the general pattern for a non-degenerate NQ is: rc/- {1 2 (3) (4)} - {2 3 (4) (1)} - {3 4 (1) (2)} - {4 1 (2) (3)} (where the 3 links are the same unit).

Consider a candidate 1 in a cell belonging to the unit of the quadruplet but not to the quadruplet itself (i.e. a candidate that can be eliminated by NQ in this unit)
As before, the above pattern becomes the nrczt4-chain based on the chosen candidate:
rc/- {1 2 (3) (4)} - {2 3 (4) (1*)} - {3 4 (1*) (2#1)} - {4 1 (2#1) (3#2)},
provided that candidates 3 and 4 are absent from the first cell and candidate 4 is absent from the second.

We thus get:
Theorem: XYZT4 (and therefore also NRCZT4) eliminates any candidate 1 eliminated by a NQ with pattern {1 2} - {2 3 (1)} - {3 4 (1) (2)} - {4 1 (2) (3)} (all links along the same unit)


I've also stated theorems for finned fish, sashimi or not - that I won't reacll here in detail. Let's just asy: nrczt-chains subsume "almost all" finned (sashimi or not).




PART 2) EXAMINING HOW NRCZT-CHAIN RULES COMPENSATE FOR THE NON SUBSUMED CASES OF NAKED, HIDDEN AND SUPER-HIDDEN SUBSET RULES.

From the theorems in part 1, one can see that most of the eliminations allowed by naked, hidden and super-hidden subset rules can be done by corresponding nrczt-chains (of the same size).
But "most" still keeps a very vague meaning.
Using the Sudogen0 reference collection of 10,000 random minimal puzzles, I analysed what this means in practice.
For this purpose, I ran SudoRules with all the rules turned off, except ECP, NS, HS and nrczt chains and lassos of any length, on the full Sudogen0 collection. (Remember that basic interaction rules are subsumed by NRCZ1).

Results:
- all the puzzles in Sudogen0 are still solved by this epurated version of SudoRules;
- all these puzzles are solved with chains of the same maximal length as in the full SudoRules, except:
# 220, 1239, 6420, 6580, 8693, 8701, 9514 need chains of length 4 instead of 3
# 1222 needs chains of length 5 instead of 3

Notice the meaning of "compensate" in the title. It doesn't mean that any subset is repalced by a corresponding chain but that there appears to be some opportune, maybe unrelated, chain(s) that do the same elimination work. In the few cases for which the level is changed, we can be sure that there is no related chain and they are cases of exceptional subset patterns.

Although this is not a formal proof, it may help understand why almost any puzzle solved using AICs with ALSs can also be solved using only nrczt-chains: nrczt-chains formally subsume the most common cases of AICs with ALSs (same proof as for pure subset rules) and they compensate for almost all of the other cases in practice.
(We already know that nrczt-chains also subsume hinges).


PART 3) EXAMPLE
Consider puzzle Sudogen0 #220
.4..72.6.
.......9.
.7.49.5..
796..1.5.
.1....8..
..3...6..
9........
6..134...
...9....8

If we allow subset rules, we get:

***** SudoRules version 13 *****
.4..72.6........9..7.49.5..796..1.5..1....8....3...6..9........6..134......9....8
;;; start common part
hidden singles ==> r1c3 = 9, r3c6 = 6, r2c2 = 6, r9c5 = 6, r5c4 = 6, r7c9 = 6, r8c9 = 5, r8c7 = 9, r2c5 = 1, r3c8 = 8
.49.72.6.
.6..1..9.
.7.49658.
796..1.5.
.1.6..8..
..3...6..
9.......6
6..1349.5
...96...8
interaction row r8 with block b7 for number 8 ==> r7c3 <> 8, r7c2 <> 8
interaction row r4 with block b5 for number 8 ==> r6c6 <> 8, r6c5 <> 8, r6c4 <> 8
interaction column c2 with block b7 for number 3 ==> r9c1 <> 3
interaction block b8 with row r7 for number 2 ==> r7c8 <> 2, r7c7 <> 2, r7c3 <> 2, r7c2 <> 2
;;; end common part

naked-pairs-in-a-row {n1 n3}r1{c7 c9} ==> r1c4 <> 3
interaction block b2 with row r2 for number 3 ==> r2c9 <> 3, r2c7 <> 3, r2c1 <> 3
naked-pairs-in-a-row {n1 n3}r1{c7 c9} ==> r1c1 <> 3
hidden-single-in-a-block ==> r3c1 = 3
naked-pairs-in-a-row {n1 n3}r1{c7 c9} ==> r1c1 <> 1
naked and hidden singles ==> r3c3 = 1, r3c9 = 2, r9c1 = 1
interaction column c1 with block b4 for number 4 ==> r5c3 <> 4
;;; at this point, the decided values are:
.49.72.6.
.6..1..9.
371496582
796..1.5.
.1.6..8..
..3...6..
9.......6
6..1349.5
1..96...8
;;; end equivalent parts

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; restrictive naked triplets (we can check that we have all 3 values in all 3 cells):
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
naked-triplets-in-a-row {n4 n5 n2}r5{c1 c3 c5} ==> r5c9 <> 4
naked-triplets-in-a-row {n4 n5 n2}r5{c1 c3 c5} ==> r5c8 <> 4 ;;; this elimination can't be done by any equivalent nrczt3-chain
naked-triplets-in-a-row {n4 n5 n2}r5{c1 c3 c5} ==> r5c8 <> 2
naked-triplets-in-a-row {n4 n5 n2}r5{c1 c3 c5} ==> r5c6 <> 5
xy3-chain {n7 n4}r2c9 - {n4 n3}r4c9 - {n3 n7}r5c8 ==> r6c9 <> 7, r5c9 <> 7
naked and hidden singles ==> r2c9 = 7, r2c7 = 4
interaction column c7 with block b9 for number 7 ==> r9c8 <> 7, r8c8 <> 7
naked and hidden singles ==> r8c8 = 2, r8c2 = 8, r8c3 = 7, r6c1 = 8, r1c1 = 5, r2c1 = 2, r5c1 = 4, r2c3 = 8, r1c4 = 8, r4c5 = 8, r7c6 = 8, r6c5 = 4, r4c9 = 4, r4c7 = 2, r4c4 = 3, r2c4 = 5, r2c6 = 3
interaction column c7 with block b9 for number 7 ==> r7c8 <> 7
nrc2-chain n5{r9c6 r7c5} - n5{r5c5 r5c3} ==> r9c3 <> 5
x-wing-in-columns n5{r5 r7}{c3 c5} ==> r7c2 <> 5
naked-single ==> r7c2 = 3
nrc3-chain n7{r7c4 r7c7} - n1{r7c7 r7c8} - {n1 n7}r6c8 ==> r6c4 <> 7
naked singles
GRID 220 SOLVED. LEVEL = L3, MOST COMPLEX RULE = NRC3
549872361
268513497
371496582
796381254
412659873
853247619
935728146
687134925
124965738


Without subset rules
CLIPS> (solve-nth-grid-from-text-file (str-cat ?*PuzzlesDir* "Sudogen/sudogen0.txt" 220)
***** SudoRules version 13 *****
.4..72.6........9..7.49.5..796..1.5..1....8....3...6..9........6..134......9....8
;;; start common part
hidden singles ==> r1c3 = 9, r3c6 = 6, r2c2 = 6, r9c5 = 6, r5c4 = 6, r7c9 = 6, r8c9 = 5, r8c7 = 9, r2c5 = 1, r3c8 = 8
.49.72.6.
.6..1..9.
.7.49658.
796..1.5.
.1.6..8..
..3...6..
9.......6
6..1349.5
...96...8
interaction row r8 with block b7 for number 8 ==> r7c3 <> 8, r7c2 <> 8
interaction row r4 with block b5 for number 8 ==> r6c6 <> 8, r6c5 <> 8, r6c4 <> 8
interaction column c2 with block b7 for number 3 ==> r9c1 <> 3
interaction block b8 with row r7 for number 2 ==> r7c8 <> 2, r7c7 <> 2, r7c3 <> 2, r7c2 <> 2
;;; end common part

nrczt2-chain n5{r1c1 r1c4} - n8{r1c4 r1c1} ==> r1c1 <> 1
interaction row r1 with block b3 for number 1 ==> r3c9 <> 1
nrczt2-chain n5{r1c1 r1c4} - n8{r1c4 r1c1} ==> r1c1 <> 3
nrczt2-chain n5{r1c4 r1c1} - n8{r1c1 r1c4} ==> r1c4 <> 3
interaction row r1 with block b3 for number 3 ==> r3c9 <> 3
naked and hidden singles ==> r3c9 = 2, r3c3 = 1, r3c1 = 3, r9c1 = 1
interaction column c1 with block b4 for number 4 ==> r5c3 <> 4
interaction row r1 with block b3 for number 3 ==> r2c9 <> 3, r2c7 <> 3
;;; end equivalent parts
;;; notice that, although the state can easily be checked to be the same as above, the resolution path is different: the naked pairs haven't been replaced by equivalent nrczt2 chains (but they could have); this is because there are many resolution paths and which one is chosen by SudoRules can't be guaranteed.

nrczt3-chain n1{r6c8 r6c9} - {n1 n3}r1c9 - {n3 n4}r4c9 ==> r6c8 <> 4
nrczt3-chain n5{r6c5 r7c5} - n2{r7c5 r7c4} - n7{r7c4 r6c4} ==> r6c4 <> 5
nrczt3-chain n9{r5c9 r5c6} - n3{r5c6 r5c8} - n7{r5c8 r5c9} ==> r5c9 <> 4
nrczt3-lr-lasso n9{r5c6 r5c9} - n3{r5c9 r5c8} - n7{r5c8 r5c9} ==> r5c6 <> 5
nrczt3-lr-lasso {n2 n5}r5c3 - {n5 n4}r5c1 - {n4 n5}r5c5 ==> r5c8 <> 2
nrczt4-lr-lasso {n4 n3}r4c9 - n3{r5c9 r5c6} - n7{r5c6 r5c9} - n9{r5c9 r5c6} ==> r5c8 <> 4 ;;; instead of triplet rule above
interaction column c8 with block b9 for number 4 ==> r9c7 <> 4
interaction column c8 with block b9 for number 4 ==> r7c7 <> 4
nrczt3-lr-lasso {n4 n3}r4c9 - {n3 n7}r5c8 - n7{r6c9 r5c9} ==> r2c9 <> 4
naked singles ==> r2c9 = 7, r2c7 = 4
interaction column c7 with block b9 for number 7 ==> r9c8 <> 7, r8c8 <> 7
naked and hidden singles ==> r8c8 = 2, r8c2 = 8, r8c3 = 7, r6c1 = 8, r1c1 = 5, r2c1 = 2, r5c1 = 4, r2c3 = 8, r1c4 = 8, r4c5 = 8, r7c6 = 8, r6c5 = 4, r4c9 = 4, r4c7 = 2, r4c4 = 3, r2c4 = 5, r2c6 = 3
interaction column c7 with block b9 for number 7 ==> r7c8 <> 7
nrczt2-chain n5{r5c3 r5c5} - n5{r7c5 r9c6} ==> r9c3 <> 5
nrczt2-chain n5{r6c2 r6c6} - n5{r9c6 r9c2} ==> r7c2 <> 5
naked-single ==> r7c2 = 3
nrczt3-chain n1{r7c7 r7c8} - {n1 n7}r6c8 - n7{r6c4 r7c4} ==> r7c7 <> 7
naked-singles
GRID 220 SOLVED. LEVEL = L4, MOST COMPLEX RULE = NRCZT4
549872361
268513497
371496582
796381254
412659873
853247619
935728146
687134925
124965738

WHIPS

Partial xy-chains [resp. xyt, xyz, xyzt] allow eliminations that seem to have been unnoticed until now. The same general principle can be extended to all the types of chains I've introduced.

Contrary to chains that must be closed on the target, or to lassos that must be closed on a previous left- or right- linking candidate, whips remain open ended. Whence the name I chose for them.


Definition: an xy-whip of length n is a partial xy-chain of length n-1 plus a nth left-linking candidate (call it nrc) such that at least one of the following conditions is true:
- every candidate in rc-cell rc is nrc-linked to a previous right-linking candidate [or, for chains containing the z-extension: to the pre-selected target]
- every candidate in rn-cell rn is nrc-linked to a previous right-linking candidate [or, for chains containing the z-extension: to the pre-selected target]
- every candidate in cn-cell cn is nrc-linked to a previous right-linking candidate [or, for chains containing the z-extension: to the pre-selected target]
- every candidate in bn-cell bn is nrc-linked to a previous right-linking candidate [or, for chains containing the z-extension: to the pre-selected target], where b is the block of cell rc.

Example of an xy4-whip
{n1 n2}r1c1 - {n2 n3}r2c2 - {n3 n4}r3c3 - {n4 ...}r4c4
with each of the cells r2c2, r3c3 and r4c4 sharing a unit with the previous one and with n4r4c4 satisfying the conditions of the definition.
The "..." indicate that the definition of the last cell is not yet finished.

Theorem: given an xy-whip [resp. an xyt- xyz- xyzt- whip] of length >1, any candidate z that is nrc-linked to the first left-linking candidate [resp. for chains containing the z-extension: to the pre-selected target z] can be eliminated.

Proof:
first recall the partial xy-chain [resp. xyt- xyz- xyzt-] theorem: given a potential target, if it was true, then any left-linking candidate would be false and any right-linking candidate would be true.

In the given situation, we have a left-linking candidate nrc which leaves no possibility for having a candidate true in cell rc or no possibility for having a candidate true in rn-cell rn or no possibility for having a candidate true in cn-cell cn or no possibility for having a candidate true in bn-cell bn, where b is the block of rc-cell rc.
Conclusion: either z is false or the puzzle has no solution.
But if the puzzle has no solution, eliminating z from its candidates won't make it have fewer solutions.
We can therefore always conclude that z can be eliminated.


This theorem can be extended in an obvious way to the hidden counterparts of the above 2D chains [hxy, hxyt, hxyz, hxyzt] and to the fully supersymmetric chains [nrc, nrct, nrcz, nrczt], using the corresponding partial chain theorem.



First easy example: Sudogen0 #23
***** SudoRules version 13.7w *****
.16..5...
.7.4.9...
..98....4
.4.....29
...54....
.2..6.1.8
..1....3.
......6.5
....8....

hidden-singles ==> r1c1 = 4, r4c1 = 6, r5c1 = 1, r5c2 = 9, r6c4 = 9, r5c6 = 2, r4c6 = 8, r5c3 = 8, r2c1 = 8, r6c8 = 4, r4c7 = 5, r7c5 = 5, r8c5 = 9, r3c6 = 6
interaction column c5 with block b2 for number 2 ==> r1c4 <> 2
interaction column c6 with block b8 for number 1 ==> r9c4 <> 1, r8c4 <> 1
hidden-single-in-a-column ==> r4c4 = 1
hidden-pairs-in-a-row {n8 n9}r1{c7 c8} ==> r1c8 <> 7, r1c7 <> 7, r1c7 <> 3, r1c7 <> 2

At this point, the PM is:

Code: Select all

+-------------------------+-------------------------+-------------------------+
|4       1       6        |37      237     5        |89      89      237      |
|8       7       235      |4       123     9        |23      156     1236     |
|235     35      9        |8       1237    6        |237     157     4        |
+-------------------------+-------------------------+-------------------------+
|6       4       37       |1       37      8        |5       2       9        |
|1       9       8        |5       4       2        |37      67      367      |
|357     2       357      |9       6       37       |1       4       8        |
+-------------------------+-------------------------+-------------------------+
|279     68      1        |267     5       47       |24789   3       27       |
|237     38      2347     |237     9       1347     |6       178     5        |
|23579   356     23457    |2367    8       1347     |2479    179     127      |
+-------------------------+-------------------------+-------------------------+


and we get our first xyz-whip:

xyz2-whip n3{r3c1 r2c3 r3c2*} - r4n3{c3 . c5*} ==> r3c5 <> 3 (the dot in the last rn-cell indicates the impossibility of having any right-linking candidate)

Nothing new in the sequel:
naked-triplets-in-a-column {n3 n2 n7}{r2 r3 r5}c7 ==> r9c7 <> 7, r9c7 <> 2, r7c7 <> 7, r7c7 <> 2
interaction column c7 with block b3 for number 2 ==> r2c9 <> 2, r1c9 <> 2
hidden-single-in-a-row ==> r1c5 = 2
naked-triplets-in-a-block {n7 n3 n2}{r1c9 r2c7 r3c7} ==> r3c8 <> 7, r2c9 <> 3
nrc3-chain {n2 n7}r7c9 - n7{r1c9 r3c7} - n2{r3c7 r3c1} ==> r7c1 <> 2
nrc3-chain n1{r8c6 r8c8} - n8{r8c8 r7c7} - n4{r7c7 r7c6} ==> r8c6 <> 4
hidden-single-in-a-row ==> r8c3 = 4
nrc4-chain n1{r8c6 r9c6} - n1{r9c9 r2c9} - {n1 n3}r2c5 - n3{r4c5 r6c6} ==> r8c6 <> 3
nrc2-chain n3{r9c6 r6c6} - n3{r4c5 r4c3} ==> r9c3 <> 3
nrc4-chain n7{r1c9 r3c7} - n2{r3c7 r3c1} - n2{r2c3 r9c3} - n2{r9c9 r7c9} ==> r7c9 <> 7
naked-single ==> r7c9 = 2
nrct3-chain n6{r9c2 r9c4} - n2{r9c4 r8c4} - n3{r8c4 r9c6} ==> r9c2 <> 3
xy4-chain {n3 n7}r1c4 - {n7 n6}r7c4 - {n6 n8}r7c2 - {n8 n3}r8c2 ==> r8c4 <> 3
interaction row r8 with block b7 for number 3 ==> r9c1 <> 3
nrc4-chain n8{r8c8 r8c2} - {n8 n6}r7c2 - {n6 n7}r7c4 - {n7 n1}r8c6 ==> r8c8 <> 1
hidden-single-in-a-row ==> r8c6 = 1
nrc4-chain n2{r9c3 r2c3} - n2{r3c1 r3c7} - n7{r3c7 r3c5} - n7{r4c5 r4c3} ==> r9c3 <> 7
interaction column c3 with block b4 for number 7 ==> r6c1 <> 7
nrc3-chain {n5 n3}r6c1 - n3{r8c1 r8c2} - {n3 n5}r3c2 ==> r3c1 <> 5
nrczt4-lr-lasso n7{r7c4 r7c1} - n7{r8c1 r8c8} - n8{r8c8 r7c7} - n9{r7c7 r7c1} ==> r9c4 <> 7
nrczt4-lr-lasso n7{r7c4 r7c1} - n7{r8c1 r8c8} - n8{r8c8 r7c7} - n9{r7c7 r7c1} ==> r9c6 <> 7
xy5-chain {n1 n5}r3c8 - {n5 n3}r3c2 - {n3 n8}r8c2 - {n8 n7}r8c8 - {n7 n1}r9c9 ==> r9c8 <> 1
naked and hidden singles ==> r9c9 = 1, r2c9 = 6, r5c8 = 6
nrc5-chain n6{r9c2 r9c4} - n3{r9c4 r1c4} - {n3 n1}r2c5 - {n1 n5}r2c8 - n5{r3c8 r3c2} ==> r9c2 <> 5
naked-singles
GRID 23 SOLVED. LEVEL = L5, MOST COMPLEX RULE = NRC5
416325897
872419356
359876214
647138529
198542763
523967148
781654932
234791685
965283471

Consider this only as a first illustrative example. I know this puzzle can be solved without whipping it, with the same most complex nrc5 chain rule.

I don't have much time for Sudoku now that my students are back, but I'll try to find more interesting examples.
From my first blind computations with SudoRules, it appears that, the longer the chains in a resolution path, the more useful the whips are to find a solution with shorter chains.
From these preliminary computations, whips seem to appear "often" in hard puzzles that have few chains ("often", very long chains can be found in such puzzles).
As a result, contrary to lassos, "often", the introduction of whips significantly shortens the maximum length of the chains needed to solve a puzzle.
What "often" means and global classifcation results with these new resolution rules will appear as soon as I have time to run the necessary systematic computations.

Here is another interesting example of an instance of Ruud's diagonal pattern (#42 in the list of 100 provides by JPF: http://forum.enjoysudoku.com/viewtopic.php?t=4212&postdays=0&postorder=asc&start=870).
(As I mentioned previously, this pattern is very interesting and I've already given an example of it. I'ven't studied all the 100 instances provided by JPF, but the few cases I've tried show that it allows nrczt solutions for puzzles with SER higher than usual.)
This puzzle with SER 9.4 needs nrczt-chains and lassos of length 17.


1..2..3..
....4..5.
..2..6...
7..3..5..
.4..8..7.
..9.....6
9..5..4..
....2..1.
..7..1..8

***** SudoRules version 13.4 *****
1..2..3......4..5...2..6...7..3..5...4..8..7...9.....69..5..4......2..1...7..1..8
hidden-single-in-a-column ==> r8c9 = 5
nrczt12-rl-lasso n5{r9c1 r9c2} - n5{r3c2 r3c5} - n5{r6c5 r6c6} - n5{r1c6 r1c3} - n4{r1c3 r8c3} - n4{r9c1 r3c1} - n3{r3c1 r3c2} - n3{r3c5 r2c6} - n3{r8c6 r8c1} - n3{r6c1 r6c8} - n4{r6c8 r6c4} - n4{r9c4 r9c1} ==> r5c1 <> 5
nrczt16-chain n4{r9c4 r9c1} - n4{r8c3 r1c3} - n5{r1c3 r5c3} - n6{r5c3 r5c1} - n2{r5c1 r6c1} - n5{r6c1 r3c1} - n5{r9c1 r9c2} - n2{r9c2 r7c2} - n1{r7c2 r7c3} - {n1 n8}r4c3 - {n8 n1}r4c2 - {n1 n3}r6c2 - n3{r3c2 r3c5} - n3{r9c5 r9c8} - {n3 n7}r7c9 - {n7 n6}r7c5 ==> r9c4 <> 6
nrczt17-chain n4{r8c3 r1c3} - n4{r3c1 r9c1} - {n4 n9}r9c4 - n9{r8c6 r8c7} - n7{r8c7 r7c9} - {n7 n9}r1c9 - n9{r3c8 r4c8} - n9{r4c5 r3c5} - n9{r3c2 r2c2} - n9{r2c6 r5c6} - n5{r5c6 r5c3} - n5{r6c1 r3c1} - n3{r3c1 r3c2} - n7{r3c2 r1c2} - n7{r1c5 r6c5} - n1{r6c5 r4c5} - {n1 n4}r6c4 ==> r8c4 <> 4
nrczt17-chain n4{r8c3 r1c3} - n4{r3c1 r9c1} - {n4 n9}r9c4 - n9{r8c4 r8c7} - n7{r8c7 r7c9} - {n7 n9}r1c9 - n9{r3c8 r4c8} - n9{r4c5 r3c5} - n3{r3c5 r2c6} - n9{r2c6 r5c6} - n5{r5c6 r5c3} - n5{r6c1 r3c1} - n3{r3c1 r3c2} - n9{r3c2 r2c2} - n7{r2c2 r1c2} - n7{r1c5 r6c5} - n7{r6c6 r8c6} ==> r8c6 <> 4
hidden-single-in-a-block ==> r9c4 = 4
nrczt13-lr-lasso {n1 n7}r6c4 - {n7 n5}r6c5 - n5{r5c6 r1c6} - n5{r1c3 r5c3} - n6{r5c3 r5c1} - n6{r5c4 r4c5} - n1{r4c5 r3c5} - n3{r3c5 r2c6} - {n3 n8}r2c1 - {n8 n6}r2c3 - n6{r1c2 r1c8} - {n6 n4}r1c3 - n8{r1c3 r1c2} ==> r5c4 <> 1
nrczt4-chain n1{r5c9 r5c3} - n5{r5c3 r5c6} - {n5 n7}r6c5 - {n7 n1}r6c4 ==> r6c7 <> 1
nrczt16-lr-lasso {n7 n1}r6c4 - n1{r4c5 r3c5} - n3{r3c5 r2c6} - {n3 n8}r7c6 - {n8 n9}r8c6 - {n9 n5}r1c6 - {n5 n2}r5c6 - {n2 n4}r4c6 - n4{r6c6 r6c8} - n3{r6c8 r5c9} - {n3 n6}r5c1 - {n6 n8}r2c1 - {n8 n6}r2c3 - n6{r1c2 r1c8} - {n6 n4}r1c3 - n8{r1c3 r1c2} ==> r6c6 <> 7
nrczt14-chain {n7 n1}r6c4 - n1{r4c5 r3c5} - n3{r3c5 r2c6} - {n3 n8}r7c6 - {n8 n9}r8c6 - n7{r8c6 r1c6} - n5{r1c6 r1c5} - n5{r1c3 r5c3} - n5{r5c6 r6c6} - n4{r6c6 r6c8} - n3{r6c8 r5c9} - n1{r5c9 r5c7} - n9{r5c7 r5c4} - n6{r5c4 r8c4} ==> r8c4 <> 7
nrczt6-chain n3{r8c3 r8c6} - n7{r8c6 r8c7} - {n7 n2}r7c9 - n2{r2c9 r2c7} - n6{r2c7 r9c7} - {n6 n3}r7c8 ==> r7c3 <> 3
nrczt6-rl-lasso n5{r5c3 r1c3} - n4{r1c3 r8c3} - n3{r8c3 r2c3} - n3{r2c6 r3c5} - n5{r3c5 r6c5} - n5{r5c6 r5c3} ==> r5c3 <> 6
nrczt6-rl-lasso n5{r5c3 r1c3} - n4{r1c3 r8c3} - n3{r8c3 r2c3} - n3{r2c6 r3c5} - n5{r3c5 r6c5} - n5{r5c6 r5c3} ==> r5c3 <> 1
interaction row r5 with block b6 for number 1 ==> r4c9 <> 1
nrczt6-chain n3{r8c3 r8c6} - n7{r8c6 r8c7} - {n7 n2}r7c9 - n2{r2c9 r2c7} - n6{r2c7 r9c7} - {n6 n3}r7c8 ==> r7c2 <> 3
nrczt10-chain n3{r8c3 r8c6} - n7{r8c6 r8c7} - n9{r8c7 r8c4} - {n9 n6}r9c5 - n6{r9c7 r2c7} - n2{r2c7 r2c9} - {n2 n3}r7c9 - n3{r5c9 r5c3} - {n3 n8}r2c3 - {n8 n3}r2c1 ==> r9c1 <> 3
nrczt10-lr-lasso n6{r5c1 r5c4} - n6{r4c5 r7c5} - n6{r7c8 r1c8} - n6{r2c7 r8c7} - n7{r8c7 r8c6} - n9{r8c6 r8c4} - n8{r8c4 r7c6} - n3{r7c6 r2c6} - {n3 n8}r2c1 - n8{r1c2 r1c3} ==> r9c1 <> 6
nrczt15-lr-lasso n5{r9c1 r9c2} - n5{r3c2 r3c5} - n5{r1c6 r1c3} - n4{r1c3 r8c3} - n4{r8c1 r3c1} - n3{r3c1 r3c2} - n3{r8c2 r8c1} - n8{r8c1 r2c1} - n6{r2c1 r5c1} - n6{r5c4 r8c4} - {n6 n8}r8c2 - n8{r8c6 r7c6} - n8{r1c6 r1c8} - n6{r1c8 r2c7} - {n6 n3}r2c3 ==> r6c1 <> 5
nrczt10-lr-lasso {n8 n2}r6c7 - {n2 n3}r6c1 - {n3 n4}r6c8 - n4{r4c9 r4c6} - n2{r4c6 r5c6} - {n2 n6}r5c1 - {n6 n8}r2c1 - n8{r2c7 r3c7} - n8{r3c4 r8c4} - n6{r8c4 r5c4} ==> r6c2 <> 8
nrczt17-rl-lasso n5{r1c3 r5c3} - n5{r5c6 r6c6} - n5{r6c5 r3c5} - n3{r3c5 r2c6} - n3{r2c3 r8c3} - n4{r8c3 r1c3} - n6{r1c3 r1c8} - n8{r1c8 r1c6} - {n8 n7}r7c6 - {n7 n9}r8c6 - {n9 n2}r5c6 - {n2 n4}r4c6 - n4{r6c6 r6c8} - n3{r6c8 r5c9} - {n3 n6}r5c1 - n6{r5c4 r8c4} - n8{r8c4 r7c6} ==> r1c2 <> 5
nrczt17-rl-lasso {n2 n8}r6c7 - {n8 n3}r6c1 - {n3 n4}r6c8 - n4{r4c9 r4c6} - n2{r4c6 r5c6} - n2{r5c1 r9c1} - n5{r9c1 r3c1} - n4{r3c1 r8c1} - n8{r8c1 r2c1} - n6{r2c1 r5c1} - n6{r5c4 r8c4} - n8{r8c4 r3c4} - {n8 n9}r3c8 - {n9 n2}r4c8 - n2{r5c7 r2c7} - n6{r2c7 r1c8} - n8{r1c8 r3c8} ==> r6c2 <> 2
nrczt12-chain n3{r2c6 r3c5} - n3{r9c5 r9c8} - n3{r7c9 r5c9} - {n3 n5}r5c3 - {n5 n1}r6c2 - n1{r6c5 r4c5} - n6{r4c5 r5c4} - {n6 n2}r5c1 - {n2 n5}r9c1 - n5{r9c2 r3c2} - n7{r3c2 r1c2} - n9{r1c2 r2c2} ==> r2c2 <> 3
nrczt17-lr-lasso n1{r3c4 r6c4} - n7{r6c4 r6c5} - n5{r6c5 r1c5} - n5{r1c3 r5c3} - {n5 n3}r6c2 - n3{r6c8 r5c9} - n1{r5c9 r2c9} - n2{r2c9 r2c7} - {n2 n8}r6c7 - {n8 n2}r6c1 - {n2 n6}r5c1 - n6{r5c4 r8c4} - {n6 n8}r8c2 - n8{r4c2 r4c3} - n8{r7c3 r7c6} - n8{r1c6 r1c8} - n6{r1c8 r2c7} ==> r3c5 <> 1
interaction column c5 with block b5 for number 1 ==> r6c4 <> 1
naked-single ==> r6c4 = 7
nrczt15-chain n4{r3c1 r1c3} - n5{r1c3 r5c3} - n3{r5c3 r5c9} - n3{r6c8 r6c2} - n1{r6c2 r6c5} - n5{r6c5 r6c6} - n4{r6c6 r6c8} - n4{r3c8 r3c9} - n1{r3c9 r2c9} - n2{r2c9 r2c7} - n2{r6c7 r6c1} - {n2 n6}r5c1 - {n6 n9}r5c4 - {n9 n8}r2c4 - {n8 n3}r2c1 ==> r3c1 <> 3
nrczt10-rl-lasso n3{r3c5 r3c2} - n3{r9c2 r9c8} - n3{r6c8 r6c1} - {n3 n5}r5c3 - n5{r6c2 r9c2} - {n5 n2}r9c1 - {n2 n6}r5c1 - n6{r5c4 r4c5} - n1{r4c5 r6c5} - {n1 n5}r6c2 ==> r7c5 <> 3
nrczt10-lr-lasso n3{r3c5 r3c2} - n5{r3c2 r3c1} - n5{r9c1 r9c2} - {n5 n1}r6c2 - {n1 n5}r6c5 - {n5 n9}r1c5 - n9{r1c2 r2c2} - n7{r2c2 r1c2} - {n7 n4}r1c9 - n4{r1c3 r3c1} ==> r3c5 <> 7
nrczt9-chain n7{r7c9 r8c7} - n7{r3c7 r3c2} - n3{r3c2 r3c5} - n5{r3c5 r3c1} - n5{r9c1 r9c2} - n3{r9c2 r9c8} - n9{r9c8 r9c7} - n6{r9c7 r2c7} - n2{r2c7 r2c9} ==> r2c9 <> 7
nrczt9-lr-lasso n7{r3c7 r3c2} - n3{r3c2 r3c5} - n5{r3c5 r3c1} - n5{r9c1 r9c2} - n3{r9c2 r9c8} - {n3 n2}r7c9 - n2{r2c9 r2c7} - n6{r2c7 r1c8} - {n6 n2}r7c8 ==> r1c9 <> 7
nrczt6-chain {n4 n9}r1c9 - {n9 n8}r3c8 - {n8 n5}r3c1 - {n5 n2}r9c1 - n2{r7c2 r4c2} - {n2 n4}r4c9 ==> r3c9 <> 4
nrczt8-lr-lasso n7{r3c9 r7c9} - n3{r7c9 r5c9} - {n3 n5}r5c3 - n5{r1c3 r3c1} - {n5 n2}r9c1 - {n2 n6}r5c1 - n6{r5c4 r8c4} - {n6 n7}r7c5 ==> r3c2 <> 7
interaction row r3 with block b3 for number 7 ==> r2c7 <> 7
nrczt6-lr-lasso n7{r2c2 r2c6} - n7{r8c6 r8c7} - n6{r8c7 r9c7} - n9{r9c7 r9c8} - {n9 n3}r9c5 - n3{r3c5 r2c6} ==> r2c2 <> 6
nrczt7-rl-lasso n3{r3c5 r3c2} - n5{r3c2 r3c1} - n4{r3c1 r3c8} - {n4 n9}r1c9 - n9{r1c2 r2c2} - n7{r2c2 r2c6} - n3{r2c6 r3c5} ==> r3c5 <> 9
nrczt8-lr-lasso n2{r5c1 r9c1} - n5{r9c1 r3c1} - n4{r3c1 r3c8} - {n4 n9}r1c9 - {n9 n4}r4c9 - {n4 n9}r4c6 - n9{r4c8 r9c8} - n9{r9c5 r4c5} ==> r4c2 <> 2
interaction column c2 with block b7 for number 2 ==> r9c1 <> 2
naked-single ==> r9c1 = 5
hidden-pairs-in-a-row {n3 n5}r3{c2 c5} ==> r3c2 <> 9
hidden-pairs-in-a-block {n7 n9}{r1c2 r2c2} ==> r2c2 <> 8, r1c2 <> 8, r1c2 <> 6
hidden-pairs-in-a-row {n3 n5}r3{c2 c5} ==> r3c2 <> 8
nrczt4-chain n4{r8c3 r1c3} - n6{r1c3 r1c8} - n8{r1c8 r1c6} - n8{r7c6 r7c2} ==> r8c3 <> 8
hxyzt6-rn-chain {c8 c3}r1n6 - {c3 c6}r1n8 - {c6 c5}r1n5 - {c5 c2}r3n5 - {c2 c6}r6n5 - {c6 c8}r6n4 ==> r1c8 <> 4
nrct6-chain {n4 n9}r1c9 - {n9 n7}r1c2 - {n7 n5}r1c5 - n5{r3c5 r3c2} - n5{r6c2 r6c6} - n4{r6c6 r6c8} ==> r4c9 <> 4
naked and hidden singles ==> r1c9 = 4, r3c1 = 4, r8c3 = 4
nrc3-chain n3{r2c3 r5c3} - n5{r5c3 r1c3} - {n5 n3}r3c2 ==> r2c1 <> 3
nrczt3-chain n4{r4c8 r4c6} - n2{r4c6 r4c9} - {n2 n8}r6c7 ==> r4c8 <> 8
interaction row r4 with block b4 for number 8 ==> r6c1 <> 8
nrczt2-chain n8{r2c1 r8c1} - n8{r8c4 r3c4} ==> r2c6 <> 8
naked-triplets-in-a-row {n2 n4 n9}r4{c6 c8 c9} ==> r4c5 <> 9
nrct3-chain n3{r2c3 r5c3} - n3{r6c1 r8c1} - n8{r8c1 r2c1} ==> r2c3 <> 8
nrczt3-chain n9{r8c7 r9c8} - n9{r9c5 r1c5} - n9{r3c4 r3c9} ==> r2c7 <> 9
nrczt3-chain n6{r9c2 r4c2} - {n6 n1}r4c5 - n1{r4c3 r7c3} ==> r7c3 <> 6
nrc4-chain n7{r2c6 r2c2} - {n7 n9}r1c2 - n9{r1c5 r9c5} - n3{r9c5 r3c5} ==> r2c6 <> 3
naked and hidden singles ==> r3c5 = 3, ==> r3c2 = 5, r5c3 = 5, r2c3 = 3
naked-pairs-in-a-row {n7 n9}r2{c2 c6} ==> r2c9 <> 9, r2c4 <> 9
nrc3-chain {n9 n2}r4c9 - {n2 n1}r2c9 - n1{r5c9 r5c7} ==> r5c7 <> 9
nrczt3-chain n9{r5c6 r5c4} - n6{r5c4 r8c4} - {n6 n9}r9c5 ==> r8c6 <> 9
nrc3-chain n9{r8c4 r8c7} - n7{r8c7 r7c9} - {n7 n6}r7c5 ==> r8c4 <> 6
naked and hidden singles ==> r5c4 = 6, r4c5 = 1, r6c5 = 5, r1c6 = 5, r6c2 = 1, r7c3 = 1
interaction column c2 with block b7 for number 3 ==> r8c1 <> 3
interaction column c6 with block b8 for number 8 ==> r8c4 <> 8
naked and hidden singles
GRID 0 SOLVED. LEVEL = L17, MOST COMPLEX RULE = NRCZT17
176295384
893147652
452836197
768312549
345689271
219754836
921578463
684923715
537461928

Whip example deleted.
There was a stupid bug in nrczt-whip[11]: one line missing in a copy-paste.

denis_berthier wrote:and we get our first xyz-whip:

xyz2-whip n3{r3c1 r2c3 r3c2*} - r4n3{c3 . c5*} ==> r3c5 <> 3 (the dot in the last rn-cell indicates the impossibility of having any right-linking candidate)

All I see is ... n3{r4c5 r4c3} - n3{r2c3 r3c12}

Have you got a better illustraton ... with more than one digit value

ronk wrote:

denis_berthier wrote:and we get our first xyz-whip:

xyz2-whip n3{r3c1 r2c3 r3c2*} - r4n3{c3 . c5*} ==> r3c5 <> 3 (the dot in the last rn-cell indicates the impossibility of having any right-linking candidate)

All I see is ... n3{r4c5 r4c3} - n3{r2c3 r3c12}

Have you got a better illustraton ... with more than one digit value

No wonder you can find other patterns on other cells.
This nevertheless remains a good elementary example.
If you want more complex examples, look at the 2nd post after that one.

denis_berthier wrote:[b]

Code: Select all

+-------------------------+-------------------------+-------------------------+
|4       1       6        |37      237     5        |89      89      237      |
|8       7       235      |4       123     9        |23      156     1236     |
|235     35      9        |8       1237    6        |237     157     4        |
+-------------------------+-------------------------+-------------------------+
|6       4       37       |1       37      8        |5       2       9        |
|1       9       8        |5       4       2        |37      67      367      |
|357     2       357      |9       6       37       |1       4       8        |
+-------------------------+-------------------------+-------------------------+
|279     68      1        |267     5       47       |24789   3       27       |
|237     38      2347     |237     9       1347     |6       178     5        |
|23579   356     23457    |2367    8       1347     |2479    179     127      |
+-------------------------+-------------------------+-------------------------+


I do not catch why the solver does not find at that point easy next move

r1c5=2

champagne

champagne wrote:I do not catch why the solver does not find at that point easy next move
r1c5=2
champagne

The next steps are:

Code: Select all

naked-triplets-in-a-column {n3 n2 n7}{r2 r3 r5}c7 ==> r9c7 <> 7, r9c7 <> 2, r7c7 <> 7, r7c7 <> 2
interaction column c7 with block b3 for number 2 ==> r2c9 <> 2, r1c9 <> 2
hidden-single-in-a-row ==> r1c5 = 2

One first reason is that the only rules that assert values in SudoRules are NS and HS.
For a more detailed answer, I need to know what "easy next move" you are invoking. It is likely to be given a lower prioritiy than triplets and basic interactions in SudoRules default strategy.

denis_berthier wrote:

champagne wrote:I do not catch why the solver does not find at that point easy next move
r1c5=2
champagne

The next steps are:

Code: Select all

naked-triplets-in-a-column {n3 n2 n7}{r2 r3 r5}c7 ==> r9c7 <> 7, r9c7 <> 2, r7c7 <> 7, r7c7 <> 2
interaction column c7 with block b3 for number 2 ==> r2c9 <> 2, r1c9 <> 2
hidden-single-in-a-row ==> r1c5 = 2

One first reason is that the only rules that assert values in SudoRules are NS and HS.
For a more detailed answer, I need to know what "easy next move" you are invoking. It is likely to be given a lower prioritiy than triplets and basic interactions in SudoRules default strategy.

you have it but why not before that whisp!!! It was already there.

champagne wrote:you have it but why not before that whisp!!! It was already there.

Yes, the Triplets was already there. But nrczt-whip[2] has higher priority than Triplets in the default strategy, which is based on the number of (rc-, rn-, cn- and bn-) cells necessary to define a pattern.
This choice is consistent with the general pattern for non-degenerate Triplets:
{1 2 (3)} - {2 3 (1)} - {3 1 (2)} (parens indicate optional candidates, all the others are compulsory)
which is very close to the pattern for xy-chain[3]
{1 2} - {2 3} - {3 1}

I plan to tell more about strategies in general as soon as I've time.

denis_berthier wrote:Yes, the Triplets was already there. But nrczt-whip[2] has higher priority than Triplets in the default strategy, which is based on the number of (rc-, rn-, cn- and bn-) cells necessary to define a pattern.
This choice is consistent with the general pattern for non-degenerate Triplets:
{1 2 (3)} - {2 3 (1)} - {3 1 (2)} (parens indicate optional candidates, all the others are compulsory)
which is very close to the pattern for xy-chain[3]
{1 2} - {2 3} - {3 1}

I plan to tell more about strategies in general as soon as I've time.

There I am lost.

Any "nearly beginner" player would have found that step on a "pencil mark" basis in ten seconds. How long would he have to work to find a "whisp".

denis_berthier wrote:If you want more complex examples, look at the 2nd post after that one.

No thanks. I'll take a look at a more complex example of a "whip" ... when you provide an illustration for one.

champagne wrote:Any "nearly beginner" player would have found that step on a "pencil mark" basis in ten seconds. How long would he have to work to find a "whisp".

SudoRules default strategy is tied to the NRCZT-rating.
The backbone of the NRCZT-rating is the various chains in the xy to nrczt family.
The basis of this rating is the length of the chains (lassos and now also whips (not whisps).
Other patterns have to be inserted in this natural hierarchy. General principles for this must be devised. There are many possibilities - and many strategies. None of these will reflect faithfully a human's behaviour.

Moreover, given some pattern, say quads or xy-chain[6], some instances will be much easier to find than others, depending on many parameters (position on the grid, ...). No absolute classification of patterns is possible.
SudoRules default strategy is based on the length. I'll speak of other possibilities later, combining length and type.

The NRCZT-rating may be debated, as any rating. But statistics show that it is globally not so absurd.

I've noticed that nrczt-whip[n] = nrczt-chain[n] or nrczt-lasso[n].

The notion is therefore not a new extension of nrczt chains or lassos, but I'll soon explain that it remains interesting.

No time right now.

NRCZT- CHAINS, LASSOS AND WHIPS

As many of us I think, I've started with the idea that the two ends of a chain must be linked to any of its targets.
After introducing several new types of chains based on this idea, I've discovereed lr-lassos, whose tail is linked to a previous right-linking candidate instead of the target (and rl-lassos, which can be considered as a special case of lr-lassos)
Trying to see if other kinds of contradictions can be obtained from a partial chain, I recently found whips, which are open ended (a left-linking candidate in a 2D-cell with no possibility for a right-linking candidate in this cell, compatible with both the target and the previous right-linking candidates).

I now realise that the (non disjoint) union of chains and lassos is equivalent to whips.

Theorem: the set of nrczt-whips of length n is equal to the set of nrczt chains and lassos of length n.

Abbreviations used: rlc (llc) rigth- (left-) linking candidate.
Proof:
It is obvious that chains and lassos can be considered as whips:
- for chains, the last rlc is nrc-linked to the target; it is therefore an impossible value in the last rc-, rn-, cn- or bn- cell of the partial chain;
- for lr-lassos, the last rlc is nrc-linked to a previous rlc; it is therefore an impossible value in the last rc-, rn-, cn- or bn- cell of the partial chain;
- for rl-lassos, the last rcl is equal to a previous lrc (which is nrc-linked to an rlc: the next one); it is therefore an impossible value in the last rc-, rn-, cn- or bn- cell of the partial chain.
In each case, the last cell has no possible rlc non linked to a previous rlc or to the target.

Conversely, given a whip, let nrc be its last llc; by definition, there is a rc-, rn-, cn- or bn- cell containing nrc such that each of its candidates is nrc-linked to a previous rlc or to the target. We thus have a lr-lasso or a chain.

The distinction between chains and lassos is based on whether there is a z-candidate in the last cell. But in the nrczt context, this may be considered immaterial.
What becomes more interesting is whether the last cell (with no remaining possibility for a right-linking candidate) is an rc-, rn-, cn- or bn- cell. Depending on this 2D space, we get nrczt-whip-rc, nrczt-whip-rn, nrczt-whip-cn, nrczt-whip-bn.
This is secondary from a conceptual POV but this indication may be helpful when reading the resolution path, if one wants to be able to check the contradiction easily. I'm going to implement this in SudoRules as soon as possible, with whips replacing chains and lassos.


By virtue of the above theorem, is the notion of a whip useless?
From the POV of finding new eliminations, it is useless.
But, fromother POVs, it is not useless, because:
- it unites 2 notions that where separated until now;
- it remains useful for xy-chains or nrc-chains (= basic Nice Loops); it still allows to draw conclusions that weren't classically drawn from such chains. (Of course this doesn't add to them when we consider them as special cases of xyzt or nrczt chains; but it may be a transition step from xy/nrc to xyzt/nrczt).
- it simplifies the proof of the confluence property for well built theories with nrczt-chains and lassos; (see a forthcoming post);
- at the implementation level, it allows efficiency gains (factor 2 in both speed and memory, independently of the length of the chains - this factor 2 is true with extremely high correlation: 0.99, i.e. for almost any puzzle).