sag wrote:- Code: Select all
`1. Consider the chain r4c5-3-r6c5-3-r6c2-6-r4c3-6-r4c7.`

When the cell r4c7 contains the value 3, some other value must occupy the cell r4c5, which means that the value 6 must occupy the cell r4c7 - a contradiction.

Therefore, the cell r4c7 cannot contain the value 3.

- The move r4c7:=3 has been eliminated.

I don't understand your explanation, but now that you have pointed it out I can see that you are correct in my own way.

The notation describes the following implication chain:

r4c5<>3 => r6c5=3 => r6c2=6 => r4c3<>6 => r4c7=6

So, when r4c7 contains the value 3, r4c5 doesn't (because the cells are in Row 4) whereupon the chain tells us that r4c7 must contain a 6, which contradicts the original assertion.

- Code: Select all
`Consider the chain r5c1-8-r4c1-3-r6c2-6-r8c2-4-r8c1.`

When the cell r5c1 contains the value 4, so does the cell r8c1 - a contradiction.

Therefore, the cell r5c1 cannot contain the value 4.

The implication chain here is:

r5c1<>8 => r4c1=8 => r6c2=3 => r8c2=6 => r8c1=4

So r5c1=4 => r8c1=4, the necessary contradiction.

em wrote:r5c1=4 => r8c1=9

This is undoubtedly true but it doesn't allow us to make an inference because, as the logic books tells us, it's possible to prove anything from a false statement. (Of course, at this stage we don't know for sure that the statement is false, but we have no reason to suppose that it is true). The solver is able to make an inference from the initial assumption that r5c1=4 because it goes on to derive a statement that blatantly contradicts that assumption. Since the statement r5c1=4 is false, it will be possible to draw many different contradictory inferences from it.

em wrote:r5c1=8 => r5c7=3 => r5c2=4 => r8c1=4

Again, this is true. Your assertion r5c1=8 => r8c1=4 could be combined with my assertion r5c1<>8 => r8c1=4 to prove that r8c1=4. (It does, check the solution). However, my Forcing Chains logic misses this argument because your assertion can't be derived just from a true Forcing Chain, where it's only possible to infer a statement from its immediate predecessor in the chain.