_m_k wrote:Leon1789:

Will you please explain the following? It sounds interesting and I like to learn in detail.

10 contradiction nets using singles and locked sets in 0-level recursion

f7#1, b7#8, c6#1, c5#8, f3#1, c9#3, a4#3, h7#4, k7#5, a8#3, finished

C#z means C=z is a disproved move by a contradiction net using singles, triples, quads... so -zC is proved.

- Code: Select all
`123456789`

+----------

A |1.......2

B |.3..4..5.

C |..6...7..

D |...1.3...

E |.8..7..4.

F |...4.6...

G |..2...6..

H |.5..3..8.

K |9.......1

Starting point : try f7=1 and find a quick contradiction (using singles, triples, quads). So f7#1 definitively.

Now, try b7=8 and find a contradiction. So b7#8 definitively.

And so on... c6#1, c5#8, f3#1, c9#3, a4#3, h7#4, k7#5, a8#3, and finish (using singles, triples, quads).

At the end, a unique solution is find and proved , and there are no recusion, but only 10 iterative steps :

- Code: Select all
`if f7=1`

then contradiction

therefore f7#1

if b7=8

then contradiction

therefore b7#8

if c6=1

then contradiction

therefore c6#1

...

if a8=3

then contradiction

therefore a8#3

finally a singles,triples,quads application leads to a solution

The "2 backdoor guess" does not prove the uniqueness of the solution : for me, it's a big difference between a simple guessing (no proof) and a dynamic forcing chain (valid proof).

I will post solutions for the five puzzles, but they are a little bit hard. Here, 1-level recursion is obligatory.