The New Sudoku Players' Forum

[eleven]

Too short of time to answer more.
Let me start with, that i agree with Serg, that we should talk about the more general "RW's rule", which has exactly the same proof. Why should we always restrict us to a special case ? Because UR1.1's are harder to find ??

Here is a better example : this time I removed the 9 from r9c8 : .5........6.5.42....8.71...4....36.8.........89.1..7..3...........2.7.1..72.3.... and there were the following 175 solutions:
...
As far as I can see, the only other value that r2c9 can have is 3.

No, it is r3c2, which has 3 in all solutions, not r2c9. 7 and 9 can be in any cells of the rectangle r12c19, so you cannot use it without uniquness assumption.

Code: Select all

a  b
b  ac


...
Indeed, there are puzzles with multiple solutions where c is common to all the solutions of the puzzle (see the example proposed by Denis Berthier) and puzzles with multiple solutions where at least one solution does not contain c (I can propose some).

If none of them is a given, c must be part of a solution. This has been proved now again and again. But feel free to give a counter-example.

I tried Philip Beeby's solver. Using only steps up to 'Advanced Set' but not 'Deadly' takes one to :
[...]
so r2c9 is 3.

So, we reach the same conclusion: it doesn't result from some UR1.1

The conclusion is, that it can be derived without UR1.1. That is trivial.

... what's the (other) extra-logical assumption in RedEd's proof? My two cents is uniqueness, because in case of non-uniqueness, it seems that the a/b/b/ac pattern cannot be found in any resolution path if there is no given in the a/b/c part. All the examples examined until now support this conclusion.

The main reason, that we have no examples is, that no one searched for them. Why should one ? Just to give you an example for something, which is proved anyway ? Nobody here is interested in multi-solution puzzles. This is not worth the time. What is true is, that good examples are very rare and therefore hard to find.

So you can picture Red Ed's move as :

Code: Select all

12  12

12  12+3

ie I don't see any fundamental difference between UR1.1 and good old UR 1. Takes a bit of getting used to but it works - one of the best sections in Hodoku IMHO.

No. Only if you can eliminate one of the 1's or 2's (without uniqueness methods), you can place the 3 as a non uniqueness move.
Using uniqueness the UR1.1 is a also a simple hidden unique rectangle.

[Leren]

eleven wrote : No, it is r3c2, which has 3 in all solutions, not r2c9.

I don't get what you are trying to say here. In my original example puzzle, the UR1.1 cells were r12c19 and the elimination cell was r2c9.

I then tried making the solution to the entire puzzle non unique, to see what effect that had on this cell.

My first attempt had just 3 solutions and r2c9 was 3 in all 3 of them. My third attempt had 175 solutions and r2c9 had 3 possible values.

I've just "solved" this puzzle as far as I could and found that 9 cells have only one possible value, including, as you say, r3c2 = 3.

If anything I had done was not addressing the issue at hand I would have expected denis to say something about it, but he didn't say anything along these lines, but of course you are free to do so.

Leren

[denis_berthier]

Hi Serg

... Can you make it more general than the usual UR1?...

I am not quite understand - what generalization do you mean.[...]

It was in relation to opening a new thread.
I meant, if your formulation is equivalent to UR1, I don't think there'll be much to discuss in your new thread. UR1 is perfectly clear.
Maybe you should have a look at the Hodoku doc. They define UR1 ... UR6 and BUG. (The explanations are awful, but the rules are clear).

[denis_berthier]

For the avoidance of any semantic misunderstanding the phrase I used was mentally "put back". By this I meant that you don't actually reintroduce the eliminated candidate, you just imagine what the puzzle was like before you eliminated it.

Ok, this more or less cancels my objections 1 and 2 if you do this only for UR1 or a few easy patterns; it wouldn't work if you do this for all the possible chain patterns.
But objections 3 and 4 remain valid:
- If the URI has never been actually present on the grid, there's no guarantee that any resolution path would find it; it means you may be creating a resolution state that no resolution path could reach
- It supposes uniqueness. You already think UR1.1 does (like me), it's not a problem for us, but it's one for those who say it doesn't.

There is a similar trick that comes up, for example, in UR type 6's. I've got an example where I can eliminate 4 candidates in a 4 cell UR Type 6 pattern, but if I make the eliminations sequentially, I will miss some of the others. What I do is check all of the 8 UR digits in the pattern, to see if they can be proven False. A candidate that has already been proven False is not immediately eliminated and may form part of the proof that another candidate is False.
So you might characterise this as "delaying the elimination of a False candidate" rather than "reintroducing" it.

I think this case is different. You've found a real pattern on the grid. You note all the candidates that it could eliminate and the you eliminate them all at once.

[Leren]

denis_bertier wrote : But objections 3 and 4 remain valid:
- If the URI has never been actually present on the grid, there's no guarantee that any resolution path would find it; it means you may be creating a resolution state that no resolution path could reach

Really ? Applying basics to my original puzzle, You get to here.

Code: Select all

*--------------------------------------------------------------------------------*
| 79cC    5       4        | 3       268     268      | 19bB    68     a79-1aA   |
| 79dD    6       1        | 5       89eE    4        | 2      j378hF   379      |
| 2       3       8        |d69      7       1        | 45      456    c459      |
|--------------------------+--------------------------+--------------------------|
| 4       1       57       |e79      259f    3        | 6       25g     8        |
| 56      2      g3567     |f4678    4568    568      | 19     h345    b19       |
| 8       9       356      | 1       2456    256      | 7       2345    2345     |
|--------------------------+--------------------------+--------------------------|
| 3       48      56       | 468     1       9        | 458     27g     27       |
| 56      48      9        | 2       4568    7        | 3       1       456      |
| 1       7       2        | 468     3       568      | 458     9       456      |
*--------------------------------------------------------------------------------*

Kraken Cell r2c8: 

1 r1c9 - (1=9) r5c9 - 9r3c9 = 9r3c4 - (9=7) r4c4 - 7r5c4 = (7-3) r5c3 = 3r5c8 - 3r2c8;

1 r1c9 - (1=9) r1c7 - 9r1c1 = 9r2c1 - 9r2c5 = (9-2) r4c5 = 2r4c8 - (2=7) r7c8 - 7r2c8;

1 r1c9 - (1=9) r1c7 - 9r1c1 = 9r2c1 - (9=8) r2c5                              - 8r2c8; => - 1  r9c9

After this we have:

Code: Select all

*--------------------------------------------------------------------------------*
|*79      5       4        | 3       268     268      | 19      68     *79       |
|*79      6       1        | 5       89      4        | 2       378    *379      |
| 2       3       8        | 69      7       1        | 45      456     459      |
|--------------------------+--------------------------+--------------------------|
| 4       1       57       | 79      259     3        | 6       25      8        |
| 56      2       3567     | 4678    4568    568      | 19      345     19       |
| 8       9       356      | 1       2456    256      | 7       2345    2345     |
|--------------------------+--------------------------+--------------------------|
| 3       48      56       | 468     1       9        | 458     27      27       |
| 56      48      9        | 2       4568    7        | 3       1       456      |
| 1       7       2        | 468     3       568      | 458     9       456      |
*--------------------------------------------------------------------------------*

UR (79) r12c19 => - 79 r2c9. However, we won't actually take that path, Instead we have:

Code: Select all

*--------------------------------------------------------------------------------*
| 79bB    5       4        | 3       268     268      | 1       68     a7-9aA    |
| 79cC    6       1        | 5       89dD    4        | 2      g378gE   379      |
| 2       3       8        |c69      7       1        | 45      456    b459      |
|--------------------------+--------------------------+--------------------------|
| 4       1      e57       |d79      259e    3        | 6      f25f     8        |
| 56      2       3567     | 4678    4568    568      | 9       345     1        |
| 8       9       356      | 1       2456    256      | 7       2345    2345     |
|--------------------------+--------------------------+--------------------------|
| 3       48      56       | 468     1       9        | 458     27      27       |
| 56      48      9        | 2       4568    7        | 3       1       456      |
| 1       7       2        | 468     3       568      | 458     9       456      |
*--------------------------------------------------------------------------------*

Kraken Cell r2c8:   

9r1c9 - 9r3c9 = 9r3c4 - (9=7) r4c4 - 7r5c4 = (7-3) r5c3 = 3r5c8 - 3r2c8;

9r1c9 - 9r1c1 = 9r2c1 - 9r2c5 = (9-2) r4c5 = 2r4c8 - (2=7) r7c8 - 7r2c8;

9r1c9 - 9r1c1 = 9r2c1 - (9=8) r2c5                              - 8r2c8; => - 9 r1c9;

After some more basics we get to here:

Code: Select all

*--------------------------------------------------------------------------------*
|*9       5       4        | 3       268     268      | 1       68     *7        |
|*7       6       1        | 5       89      4        | 2       38     *3-9      |
| 2       3       8        | 69      7       1        | 45      456     459      |
|--------------------------+--------------------------+--------------------------|
| 4       1       57       | 79      259     3        | 6       25      8        |
| 56      2       3567     | 4678    4568    568      | 9       345     1        |
| 8       9       356      | 1       2456    256      | 7       2345    345      |
|--------------------------+--------------------------+--------------------------|
| 3       48      56       | 468     1       9        | 458     7       2        |
| 56      48      9        | 2       4568    7        | 3       1       456      |
| 1       7       2        | 468     3       568      | 458     9       456      |
*--------------------------------------------------------------------------------*

UR1.1 (79) r12c19 => - 9 r2c9; stte

Leren

[denis_berthier]

denis_bertier wrote : But objections 3 and 4 remain valid:
- If the URI has never been actually present on the grid, there's no guarantee that any resolution path would find it; it means you may be creating a resolution state that no resolution path could reach

Really ? Applying basics to my original puzzle, You get to here.[...]

I was not speaking of this case in particular. I meant, how can you be sure that, in every case a UR1.1 appears, there must have been a UR1 before it in some resolution path? [It may be true, I don't know, but that's very far from obvious - unless, of course, no UR1.1 can ever appear if there was no clue on any of the 4 cells.]

[Leren]

Hi denis,

This thread is not just a storm in a teacup, it's more like a hurricane in a thimble, but here goes anyway. You say you are a mathematician, so I think you would accept the various forms of proof : by construction, by induction, by contradiction etc.

I think I may have a convincing argument (at least for me) using proof by contradiction. I know that's considered ugly in Sudoku solving, but it is mathematically valid. OK let's start with some baby steps.

Code: Select all

a     b           a.b   b.a           a.bd   b.a

b     a.c         b.a   a.bc          b.a    a.bc

The three diagrams are 1. What we know is assumed to be True, a UR1.1 pattern. 2. A UR.1 pattern that must precede it (by my assertion). 3. A disrupting digit d in the top left cell.

Now what we also know about those diagrams, is that all the letters to the left of the decimal points are True and those to the right of the decimal points are False (by the first diagram and UR1.1).

I think your doubts can be boiled down to the proposition that it is impossible to prove that d is False without first proving that b is False (in the top left hand cell of the third diagram).

Now assume that d is True (that implies that a and b are both False but doesn't actually prove anything about them. We know that a is in fact True and b is False).

Well, if you do that, since we know that d is in fact False, you must eventually end up with a contradiction (at least one unsolved cell with no candidates). So you can remove d from diagram 3 and end up with diagram 2, QED.

It would be nice if we could say with some certainty that some constructive proof could always be found, no matter how complex and messy, that could come to the same conclusion, but I think it's not actually necessary for a mathematician.

Also I think you could add more letters to the right of the decimal points in all cells of the third diagram and run through the same argument as many times as necessary and it still works.

Over to you. Leren

[Mauriès Robert]

Hi Denis and Leren,
Have you read my post of February 25th?
Robert

[denis_berthier]

Hi Denis and Leren,
Have you read my post of February 25th?

Yes, and I answered.

[Mauriès Robert]

No Denis, you replied to the one of February 24 but not to the one of February 25.
Robert

[denis_berthier]

You say you are a mathematician, so I think you would accept the various forms of proof : by construction, by induction, by contradiction etc

Yes, these are classical methods. However, depending on one's goals, constructiveness may be necessary and then proofs by contradiction are not applicable. Mathematicians don't make it a personal matter; they know that different goals imply different methods. All they need is being clear on one's hypotheses.

I think I may have a convincing argument (at least for me) using proof by contradiction. I know that's considered ugly in Sudoku solving, but it is mathematically valid. OK let's start with some baby steps.

Code: Select all

a     b           a.b   b.a           a.bd   b.a

b     a.c         b.a   a.bc          b.a    a.bc

The three diagrams are 1. What we know is assumed to be True, a UR1.1 pattern. 2. A UR.1 pattern that must precede it (by my assertion). 3. A disrupting digit d in the top left cell.
Now what we also know about those diagrams, is that all the letters to the left of the decimal points are True and those to the right of the decimal points are False (by the first diagram and UR1.1).
I think your doubts can be boiled down to the proposition that it is impossible to prove that d is False without first proving that b is False (in the top left hand cell of the third diagram).

Not exactly. My doubts are about whether it is always possible. Your example with 3 solutions already showed that it is sometimes possible.

Now assume that d is True (that implies that a and b are both False but doesn't actually prove anything about them. We know that a is in fact True and b is False).
Well, if you do that, since we know that d is in fact False, you must eventually end up with a contradiction (at least one unsolved cell with no candidates). So you can remove d from diagram 3 and end up with diagram 2, QED.

Yes, you are right of course, and it answers my doubts to some point.

But, as you noticed at the beginning, the question is, what does one consider as an "acceptable" method?
If one wants a "pattern-based" resolution method (based only on resolution rules), can he accept that those rules be themselves proven (from the four axioms of Sudoku) by methods that he wouldn't accept applying directly in his resolution process (e.g. T&E or DFS)?
There is no general answer. It's up to everyone to decide what he wants to use.

There are (at least) 3 possible positions, from broadest to strictest:
1) accept any type of methods;
2) accept only constructive rules, but accept that some of those rules (e.g. all the uniqueness rules) can themselves be proven (from the axioms of Sudoku) by non-constructive methods; your proof falls in this category;
3) accept only constructive rules proven by constructive methods.

Discussions about what one accepts or not are pointless.
I personally never use uniqueness or any non-constructively proven rule (position 3) when I want a solution with an explicit resolution path, but SudoRules has uniqueness rules for users who want to use them (position 2). SudoRules also has (very inefficient) T&E and DFS methods (corresponding to position 1); if at some point in time, my goal is to have the fastest solution, I use DFS.
[There's no UR1.1 rule in SudoRules because I'm much too lazy to code a "rule" for which nobody has any example. My last objection about UR1.1 is not about the proof (as I said, my first formulation was inadequate), it's about its conditions (with the "unclued" clause) being impossible.]

It would be nice if we could say with some certainty that some constructive proof could always be found, no matter how complex and messy, that could come to the same conclusion, but I think it's not actually necessary for a mathematician.

Some mathematicians work on constructive maths; it's necessary for them. But I agree with you.
BTW, I can indeed say that a constructive solution of all the (known) valid 9x9 puzzles always exists: they can all be solved by B-braids (and even by B7-braids). But a long sequence of B-braids (for the hardest puzzles) is not something one would want to read.

Also I think you could add more letters to the right of the decimal points in all cells of the third diagram and run through the same argument as many times as necessary and it still works.

I have no doubt that it'd work the same way.

[denis_berthier]

No Denis, you replied to the one of February 24 but not to the one of February 25.

Ach. I missed it.

[denis_berthier]

Hi Robert,

It seems to me that it is impossible, in a puzzle, to see the following UR1.1 configuration appearing
a b
b ac
otherwise than :
- either because a and b are data,
- or because it is possible to eliminate by logical resolution procedures (basic techniques, AIC, track, braid, etc...) candidates b and a (in red) from a following UR1 configuration
ab ba
ba abc
Therefore, since the use of UR1 is justified only by the announced uniqueness of the solution of the puzzle, the same applies to the use of UR1.1 which no other reason can justify.

It seems we more or less reach the same conclusion.

[Mauriès Robert]

Hi Eleven and Denis,

Code: Select all

a  b
b  ac


...
Indeed, there are puzzles with multiple solutions where c is common to all the solutions of the puzzle (see the example proposed by Denis Berthier) and puzzles with multiple solutions where at least one solution does not contain c (I can propose some).

If none of them is a given, c must be part of a solution. This has been proved now again and again. But feel free to give a counter-example.

Here is a puzzle that presents UR1.1 (7/9/7/39) in cells r12c19 and has 5 solutions, 3 containing the 9r2c9 that rule UR1.1 should eliminate and 2 containing the 3r2c9.

puzzle: Show

Denis Berthier gave on this thread an example of a single solution puzzle that does not respect UR1.1 and another example of a multiple solution puzzle that respects UR1.1 for all solutions.
For me, these three examples show that the UR1.1 rule, even with the assumption of uniqueness, has no basis and that its proper functioning in a resolution is pure chance.
Sincerely
Robert

[champagne]

Hi Eleven and Denis,

Here is a puzzle that presents UR1.1 (7/9/7/39) in cells r12c19 and has 5 solutions, 3 containing the 9r2c9 that rule UR1.1 should eliminate and 2 containing the 3r2c9.

puzzle: Show

Denis Berthier gave on this thread an example of a single solution puzzle that does not respect UR1.1 and another example of a multiple solution puzzle that respects UR1.1 for all solutions.
For me, these three examples show that the UR1.1 rule, even with the assumption of uniqueness, has no basis and that its proper functioning in a resolution is pure chance.
Sincerely
Robert

Sorry Robert, but your example shows nothing. It is as relevant as an old example given by Denis.

The first condition to produce an example is to have no given in the UR area.

BTW, reading your comments on the UR1.1 logic, it seemed to me that you understood the proof. This example is the proof that I was wrong