The New Sudoku Players' Forum

[David P Bird]

Blue, I see that you're Sudoku active here but are paddling at the shallow end of the pool! Here's something that's more appropriate to your talents.

As we know, the Avoidable Rectangle theorem proves that lacking any givens, 4 cells in 2 boxes that form a rectangle must hold at least 3 different digits.

My conjecture is that a digit placement arising from only elementary eliminations (naked and hidden singles and tuples, box/line reductions and simple fish) can never produce an AR threat.

Code: Select all

  12  .  .  | 24 .  .
  .   .  .  | .  .  .
  23  .  .  | 1  .  .

This shows a possible scenario where it has been possible to place (1)r3c4 to produce an AR strong inference (4)r1c4 = (3)r3c1. From practical experience either (1)r1c1 will never occur as a candidate or one of the cells will hold a given. I therefore think that looking for ARs immediately after making preliminary eliminations is fruitless.

I believe that to produce such a situation some more advanced elimination method must have been used beforehand. Your mission, if you choose to accept it, is to prove whether that is true or not.

DPB

[blue]

My conjecture is that a digit placement arising from only elementary eliminations (naked and hidden singles and tuples, box/line reductions and simple fish) can never produce an AR threat.

[...]

I believe that to produce such a situation some more advanced elimination method must have been used beforehand. Your mission, if you choose to accept it, is to prove whether that is true or not.

Hi David,

It's a nice challenge.
Your conjecture is correct.
It follows, after a bit of argument, from this ...

Given a scenario where these 8 candidates exist:

Code: Select all

+---------+--------+-------+
| 12  . . | 12 . . | . . . |
| .   . . | .  . . | . . . |
| 12  . . | 12 . . | . . . |
+---------+--------+-------+


Statement (1): It is impossible for 1r1c1 to be eliminated using those techniques, without one of { 2r1c1, 1r1c4, 1r3c1 } also being eliminated.

This will be proved below.

A more refined form of the statement, would be that if 1r1c1 has been eliminated using one of those techniques, then either one of { 2r1c1, 1r1c4, 1r3c1 } was also eliminated, or an elimination has been missed, and is still available.

-----

I think the most general form of the AR argument is this:

Given a scenario like this:

Code: Select all

+--------+--------+-------+
| 1A . . | 2B . . | . . . |        None of the 4 cells were givens
| .  . . | .  . . | . . . |        A, B, C are lists of candidates; empty lists are allowed
| 2C . . | 1  . . | . . . |        Somehow, 1r3c4 has been (properly) deduced.
+--------+--------+-------+


Statement (AR):Any solution to the puzzle, unique or not, must contain a candidate from one of { A, B, C }.

A review of the proof for "Statement (AR)": If the puzzle has no solutions, then the statement is true by default. On the other hand, if it had a solution with no candidate from any of { A, B, C }, then it would contain the values { 1r1c1, 2r1c4, 2r3c1, 1r3c4 }. Since none of the four cells were "givens", there would also be a second solution containing { 2r1c1, 1r1c4, 1r3c1, 2r3c4 } -- the standard UR claim. But since that solution contains 2r3c4, it would follow that 1r3c4 was not properly deduced. So if 1r3c4 has been properly deduced, then any solution must contain a candidate from one of { A, B, C }.

That statement can be generalized to apply to this scenario:

Code: Select all

+-----------+--------+-------+
| 1[2]A . . | 2B . . | . . . |        Same setup as above, where the 2r1c1 candidate is optional,
| .     . . | .  . . | . . . |        and not considered as being part of A
| 2C    . . | 1  . . | . . . |
+-----------+--------+-------+


... by noting that in the original "AR" statement, with A replaced by A u { 2r1c1 }: 1) if the solution doesn't contain a candidate from one of { B, C }, then it contains a candidate from the larger 'A'; 2) not containing anything from { B, C }, it would contain 2r1c4 and 2r3c1; and it could not contain 2r1c1; and so 3) since the only thing left, is a candidate from the smaller 'A', it would follow that it contains a candidate from the smaller 'A'. Summarizing, if it doesn't contain a candidate from one of { B, C }, then it contains one from the smaller 'A', and so all in all, it must contain a candidate from one of { (the smaller A), B, C }.

-----

To prove your conjecture, we can use "Statement (1)" to prove that using those techniques only, it is impossible to deduce that 1r3c4 is part of the solution (i.e. impossible to see it as a "single"), as long as candidates { 1r1c1, 2r1c4, 2r3c1 }, still exist. [ That is, assuming that when any of the techniques is used, all of the eliminations are taken. ]

In other words, this follows from Statement (1) ...

In an initial scenario where these candidates still exist:

Code: Select all

+--------+--------+-------+
| 12 . . | 12 . . | . . . |
| .  . . | .  . . | . . . |
| 12 . . | 12 . . | . . . |
+--------+--------+-------+


Statement (3): It will be impossible for 1r3c4 to be seen as a naked or hidden single, using the indicated techniques, until one of { 1r1c1, 2r1c4, 2r3c1 } is eliminated.

A more refined form of the statement, would be that if 1r3c4 can ever be seen as a single, then either one of { 1r1c1, 2r1c4, 2r3c1 } will have been eliminated, or an elimination for one of them, will have been missed, and would still exist.

-----

To prove Statement (3) using Statement (1):

1) There are 3 versions of Statement (1), that follow from the symmetry of the situation:

• It is impossible to eliminate 2r3c4, without also eliminating one of { 1r3c4, 2r1c4, 2r3c1 }
• It is impossible to eliminate 1r1c4, without also eliminating one of { 2r1c4, 1r1c1, 1r3c4 }
• It is impossible to eliminate 1r3c1, without also eliminating one of { 2r3c1, 1r1c1, 1r3c4 }

2) Taken together, they imply this:

• It is impossible to eliminate one of { 2r3c4, 1r1c4, 1r3c1 }, without also eliminating one of { 1r1c1, 2r1c4, 2r3c1, 1r3c4 }.

3) For 1r3c4 to be seen as a single, one of { 2r3c4, 1r1c4, 1r3c1 } must be eliminated:

• To be seen as a naked single in r3c4, 2r3c4 would need to be eliminated
• To be seen as a hidden single in r3, 1r3c1 would neeed to be eliminated.
• To be seen as a hidden single in b2 or c4, 1r1c4 would need to be eliminated.
• Those are the only options, and each involves one of { 2r3c4, 1r1c4, 1r3c1 } being eliminated.

4) With (3) and (2) together, it follows that 1r3c4 can't be seen as a single, unless one of { 1r1c1, 2r1c4, 2r3c1, 1r3c4 } has already been eliminated.

5) Since 1r3c4 itself, is "out", that leaves one of { 1r1c1, 2r1c4, 2r3c1 }, to have been eliminated, before 1r3c4 could be seen as a single (assuming all eliminations were taken, when any of the techniques were applied).

6) Summarizing:

• It will be impossible for 1r3c4 to be placed as a single, as long as the { 1r1c1, 2r1c4, 2r3c1 } candidates still exist.

A more refined statement, would be that if it was possible to place 1r3c4 as a single, then it would be possible to eliminate one of { 1r1c1, 2r1c4, 2r3c1 } as well, destroying the "AR threat".

-----

What remains is a detailed proof for Statement (1).

1) Suppose 1r1c1 is eliminated as a naked set (n-tuple) elimination:

• Then it's a naked set in r1, in c1, or in b1
• Whichever house it is (r1,c1 or b1), it will contain (just) one of the 1r1c4, 1r3c1 cells/candidates
• The (n-tuple) cell set won't include r1c1, since naked set eliminations occur outside the cell set, and we're assuming that 1r1c1 is eliminated.
• Whichever of { 1r1c4, 1r3c1 } is in the same house as the naked set, if we assuming that that candidate is not *also* eliminated, then it would follow that the (n-tuple) cell set must include that cell (since 1's in cells outside the set, are being eliminated).
• But that cell (r1c4 or r3c1) also contains the '2' candidate (at that time), and with that cell in the set, and r1c1 ourside the set, the 2r1c1 candiadte would also eliminated.
• Summarizing: If neither of { 1r1c4, 1r3c1 } is (also) eliminated, then 2r1c1 is eliminated.
  Hence: At least one of { 1r1c4, 1r3c1, 2r1c1 } would also be eliminated.

2) Suppose 1r1c1 is eliminated in a hidden set elimination.

• Then there's a naked set is present in the same house, that would cause the identical set of eliminations, and so from the argument above, one of { 1r1c4, 1r3c1, 2r1c1 } would also be eliminated.

3) Suppose 1r1c1 is eliminated in a basic fish elimination.

• Assume it's a row fish -- 'n' rows with the '1' candidates restricted to 'n' columns, with the 1's in those columns, but in other rows, being eliminated. The argument for a column fish, would follow from symmetry.
• If the 1r3c1 candidate is also eliminated, then that's fine ... it fits with the statement that one of { 1r1c4, 1r3c1, 2r1c1 } is also eliminated.
• Focusing on the situation where 1r3c1 is not (also) eliminated, then ...
• Since 1r3c1 is not eliminated, r3 must be in the row set for the fish.
• Since 1r1c1 is being eliminated, r1 cannot be in the row set.
• Finally, since the 1r3c4 candidate is also present at the time, and since r3 is in the row set, and r1 isn't in the row set, the 1r1c4 candidate would also be eliminated, and so again, one of { 1r1c4, 1r3c1, 2r1c1 } would also be eliminated.

4) Suppose 1r1c1 was eliminated in a line/box elimination. Cases that would cause that, and details for each, are listed below. In the cases that are relevant, one of { 1r1c4, 1r3c1 }, and hence one of { 1r1c4, 1r3c1, 2r1c1 }, is also eliminated.

• 1's in r2, are locked in b1 -- then 1r3c1 also would be eliminated
• 1's in r3, are locked in b1 -- impossible since 1r3c4 is still present
• 1's in c2, are locked in b1 -- then 1r3c1 also would be eliminated
• 1's in c3, are locked in b1 -- then 1r3c1 also would be eliminated
• 1's in b2 are locked in r1 -- impossible since 1r3c4 is still present
• 1's in b3 are locked in r1 -- then 1r1c4 also would be eliminated
• 1's in b4 are locked in c1 -- then 1r3c1 also would be eliminated
• 1's in b7 are locked in c1 -- then 1r3c1 also would be eliminated

5) Suppose 1r1c1 eliminated as a "same digit", line of sight elimination, after a '1' is placed in one of { r1, c1, b1 }.

• The '1' would need to be a naked or hidden single. It can't be a hidden single, though, since the { 1r1c4, 1r3c1 } candidates are still present. So, it could only be a naked single.
• That would mean that the single in a cell that is not one of { r1c4, r3c1 }, since those cells also contain the '2' candidate.
• With that, whichever of { r1c4, r3c1 } is in the same house as the single [ and one of them would be in the same house ], the corresponding candidate from { 1r1c4, 1r3c1 }, would also be eliminated.
• That fits with the statement that one of { 1r1c4, 1r3c1, 2r1c1 } is also eliminated.

6) The last option would be that 1r1c1 is eliminated since a digit other than '1' is being placed in r1c1, as as a hidden single.

• It can't be the '2', though, since 2r1c4 and 2r3c1 are still present.
• So it would be a digit other than '2' (being placed in r1c1), and the 2r1c1 candidate would also be eliminated.
• Again, that fits with the statement that one of { 1r1c4, 1r3c1, 2r1c1 } is also eliminated.

That completes the proof.

-----

Regards,
Blue.

[David P Bird]

Blue, thank you and well done!

When I pondered this question I asked myself how would you approach it, but I suspected that there would be some neat high level theorem involved rather than a fairly extensive analysis by cases. Your use of numbered statements presents the proof very well and is something that I'll try to learn from.

Code: Select all

12a . . | 12b . .
.   . . | .   . .
12c . . | 1d  . .

For this pattern it's been possible to eliminate (2) from r3c4. This proves that these cells aren't covered by a 4-cell (12)UA and so at least one of (abcd) must be true. Although there is only one way to solve the cells using (1) & (2), it must be wrong because then the (2) elimination wouldn't have been possible.

If we define member digits of the pattern as those in the possible covering UA, then the rule is that at least one cell must contain a non-member digit.

This then extends to larger Almost Deadly Patterns where one or more of the cells are missing individual member digits.

Code: Select all

12 . . | 23 . . | .  . .
21 . . | .  . . | 31 . .
.  . . | 32 . . | 13 . .

This shows a 6-cell UA with ordered pairs giving the two possible solutions. If one of the member candidates can be eliminated, then one of the cells must contain a non member candidate regardless of how many additional member candidates can also be eliminated.

Code: Select all

1  . . | 3x . . | .  . .
2  . . | .  . . | 3  . .
.  . . | 2  . . | 1x . .

Here's the same pattern after some eliminations where one of the (x)s must be true. Working backwards like this is easy to compose such a pattern but for a player to identify one is much harder. From your work it seems that the only time it's worth even trying is immediately after an advanced elimination has been made.

David

Other contributions to this discussion are now welcome.

[denis_berthier]

As we know, the Avoidable Rectangle theorem proves that lacking any givens, 4 cells in 2 boxes that form a rectangle must hold at least 3 different digits.
My conjecture is that a digit placement arising from only elementary eliminations (naked and hidden singles and tuples, box/line reductions and simple fish) can never produce an AR threat.

Blue, [...] I suspected that there would be some neat high level theorem involved rather than a fairly extensive analysis by cases.

I don't know exactly what you're aiming at, but this evokes an old question about UR1.1. Without entering into details, there are two complementary points:
- as long as a "theorem" relies on a difference between an axiom (a given C) and a proven consequence of this axiom (the value C found by proof), it cannot be the result of any formal proof (in the sense of mathematical logic);
- as long as the proof of a "theorem" requires the use of the classical not not A = A equivalence, it cannot be proven by applying repeatedly the rules of any resolution theory (because such a proof is done within constructive logic = intuitionnistic logic).

[David P Bird]

Denis, I can't say I understand that. Can you please say which step in this sequence is logically unsound?

1) In addition to the basic Sudoku constraints there is an additional design constraint is that for any Unavoidable Set to be resolvable, one of its cells must contain a given.
2) No assumption is made whether that constraint is met for every UA in the puzzle as that would assume uniqueness.
3) However some identifying elimination(s) reveal that a particular set of cells cannot contain a UA.
4) We can therefore use that knowledge to our advantage.

[denis_berthier]

Denis, I can't say I understand that. Can you please say which step in this sequence is logically unsound?

I wasn't referring to anything in particular, just mentioning two ideas that may be relevant to questions about rules based on UAs.
My second point was not about being unsound or not, it was about HOW something can be proven - either constructively or not.

[eleven]

Any new insights ???

RedEd, please can you formulate another trivial proof to make Denis a believer this time also ?

OK.

Definition: an a/b/b/a pattern in a solution grid is anything isomorphic to that shown below:

Code: Select all

 .  .  . | .
 a  .  . | b
 b  .  . | a
---------+---
 .  .  . | .

Fact: if a solution grid (not necessarily unique) contains an a/b/b/a pattern on four unclued cells, C, then C=b/a/a/b is also a solution.

Theorem: if a puzzle-in-progress (that does not necessarily have a unique solution) has pencilmarks as shown below on four unclued cells then the bottom right value resolves to '3':

Code: Select all

 .  .  . | .
 1  .  . | 2
 2  .  . | 13
---------+---
 .  .  . | .

Proof: suppose to the contrary the bottom right value resolves to '1'. Then (vacuously) the solution grid contains the 1/2/2/1 pattern on four unclued cells, C. So, by the Fact above, C=2/1/1/2 is also a solution. But wait! - the pencilmarks do not allow that other solution - contradiction.

Thanks, RedEd, for this very smart proof.

Before it, UR1.1 was only a conjecture, a matter of belief or disbelief. It is now a valid theorem (we'll see later under what implicit conditions). It shows that a short and clean proof can do what pages of repeated but unsustained claims can't.

[denis_berthier]

Thanks, eleven, for recalling us the old time.

You are just forgetting the sequel of that thread (announced by "we'll see later under what implicit conditions") where I showed that UR1.1 is valid in classical logic but not in intuitionnistic (or constructive) logic.
As all the questions about UAs and the ways they can be used in resolution rules revolve around HOW something is proven, this makes a fundamental difference.

This being said, I think there's no new argument and we'd better leave all this where it was years ago.

[eleven]

I really don't know, what you are out for (and as it seems, David doesn't either).
Do you mean, that your resolution rules must not use the UR1.1, because they cannot prove it's validity themselves ?

If so, i am not interested in this restriction they have. Because i don't have it, when i solve a puzzle. I do know, that it is proved.

[denis_berthier]

I really don't know, what you are out for (and as it seems, David doesn't either).

Let David speak for himself. I posted in this thread only because he asked me. As his question is "How do UAs arise?" and he suggested a set of rules that cannot lead to an AR, and as he later suggested that he was expecting something more general than Blue's proof, I mentioned that (using the two remarks in my first post here), the same is probably true for any set of resolution rules: no such set can lead to an AR. As I'm not really interested in all this, these were only suggestions for anyone willing to try a general proof along such lines.

Do you mean, that your resolution rules must not use the UR1.1, because they cannot prove it's validity themselves ?
If so, i am not interested in this restriction they have. Because i don't have it, when i solve a puzzle. I do know, that it is proved.

All my resolution rules are defined in a way totally independent of UR1.1 or uniqueness.
As in the case of uniqueness, I have programmed such rules in SudoRules (UR1.1 is very easy to program in my formalism), but I never activate them (personal choice).

It is not the purpose of a resolution rule or a set thereof to prove another rule.
What I said long ago is that UR1.1 cannot be proven (from the axioms of Sudoku) by constructive logic.
Accepting UR1.1 in your arsenal is a matter of personal choice, as in the uniqueness case, and I don't want to spend my time discussing personal tastes. As for me, I find it queer, in a constructive pattern-based resolution path, to use a rule that cannot itself be proven constructively.

It seems you deeply misunderstand my approach.
My goal is not to tell anyone what they should/may/must use. I don't care at all about this.
My goal is to study what can be done when one uses a well defined set of resolution rules - said otherwise to study the scope and limitations of each type of rules, together with the relationships between different families. But this is taking us very far from the topic of this thread.

BTW, David, I'm much more interested in an answer about JExocets than about UAs.

[eleven]

I posted in this thread only because he asked me. As his question is "How do UAs arise?" and he suggested a set of rules that cannot lead to an AR, and as he later suggested that he was expecting something more general than Blue's proof, I mentioned that (using the two remarks in my first post here), the same is probably true for any set of resolution rules: no such set can lead to an AR.

If you have finally understood the UR1.1, you should know, that already a kite can lead to an AR.

[denis_berthier]

If you have finally understood the UR1.1, you should know, that

Thanks for the "finally". I see you'll still in an aggressive mood.
I think I've understood it long ago, and much deeper than you.

already a kite can lead to an AR.

My conjecture may be false. As I said, I didn't check if the two ideas could effectively be used in a proof. Everybody knows you've never made any false conjecture.
But I'd like an example with the kite.

[eleven]

I don't have a sudoku in hands with an example, but it is clear, that it is possible, that a kite bites one of the UR candidates out (in this case 2 or more solutions may exist or not).
If i remember right, i have also seen a real world puzzle by Danny (daj), but i don't know, how to search for it in the forum.

[denis_berthier]

I don't have a sudoku in hands with an example, but it is clear, that it is possible, that a kite bites one of the UR candidates out (in this case 2 or more solutions may exist or not).

Why would it be so clear for a kite when it is false for the rules mentioned by David at the start?

[eleven]

"Simple fish" only include x-wing, swordfish (and maybe jellyfish ?). Those can only eliminate none or at least 2 of the UR candidates, the latter destroying the pattern (see blues' proof).