I'm using a simple example (the one asked about) to demonstrate some forcing chain contradictions (Nishios) and verities (Krakens) and how they map into each other, AICs (Alternating Inference Chains) and DNLs (Discontinuous Nice Loops). Most of it has little relevance to experienced players, I presume, as I'm presenting the concepts with the least useful dual forcing chains. In the end I'll also talk a bit about the more practical (triple and quad) Kraken variants and their AIC equivalents, however.

Let's get to the case study. The puzzle is http://forum.enjoysudoku.com/november-11-2017-t34268.html

- Code: Select all
`+--------------+------------------+--------------------+`

| 26 8 7 | b2(9) 3 4 | 1 569 d'56(9) |

| 1 26 3 | 5 29 7 | 68 689 4 |

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

+--------------+------------------+--------------------+

| 3 7 1 | 4 b'258 6 | 58 589 c'259 |

| 4 9 68 | A8-2 1258 3 | 5678 15678 1256 |

| 25 25 68 | 7 18 9 | 4 3 16 |

+--------------+------------------+--------------------+

| 67 1 9 | 3 4 5 | 2 67 8 |

| 8 35 4 | 6 7 2 | 9 15 135 |

| 567 356 2 | 89 89 1 | 567 4 356 |

+--------------+------------------+--------------------+

1. Forcing Chain Contradictions (Nishios) vs. Verities (Krakens)

The original logic presented to me was like this:

"2r5c4 => 9r1c4, but also 2r5c4 => 2r4c9 => 9r4c8 => 9r1c9, resulting in two 9s in Row1, so r5c4<>2 => r5c4 = 8"

The same presented as a diagram (my "|" means OR, so to avoid confusion "=" and "-" are used in vertical relationships as well):

- Code: Select all
`(2)r5c4-|(2)r1c4===========(9)r1c4`

| -

|(2)r4c5=(2-9)r4c9=(9)r1c9

=> -2 r5c4

Some (like Hodoku) would call that a Forcing Chain Contradiction. Others might call it Nishio. Either way it means that you assume something to be true (or false) and see if it leads into a contradiction of some kind elsewhere. In this case the starting assumption is 2r5c4, which leads into a contradiction of two 9s in row 1 (c4 and c9). The contradiction arises because the two 9s are within the same Weak Inference Set (WIS) where there can be at most one. That proves the starting assumption wrong. Perhaps not very elegant, but it's a logical proof indeed. If we view its mirror image we get:

Kraken Row (9)r1:

- Code: Select all
`(9)r1c4===========(2)r1c4|-(2)r5c4`

- |

(9)r1c9=(9-2)r4c9=(2)r4c5|

That could be called a Forcing Chain Verity, or a Kraken Row (an unusual one, though, because of a WIS forming the starting hub, i.e. the initial assumptions are OFF). This proves that if any member of the WIS (9)r1 is false (and at least one must be) the target (2)r5c4 is eliminated -- thus it can be eliminated. A verity. Usually verities seem to be considered more elegant proofs than contradictions (less "assumptive", perhaps?), although there's no practical difference. Now, let's switch back to the contradiction point of view, but twist things a bit:

- Code: Select all
`(2)r5c4-|(2)r1c4=(9)r1c4-(9)r1c9`

| =

|(2)r4c5=(2)r4c9-(9)r4c9

We're using the same chain elements but with a different breaking point. That produces a different kind of contradiction. Now our last nodes of the two chains emanating from the initial assumption form a Strong Inference Set (SIS) in which at least one element must be true. Our assumption, however, would eliminate them both. Thus a different contradiction, but the same conclusion (-2 r5c4). A mirror image shows a more familiar kind of Kraken Column with a SIS as the starting hub:

Kraken Column (9)c9:

- Code: Select all
`(9)r1c9-(9)r1c4=(2)r1c4|-(2)r5c4`

= |

(9)r4c9-(2)r4c9=(2)r4c5|

That proves that if any member of the SIS (9)c9 is true, (2)r5c4 would get eliminated. Because one of those 9s must be true, we have a verity: thus -2 r5c4. We can twist those chain elements pretty much any way we like to get different contradictions or verities that all prove the same thing. For example:

- Code: Select all
`(2)r5c4-|-----------------------(2)r1c4`

| =

|(2)r4c5=(2-9)r4c9=r1c9-(9)r1c4

That contradiction variant empties the SIS cell r1c4 of all candidates (2 and 9). Its mirror image is a Kraken Cell (29)r1c4 (not shown). Or:

- Code: Select all
`(2)r5c4-|(2=9)r1c4-(9)r1c9=(9)r4c9-(2)r4c9`

| =

|--------------------------(2)r4c5

That contradiction eliminates all 2s in the SIS r4. Its mirror image is a Kraken Row (2)r4 (not shown). One twist is a bit different:

- Code: Select all
`(2)r5c4-|(2=9)r1c4-r1c9=(9)r4c9-(2)r4c9`

| +

|(2)r4c5================(2)r4c9

That contradiction arises because the initial assumption would turn the same candidate (2)r4c9 both ON and OFF. Its mirror image is a special kind of Kraken in which the hub is formed by the two possible states of a single candidate which together prove a verity (SudokuWiki would call it a Digit Forcing Chain).

2. Dual Forcing Chains vs. AICs and DNLs

Okay, that's enough for the simple contradictions and their verity counterparts. Usually we would not use any of those representations in this kind of a situation, because any dual forcing chain can be more simply expressed as an AIC (or a Discontinuous Nice Loop, if one wishes). Knowing those equivalences might help find the chains, however, and any of those forms is easily translated into an AIC or a DNL. Let's take the original Nishio contradiction, for example:

- Code: Select all
`(2)r5c4-|(2)r1c4===========(9)r1c4`

| -

|(2)r4c5=(2-9)r4c9=(9)r1c9

If we start a chain from the initial assumption and loop around (either way) in the diagram, we get one or the other:

(2)r5c4-(2)r1c4=(9)r1c4-(9)r1c9=(9-2)r4c9=(2)r4c5-(2)r5c4

(2)r5c4-(2)r4c5=(2-9)r4c9=(9)r1c9-(9)r1c4=(2)r1c4-(2)r5c4

The same in compacted form:

DNL: (2)r5c4-(2=9)r1c4-r1c9=(9-2)r4c9=r4c5-(2)r5c4 => -2 r5c4

DNL: (2)r5c4-r4c5=(2-9)r4c9=r1c9-(9=2)r1c4-(2)r5c4 => -2 r5c4

Those are equivalent Discontinuous Nice Loops directly proving the initial assumption as wrong.

The AICs (preferable) are even simpler to get, as we can leave the initial assumption (or the Kraken conclusion) out. We even get an added elimination that way:

AIC: (2=9)r1c4-r1c9=(9-2)r4c9=(2)r4c5 => -2 r5c4, r2c5

AIC: (2)r4c5=(2-9)r4c9=r1c9-(9=2)r1c4 => -2 r5c4, r2c5

Extracting the AIC is even easier from a dual Kraken:

- Code: Select all
`(9)r1c9-(9)r1c4=(2)r1c4|-(2)r5c4`

= |

(9)r4c9-(2)r4c9=(2)r4c5|

First, cut out the conclusion part (if present):

- Code: Select all
`(9)r1c9-(9)r1c4=(2)r1c4`

=

(9)r4c9-(2)r4c9=(2)r4c5

Then straighten the chain by "pulling" the lower part to the right:

(2)r1c4=(9)r1c4-(9)r1c9=(9)r4c9-(2)r4c9=(2)r4c5

Compacted (but white space added):

AIC: (2=9)r1c4 - r1c9 = (9-2)r4c9 = (2)r4c5 => -2 r5c4, r2c5

One last thing about that example. The same chaining elements can be used for a very different looking AIC (Leren's solution, in fact):

AIC: (9)r1c9 = (9-2)r4c9 = r4c5 - r5c4 = (2)r1c4 => -9 r1c4

Let's turn that into a forcing chain (just to prove a point). If we can turn a forcing chain into an AIC, we can definitely reverse that process too. If we use 9r1c4 as an initial assumption for a Nishio it should produce a contradiction, which could be turned into a Kraken. Of course we don't really want to do that because the AIC is already the preferred form, but let's just see one possibility:

- Code: Select all
`(9)r1c4-|--------------------------(2)r1c4`

| =

|(9)r1c9=(9-2)r4c9=(2)r4c5-(2)r5c4

The assumption of (9)r1c4 would remove all 2s from c4, which is a contradiction; thus -9 r1c4. Its mirror image would be the Kraken Column (2)c4. Of course we could produce other contradictions and verities as well by cutting the chain at different locations, just like before, but I'll leave that as an exercise to the reader.

Our two different-looking AICs actually produce the same end result, which is easily demonstrated if we combine them into a DNL (Type 2):

DNL: (2=9)r1c4 - r1c9 = (9-2)r4c9 = r4c5 - r5c4 = (2)r1c4 => 2r1c4

So, the point of that lengthy demonstration was to show the equivalence between Forcing Chain Contradictions (Nishios) and Verities (Krakens), as well as their dual variants' equivalence to AICs and DNLs. Whenever a forcing chain (either kind) has just two branches, it can be easily translated into an AIC or a DNL (and vice versa). Similarly the two kinds of forcing chains can be translated into each other. When applicable, AICs should be used in practice. DNLs may be easier to understand for a beginner, but AICs are more concise, generic and powerful. Forcing Chains should be reserved for more complex situations (see next).

3. Triple and Quad Krakens vs Nested AICs

The dual Nishios and Krakens above were for concept demonstration purposes only, as they could and should be presented as AICs instead. The actually useful Forcing Chain variants have more than two branches, and they can't be translated into AICs as easily. In fact, they are usually more clearly presented as Krakens.

Let's look at some SudokuWiki examples. Its Triple/Quad Cell Forcing Chains and Unit Forcing Chains are what we call Krakens, and they're also the only relevant forcing chains on that site. Its Nishios, Digit Forcing Chains, and Dual Cell/Unit Forcing Chains are unnecessary, except conceptually, as they can all be turned into simple AICs. (It's a good exercise for beginners, by the way, to go over those examples and do just that.)

The first useful example is the second Triple Cell Forcing Chain (the first triple can more easily be solved with other techniques):

http://www.sudokuwiki.org/Cell_Forcing_Chains

- Code: Select all
`+--------------------+-------------------+--------------+`

|d''17 389 2 | 348 3489 6 | 5 89 17 |

| 4 5689 x69-7 | 158 5789 578 | b17 2 3 |

| 157 3589 d''179 | 1358 35789 2 | 4 89 6 |

+--------------------+-------------------+--------------+

| 9 7 8 | 45 6 45 | 3 1 2 |

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

| 2 4 5 | 38 1 38 | 6 7 9 |

+--------------------+-------------------+--------------+

| 8 56 c'167 | 9 3457 13457 | 2 36 17 |

| 3 2 c'c''179 | 6 78 178 |b''179 5 4 |

| b'157 569 4 | 2 357 1357 | A179 36 8 |

+--------------------+-------------------+--------------+

Triple Kraken Cell (179)r9c7:

- Code: Select all
`(1)r9c7-(1=7)r2c7----------------|-(7)r2c3`

= |

'(7)r9c7-r9c1=(7)r78c3------------|

= |

''(9)r9c7-r8c7=r8c3-(9=17)r3c3,r1c1|

=> -7 r2c3

That's a forcing chain verity, proving that all candidates in cell (179)r9c7 would eliminate 7r2c3 -- thus it can be eliminated. The mirror image would be a Nishio contradiction proving that an assumption of 7r2c3 would empty the cell r9c7. How about viewing it as an AIC? Not so trivial anymore as we have more than two branches (our starting hub SIS > 2). It can be done either as a net (branching AIC) or a nested AIC. The latter is easier to produce from the diagram, as we can use almost the same process as with the simpler examples above.

If we think about it, what we have here is an almost-AIC: either we have 3r4c1 (the top branch) OR we have an AIC formed by the two lower branches. Together they produce the three endpoints needed for replicating the Kraken logic. That can be written as a nested AIC (endpoints marked with #):

AIC (ANS, Grouped, Nested): (#7=1)r2c7-r9c7=AIC:[(#7)r78c3=r9c1-(7=9)r9c1-r8c7=r8c3-(9=1#7)r3c3,r1c1] => -7r3c3

That was easy. With the quad example things get a bit hairy:

- Code: Select all
`+-------------------+---------------+----------------+`

| 1234 *12 8 | 9 236 7 | 2346 5 *2346 |

| 2359 7 235 | 238 4 268 | 236 1 89 |

| 2349 6 234 | 5 238 1 | 234 89 7 |

+-------------------+---------------+----------------+

| 6 3 A(1245) | 78 1258 258 | 9 47 *12 |

|*14 *125 *9 | 37 1236 25 | 8 47 16 |

| 128 x28-1 7 | 4 169 269 | 126 3 5 |

+-------------------+---------------+----------------+

| 7 89 15 | 6 589 3 | 145 2 1489 |

| 12358 4 1235 | 28 7 589 | 135 6 1389 |

| 2358 2589 6 | 1 258 4 | 7 89 38 |

+-------------------+---------------+----------------+

Quad Kraken Cell (1245)r4c3:

- Code: Select all
`(1)r4c3--------------------|-(1)r6c2`

= |

(2)r4c3-r4c9=r1c9-(2=1)r1c2|

= |

(4)r4c3-(4=1)r5c1----------|

= |

(5)r4c3-(5=21)r51c2--------|

=> -1 r6c2

Since a quad Kraken is an almost-almost-AIC, it requires a second nesting:

AIC (ANS, Nested): (#1)r4c3=AIC:[(#1=2)r1c2-r1c9=r4c9-r4c3=AIC:[(#1=4)r5c1-(4=5)r4c3-(5=2#1)r51c2]] => -1r6c2

For the sake of completion, let's translate the Unit Forcing Chain examples as well (though they're both solvable with simpler techniques):

http://www.sudokuwiki.org/Unit_Forcing_Chains

Triple Kraken Row (2)r1:

- Code: Select all
`(2)r1c2-----------------------|-(2)r6c2`

= |

(2)r1c3-r8c3=(2)r8c2 |

= |

(2)r1c5-(2=3)r2c6-r6c6=(3)r6c2|

=> -2 r6c2

AIC (Nested): (#2)r1c2=AIC:[(#2)r8c2=r8c3-r2c3=r1c5-(2=3)r2c6-r6c6=(#3)r6c2] => -2 r6c2

Quad Kraken Column (8)c3:

- Code: Select all
`(8)r2c3-r2c9=(8)r3c9-----------------|-(8)r3c5`

= |

(8)r3c3------------------------------|

= |

(8)r7c3-r7c4=(8)r1c4-----------------|

= |

(8-4)r8c3=r9c3-(4=6)r9c6-r3c6=(6)r3c5|

=> - 8 r3c5

AIC (Nested): (#8)r3c3=AIC:[(#8)r3c9=r2c9-r2c3=AIC:[(#8)r1c4=r7c4-r7c3=(8-4)r8c3=r9c3-(4=6)r9c6-r3c6=(#6)r3c5]] => -8 r3c5

I'm not advocating the use of the nested-AIC style, as recursion is always a bit unintuitive. Just stating that it's logically possible if compactness is needed. (Or so I think... I haven't really seen this style in practice, so perhaps I'm mistaken.) I think they're also valid AICs, unlike their net counterparts.

Comments, corrections, suggestions, additions, criticism etc are all welcome. Personally I'd be interested in tips on spotting useful triple and quad Krakens manually. So far I've found them mostly by finding a Nishio contradiction first and then reversing it.