The New Sudoku Players' Forum

[Steve K]

It is indeed unforturnate that the stuff of many classical sudoku chains is poorly served by the definitions of strong and weak links. For this reason, I find it less ambiguous to use the terms strong inference and weak inference, or alternatively just OR and NAND.

It is relatively easy to write chains that use OR and NAND as resoltution rules. One merely needs to make the stuff that these chains consider "cell equivalents". A cell equivalent is any container such that its objects have the following property: Exactly one is true.

One need not restrict cell equivalents to natural sudoku containers. Cell equivalents immediately allow the use of ALS, HALS, and many other Almost patterns. In order to infuse some patterns into chains, one may wish to add semi-cell equivalents. Two types of semi-cell equivalents come to mind: One in which At least one item is true, and one in which at most one items it true. In most cases, the use of semi-cell equivalents is not required - but, for example, to chain an almost Y wing into a pattern, one can usually only define a container that has the strong inference quality.

In any event, sudoku solving is generally viewed as a form of entertainment, and personally I find the use of such concepts to be highly entertaining. The percent of puzzles solved by a particular technique or idea by a computer really is not relevant to the entertainment value of technique set.

The Easter Monster - I have taken an opening salvo at this beast, using precise resolution rules based upon exactly the type of cell equivalents described above. The following step is most properly similar to Denis' C-chains. Regardless of whether this step is viewed as proper or not, 'tis highly entertaining, and speaks volumes for the value of this type of non-adhoc logic.

To best find this chain independently, study the grid before entering the possibilities.

(2=7)r13c2=(2&7)r56c2 (this is a typical cell equivalent type argument, and makes the finding of such chains much easier.)
It is known that amongst the 4 cells, r1356, there exists one permutation of candidates 2,7 per possible solution. One can then partition that cell equivalent snippet as one sees fit. This is precisely analagous to the partitioning of a cell when using, for example, t-chains.

(2=7)r13c2=(2&7-1&6)r56c2=(1&6)r79c2-(1&6)r8c13=(1&6-2&7)r8c45=(2&7)r8c79-(2&7)r79c8=(2&7-1&6)r45c8=(1&6)r13c8-(1&6)r2c79=(1&6-2&7)r2c56=(2=&7)r2c13

The following is eliminated by this chain:
(7)r1c3, (2)r3c1, (1)r7c3, (6)r9c1
Also, the following cells are resticted to candidates 1267:
r56c2,r8c45,r45c8,r2c56
for a total of 13 eliminations. The puzzle is still a monster after this point, just a tad less angry!

The opening boolean argument, (2=7) is intentionally written that way, as it serves as the compression vehicle for the balance of the cell equivalents, or super cells. The compression for the rest of the chain is a bit different, as the chain itself allows one to consider each of the cell groups and pertinent candidate groups as if they were merely bilocation relationships between only two candidates.

Compression into cell equivalents can be done along any primitive strong inference, and also groups of same (although often within a common container).

Finally, the = and - signs are merely a convenience, as they illustrate the preferred partioning of the cell equivalents. Such a partioning is actually arbitrary and superfluous.

Relatively complexity is difficult to measure. This particular chain, to me, feels like a conjugate chain of length 8.

[denis_berthier]

Steve,
Congratulations for this very beautiful step in solving Easter Monster.
The homogeneity of this pattern is in keeping with the philosophy of resolution rules.
Formulating precisely the underlying general resolution rule remains to be done, but it is too beautiful to be impossible
The notions of a "cell equivalent", of a "container" and of an "object of a container" should be given precise definitions.

Let me write the proof that goes with your chain, as I see it:
if {r1 r3}c2 doesn't meet {2 7}, then {r5 r6}c2 = {2 7}
if {r5 r6}c2 = {2 7}, then {r5 r6}c2 doesn't meet {1 6}
if {r5 r6}c2 doesn't meet {1 6}, then {r7 r9}c2= {1 6}
if {r7 r9}c2= {1 6}, then r8{c1 c3} doesn't meet {1 6}
if r8{c1 c3} doesn't meet {1 6}, then r8{c4 c5} = {1 6}
…
if r2{c5 c6} doesn't meet {2 7}, then r2{c1 c3} = {2 7}

Conclusion: if either r1c2≠7 or r3c2≠2, then r1c1=2 and r2c3=7. In any case r1c3≠7 and r3c1≠2.
Similar eliminations can be done by circularity.

Looks like an xy-chain on subsets of cells and values.

[ravel]

In order to find my peace in sudoku heaven, let me update my last post.
Nice find, Steve K, and thanks for the hint, but i will never understand this notation.

So how to explain the eliminations in a different way ?

Code: Select all

 *-----------------------------------------------------------------------------*
 | 1       478     34578   | 3567    3689    5678    | 3489    369     2       |
 | 238     9       378     | 4       12368   12678   | 138     5       368     |
 | 23458   248     6       | 1235    12389   1258    | 7       139     3489    |
 |-------------------------+-------------------------+-------------------------|
 | 2468    5       1478    | 9       1246    3       | 128     1267    678     |
 | 234689  12468   13489   | 126     7       1246    | 123589  12369   35689   |
 | 2369    1267    1379    | 8       5       126     | 1239    4       3679    |
 |-------------------------+-------------------------+-------------------------|
 | 7       148     14589   | 1235    12348   12458   | 6       239     3459    |
 | 456     3       145     | 12567   1246    9       | 245     8       457     |
 | 45689   468     2       | 3567    3468    45678   | 3459    379     1       |
 *-----------------------------------------------------------------------------*



This is the chain to spot, where r13c2=27 means, the 2 cells r1c2 and r3c2 must have the values 2 and 7:
r13c2=27 => r2c13=38 => r2c79=16 => r13c8=39 => r79c8=27 => r8c79=45 => r8c13=16 => r79c2=48 => r13c3=27

Because it is closed, we have the following equivalences:
1. r13c2=27 <=> r2c13=38 <=> r2c79=16 <=> r13c8=39 <=> r79c8=27 <=> r8c79=45 <=> r8c13=16 <=> r79c2=48 <=> r13c2=27
2. r13c2=48 <=> r2c13=27 <=> r2c79=38 <=> r13c8=16 <=> r79c8=39 <=> r8c79=27 <=> r8c13=45 <=> r79c2=16 <=> r13c2=48

If both are false, none of these settings can be true (r2c13<>38 meaning, that at least one of the cells must get another number).

Where can 2 and 7 be in box 1 then ? Since one of them must be in r13c2 (which is not 48) and the other in r2c13 (<>38),
they are restricted to these 4 cells. The same holds for the other cases above, so r13c13<>27 (r1c3<>7, r3c1<>2)

Then one of 48 is in r13c2 and the other in r79c2 (<>16) => r456c2<>48 (r5c2<>48)
One of 16 must be in r79c2(<>48), the other in r8c13(<>45) => r79c13<>16 (r7c3<>1, r9c1<>6)
45 must be in r8c13, r8c79 => r8c456<>45 (r8c4<>5, r8c5<>4)
27 must be in r79c8, r8c79 => r79c79<>29
39 must be in r79c8, r13c8 => r456c8<>39 (r5c8<>39)
16 must be in r13c8, r2c79 => r13c79<>16
38 must be in r2c79, r2c13 => r2c456<>38 (r2c5<>38, r2c6<>8)

Note, that this way r456c28 and r28c456 can have arbitrary candidates.

---
OT: This is my last post. 999 is a nice age to die. Many thanks to all, who taught me so much, gave me a lot of fun and inspiraton and free programs.
To a couple of you i feel friends. Hope, this forum will keep the good spirit forever.

[denis_berthier]

Steve,
Currently not much time for Sudoku. But after reading Ravel's proof, I realise mine was incomplete.
And I also think yours is not correct. Your vocabulary of cell equivalents and compresion is misleading and your notation is ambiguous.

(2=7)r13c2=(2&7)r56c2 (this is a typical cell equivalent type argument, and makes the finding of such chains much easier.)
It is known that amongst the 4 cells, r1356, there exists one permutation of candidates 2,7 per possible solution. One can then partition that cell equivalent snippet as one sees fit.

Unless you say how such a partition is used, this is meaningless.
Your "cell equivalent argument", never defined, but exemplified by your proof, seems incorrect.

This is precisely analagous to the partitioning of a cell when using, for example, t-chains.

I don't think so. In t-chains, the xy-linking candidates must satisfy precise conditions and the additional t-candidates can only be among the previous right linking candidates; there is no arbitrary partitioning. But, from what you are saying, it seems you can choose arbitrary partitions.

Ravel's proof using two chains is correct, I think yours was not. Or is there anything we are missing?

Anyway, that is a nice "chain", even though we still don't see what general pattern you are invoking for the eliminations.

[denis_berthier]

gsf
Steve's eliminations easily lead to asserting r5c6 = 4.
Does this extra entry change the Singles backdoor level of Easter Monster?
Do his eliminations (which are not a mere consequence of this extra value) change it?

[gsf]

Steve's eliminations easily lead to asserting r5c6 = 4.
Does this extra entry change the Singles backdoor level of Easter Monster?
Do his eliminations (which are not a mere consequence of this extra value) change it?

[56]=4 does not change the singles backdoor size (still 3)
but it does increase the number of singles backdoors of size 3 from 566 to 996
all of the eliminations [13]^7 [31]^2 [73]^1 [91]^6 [52][85][58][25]={126} [62][84][48][26]={1267}
result in 2 singles backdoors of size 2 (they are [14]=3[84]=2 [38]=3[84]=2)

[denis_berthier]

gsf,
Thanks.
Do you have any means of computing the backdoors for nrczt (or anything approaching them)?

[gsf]

gsf,
Thanks.
Do you have any means of computing the backdoors for nrczt (or anything approaching them)?

with methods up to and including X/Y cycles enabled and starting with Steve K's eliminations
the puzzle reaches this state

Code: Select all

  1   478 3458 |3567  389 5678 |3489  369   2
 238   9   378 |  4   126 1267 | 138   5   368
3458  248   6  |1235  389 1258 |  7   139 3489
---------------+---------------+---------------
2468   5  1478 |  9   126   3  | 128 1267  678
 389  126  389 | 126   7    4  |3589  126 3589
2369 1267 1379 |  8    5   126 |1239   4  3679
---------------+---------------+---------------
  7   148 4589 |1235  348 1258 |  6   239 3459
 456   3   145 |1267  126   9  | 245   8   457
4589  468   2  |3567  348 5678 |3459  379   1


generated by this command line for my solver

Code: Select all

-f%#ph -q-KO -E em.dat [56]=4 [13]^7 [31]^2 [73]^1 [91]^6 [52][85][58][25]={126} [62][84][48][26]={1267}

-q-KO turns off the { y-knot template-rookery } methods (the ones not suitable for human solutions)
-E stops the solver at the point where G (backtrack guessing) would kick in
to list the backdoor stats run the pm grid above with

Code: Select all

-f'# %#bM %#aM %M # %#Am' -q-KO -Fe=

to get

Code: Select all

# 1 7 7 # [13]=4 [43]=1 [52]=2 [62]=6 [84]=2 [92]=4 [96]=6

XY backdoor size 1 involving 7 cells, 7 backdoors total

enabling KO doesn't help much -- it results in 22 size 1 backdoors

although ugly, the command line syntax is versatile

[RW]

Because it is closed, we have the following equivalences:
1. r13c2=27 <=> r2c13=38 <=> r2c79=16 <=> r13c8=39 <=> r79c8=27 <=> r8c79=45 <=> r8c13=16 <=> r79c2=48 <=> r13c2=27
2. r13c2=48 <=> r2c13=27 <=> r2c79=38 <=> r13c8=16 <=> r79c8=39 <=> r8c79=27 <=> r8c13=45 <=> r79c2=16 <=> r13c2=48

If both are false, none of these settings can be true (r2c13<>38 meaning, that at least one of the cells must get another number).

It's also easy to show that both in fact are false:

Code: Select all

 *-----------------------------------------------------------------------------*
 | 1       478     34578   | 3567    3689    5678    | 3489    369     2       |
 | 238     9       378     | 4       12368   12678   | 138     5       368     |
 | 23458   248     6       | 1235    12389   1258    | 7       139     3489    |
 |-------------------------+-------------------------+-------------------------|
 | 2468    5       1478    | 9       1246    3       | 128     1267    678     |
 | 234689  12468   13489   | 126     7       1246    | 123589  12369   35689   |
 | 2369    1267    1379    | 8       5       126     | 1239    4       3679    |
 |-------------------------+-------------------------+-------------------------|
 | 7       148     14589   | 1235    12348   12458   | 6       239     3459    |
 | 456     3       145     | 12567   1246    9       | 245     8       457     |
 | 45689   468     2       | 3567    3468    45678   | 3459    379     1       |
 *-----------------------------------------------------------------------------*

From the chains wee see that r13c2=27 => ... => r79c8=27
But we also have r13c2=27 => r2c56=27 and r79c8=27 => r8c45=27, which would force two 2s in column 5. Similarily for the other chain, we get two 2s in row 5.

I haven't found any new eliminations based on this, but it gives some more information about the implications in the grid, none of the pairs in ravels chains may be true, and the none of the cellpairs r2c56, r45c8, r56c2 and r8c45 may hold a 16 or 27 pair.

---
OT: This is my last post. 999 is a nice age to die. Many thanks to all, who taught me so much, gave me a lot of fun and inspiraton and free programs.
To a couple of you i feel friends. Hope, this forum will keep the good spirit forever.

Ravel!!?? What are you talking about?! You can't just retire, sudoku is meant to be highly addictive and keep you enslaved for the rest of you life! You might try to reject your desire for sudoku now, but it will come back to haunt you!! (insert the little devilish smiley here) Well, if you really mean it, thank you for everything you've done for the sudoku community! We're sure going to miss you and hope to see you back again some day. Perhaps when somebody once again reaches a new level of sudoku difficulty, you can't resist the urge to join in on the discussion...

RW

[ronk]

From the chains wee see that r13c2=27 => ... => r79c8=27
But we also have r13c2=27 => r2c56=27 and r79c8=27 => r8c45=27, which would force two 2s in column 5. Similarily for the other chain, we get two 2s in row 5.

I haven't found any new eliminations based on this, but it gives some more information about the implications in the grid, none of the pairs in ravels chains may be true, and the none of the cellpairs r2c56, r45c8, r56c2 and r8c45 may hold a 16 or 27 pair.

That's an interesting observaton, but I think a continuous loop can be found that doesn't depend on avoiding your digit 2 conflict in column 5.

[Steve K]

The logic compresses as follows:

Consider the following four sets:
1267 column 2, column 8, row 2, row 8.
Since the intersections of these sets: r2c2,r8c8,r2c8, r8c2 are already given, and not 1267, we have at least 16 truths total. (one could say exactly 16, if one wishes. One only needs at least 16 truths for the argument, however.)

In each box,(12346789) we have at most two truths. Specifically, in boxes 1,3,7,9 we are considering only two of the 4 candidates above, thus at most two truths in each of these. In boxes 2,4,6,8 we are considering only two cells, thus at most two truths in each of these. The only way, given 8 sets of max size 2, to get 16 truths is: we must have exactly two truths in each box at the applicable intersections.


The supercells are the box/column/row/cell intersections given above. The compression is trading at least/at most one for at least, at most two.

The total truths, 16, is merely a function of chain length. The reason it feels like a chain of length 8 is also clear - 16/2 is 8.

The chain, conceptually, is a chain of boxes (ok, pieces of boxes), made to look like cells.

If one adds, later, and independently, the conflict of 2s in row 5 ( or alternatively, column 5 - another piece of nice symmetry) yields a further relationship, namely for example that (2)r3c2-(7)r3c1. This of course is propagated thru out the grid. Thus, in each of boxes 2,4,6,8 the relationship at the two cells in question per box is exacly one of 2,7 plus exactly one of 1,6. I noted this in the "eureka" forum some time ago. Depending on where one starts the deduction, any one( or more,perhaps) of eight such relationships can be deduced, but any one forces the other 7.

Getting back to the original deduction, one could have compressed further, and built four "cell equivalents" that contains at least/ at most 4 truths each. However, the description of these "cell equivalents" is a bit more complex, and probably confuses the issue.

In a futile attempt to get AIC to look like it can handle this deduction, I tried to write the chain as if it is AIC. This was an unfortunate decision on my part. Sorry about the confusion it has caused. Strictly speaking, to write the deduction as pure AIC, one probably needs two simulataneous chains. The logic is not anywhere near that complex, as noted above (I hope it is clear!).

[denis_berthier]

ON THE NOTION OF A STRONG T-BACKDOOR

The classical notion of a (singles) backdoor can be extended in two directions.

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

The usual notion of a backdoor is obtained with T ={the rules for Singles (Naked or Hidden)}
It is known that EasterMonster has Singles-backdoor size 3.


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

Let NRCZT = T0 + {the nrczt rules}.

It can be shown that EasterMonster has (at least) the following NRCZT-backdoors of size 1: {r6c2=6} et {r9c6=6}.
(I haven't checked if there are any others).
Moreover EasterMonster cannot be solved in NRCZT.
Therefore EasterMonster has NRCZT-backdoor size 1.



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

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

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


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

gsf, I remember you once evoked the idea that backdoors might lead to a solution method. Did you have anything like this in mind?


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

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

As a result, using known backdoors for focusing the search for a solution may not always be a good idea.
(Using extra information on a puzzle is always debatable, but in the present case it may also be useless).

[Steve K]

Denis - this is perhaps not topical, perhaps a tad.
The next eliminations on the Easter Monster that I can maually identify, and their associated native depth, derived depth:
(1)r6c7 native 33, derived 7
(2)r2c5 native 34, derived 13
(16)r2c6 native 9, derived 1
(2)r4c7 native 2, derived 2
(6)r6c9 native 4, derived 4

Depth meaning cell or semi-cell equivalents considered.

I shall eventually tackle the entire animal in my blog, I think.

[gsf]

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

gsf, I remember you once evoked the idea that backdoors might lead to a solution method. Did you have anything like this in mind?

what I had in mind was
supose the singles backdoor size is known a-priori
could that information help prune the search for a solution for a T-unconstrainted puzzle?
some chain methods propagate singles
the singles backdoor size may somehow characterize "the best" chains

since almost all puzzles have singles backdoor size <= 2 any insight could be useful

for example, for all singles backdoor size 1 puzzles, there is at least one proposition that
will lead a cascade of singles to the solution
what are the properties of a cascade of singles?
knowing that might help identify fruitful candidates in the pm grid

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

with all constraints enabled for the P method in my solver the easter monster yields no
contradictions for singleton propositions -- only pairwise propositions yield contradictions
what are the NRCZT singleton contradictions for the easter monster?

As a result, using known backdoors for focusing the search for a solution may not always be a good idea.

starting a solution with the backdoors in hand would not be interesting
its knowing that a backdoor exists, not the explicit backdoors themselves, that should help guide the search

[denis_berthier]

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.
My goal was having a strong definition that'd imply the backdoor is directly useful for focusing the search.
The analysis of EM shows that "T-backdoor" doesn't entail "strong T-backdoor" (this maybe be intuitively obvious but we had no example).
The conclusion, and I think we agree on this, is that knowing the T-backdoors is of no direct help for guiding the search. What'd be useful for this is strong T-backdoors - but, as you say, they may be rare. We can still try to devise other indirect ways of using information on backdoors.

with all constraints enabled for the P method in my solver the easter monster yields no contradictions for singleton propositions -- only pairwise propositions yield contradictions
what are the NRCZT singleton contradictions for the easter monster?

Each of the following additional candidates separately leads to an NRCZT contradiction, i.e. each of these contradictions can be independently proven within NRCZT (I guess this is what you mean by "NRCZT singleton contradictions"):
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 EM in NRCZT12 (*). (I haven't tried with other subsets, so this may not be the smallest).
This entails that EM can be solved in NRCZT plus "depth one Trial-and-Error(NRCZT)" - as defined in my previous post.


(*) The proof is relatively short, although not easy (an nrczt chain or lasso of length 12 is very exceptional; OK, I've given one of length 25 in the "fully super-symmetric chains" thread, but this doesn't make those of length 12 less exceptional):
naked-single ==> r4c8 = 7
hidden-single-in-a-row ==> r9c4 = 7
hidden-single-in-a-row ==> r8c9 = 7
nrc2-chain n6{r1c8 r2c9} - n6{r4c9 r4c5} ==> r1c5 <> 6
nrczt3-chain n1{r7c2 r5c2} - n1{r5c8 r3c8} - n1{r3c4 r8c4} ==> r7c5 <> 1
nrczt3-chain n2{r7c8 r5c8} - n2{r5c2 r3c2} - n2{r3c4 r8c4} ==> r7c5 <> 2
nrczt3-chain n1{r7c2 r5c2} - n1{r5c8 r3c8} - n1{r3c4 r8c4} ==> r7c6 <> 1
nrczt3-chain n2{r7c8 r5c8} - n2{r5c2 r3c2} - n2{r3c4 r8c4} ==> r7c6 <> 2
nrczt6-chain n6{r4c5 r4c9} - n6{r2c9 r2c6} - n7{r2c6 r1c6} - n7{r1c2 r6c2} - n6{r6c2 r6c1} - n6{r8c1 r8c4} ==> r9c5 <> 6
nrczt6-lr-lasso n4{r7c9 r3c9} - n4{r1c7 r1c3} - n5{r1c3 r3c1} - {n5 n6}r8c1 - {n6 n8}r9c2 - n8{r1c2 r3c2} ==> r7c2 <> 4
nrczt11-lr-lasso {n6 n8}r4c9 - {n8 n3}r2c9 - {n3 n2}r2c1 - {n2 n4}r4c1 - {n4 n1}r4c3 - {n1 n2}r4c7 - {n2 n6}r4c5 - n6{r2c5 r2c6} - n6{r1c4 r8c4} - n2{r8c4 r8c5} - n1{r8c5 r8c3} ==> r5c9 <> 6
nrczt12-chain {n6 n8}r4c9 - {n8 n3}r2c9 - {n3 n2}r2c1 - {n2 n4}r4c1 - {n4 n1}r4c3 - {n1 n2}r4c7 - n2{r6c7 r6c6} - {n2 n6}r4c5 - {n6 n1}r5c4 - n1{r5c8 r3c8} - n1{r3c6 r2c6} - n6{r2c6 r2c9} ==> r6c9 <> 6
nrczt12-lr-lasso n6{r1c8 r5c8} - n6{r4c9 r4c5} - n6{r8c5 r8c1} - n6{r9c2 r6c2} - n7{r6c2 r1c2} - n7{r1c6 r2c6} - {n7 n3}r2c3 - {n3 n2}r2c1 - n2{r3c2 r5c2} - {n2 n1}r5c4 - n1{r6c6 r3c6} - n1{r3c8 r5c8} ==> r1c4 <> 6
nrct8-chain n2{r5c2 r3c2} - {n2 n3}r2c1 - {n3 n7}r2c3 - n7{r1c2 r1c6} - n6{r1c6 r1c8} - {n6 n8}r2c9 - {n8 n1}r2c7 - n1{r3c8 r5c8} ==> r5c8 <> 2
hidden-single-in-a-column ==> r7c8 = 2
nrct3-chain n6{r5c4 r8c4} - n2{r8c4 r8c5} - n1{r8c5 r7c4} ==> r5c4 <> 1
nrct4-chain n6{r5c4 r8c4} - n2{r8c4 r8c5} - n1{r8c5 r7c4} - n1{r7c2 r5c2} ==> r5c2 <> 6
hxyzt-cn5-chain {r8 r5}c4n6 - {r5 r3}c4n2 - {r3 r5}c2n2 - {r5 r7}c2n1 - {r7 r8}c4n1 ==> r8c4 <> 5
nrc6-chain n7{r1c6 r2c6} - {n7 n3}r2c3 - {n3 n2}r2c1 - n2{r3c2 r5c2} - {n2 n6}r5c4 - n6{r5c8 r1c8} ==> r1c6 <> 6
hidden singles ==> r1c8 = 6, r4c9 = 6
nrct5-chain n2{r5c2 r3c2} - {n2 n3}r2c1 - {n3 n8}r2c9 - {n8 n1}r2c7 - n1{r3c8 r5c8} ==> r5c2 <> 1
hidden-single-in-a-column ==> r7c2 = 1
naked-pairs-in-a-row {n4 n5}r8{c3 c7} ==> r8c5 <> 4, r8c1 <> 5, r8c1 <> 4
naked and hidden singles ==> r8c1 = 6, r6c2 = 6, r6c3 = 7, r2c3 = 3, r2c1 = 2, r2c9 = 8, r2c7 = 1, r2c5 = 6, r2c6 = 7, r1c2 = 7, r5c8 = 1, r4c3 = 1, r6c6 = 1, r6c7 = 2, r4c7 = 8, r4c1 = 4, r4c5 = 2, r5c4 = 6, r5c6 = 4, r8c5 = 1, r8c4 = 2, r3c6 = 2, r3c4 = 1, r3c1 = 5, r9c6 = 6, r9c7 = 5, r8c7 = 4, r8c3 = 5, r3c9 = 4, r3c2 = 8, r1c3 = 4, r5c2 = 2, r9c2 = 4, r7c5 = 4, r5c9 = 5
x-wing-in-rows n3{r3 r9}{c5 c8} ==> r1c5 <> 3
nrc2-chain n9{r7c3 r5c3} - n9{r6c1 r6c9} ==> r7c9 <> 9
…(naked singles)…
174385962
293467158
586192734
451923876
928674315
367851249
719548623
635219487
842736591