The concept of a RESOLUTION RULE and its applications

Advanced methods and approaches for solving Sudoku puzzles

Postby Glyn » Sat Nov 08, 2008 9:08 am

To all To allow the discussion of Isolated Subpuzzles/Uniqueness to continue without overburdening this thread I have started a new thread with a post by Allan Barker here Isolated Subpuzzles
Would subsequent posters on this particular issue please post in that thread.

I realise that much has already been said, but as this one could run on it has to be split at some point. Allan's post seems a good point to do that.
Last edited by Glyn on Sat Nov 08, 2008 5:18 am, edited 1 time in total.
Glyn
 
Posts: 357
Joined: 26 April 2007

Postby Red Ed » Sat Nov 08, 2008 9:13 am

eleven wrote: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.
Red Ed
 
Posts: 633
Joined: 06 June 2005

Postby coloin » Sat Nov 08, 2008 10:04 am

Red Ed wrote:But hang on, our 1/2/2/13 pencilmarks do not permit that solution -- contradiction!


But if it was a "rubbish" puzzle there might not be a contradiction......which is i believe denis's point.......but then, possibly, you will then know it is a "rubbish" puzzle......


If it is a valid puzzle the 1/2/2/1 will not be permitted.
coloin
 
Posts: 2493
Joined: 05 May 2005
Location: Devon

Postby Red Ed » Sat Nov 08, 2008 10:25 am

If by "rubbish" you mean "zero solutions" then I have to agree with you.

My proof assumes >0 solutions. So there is still an assumption about the solution count, but it's a weaker assumption than uniqueness.

@Denis: do you want to bother with the zero solutions case?
(EDIT: actually the zero solutions case is trivial. You should still resolve it to a 3. Either that'll give an immediate contradiction with a resolved 3 in the same row/col/box or it'll set you up for a contradiction later. Either way, no harm done.)
Red Ed
 
Posts: 633
Joined: 06 June 2005

Postby eleven » Sat Nov 08, 2008 10:50 am

Thanks to ronk, RedEd and coloin.
eleven
 
Posts: 3150
Joined: 10 February 2008

Postby StrmCkr » Sat Nov 08, 2008 7:08 pm

removed
Last edited by StrmCkr on Sat Dec 24, 2016 3:26 am, edited 1 time in total.
Some do, some teach, the rest look it up.
stormdoku
User avatar
StrmCkr
 
Posts: 1430
Joined: 05 September 2006

Postby denis_berthier » Sat Nov 08, 2008 8:12 pm

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.

Of course, this proof doesn't apply to UR1 and no obvious adaptation of it does; UR1 therefore remains dependent on the assumption of uniqueness. Believers of the independence have been invited to participate in another thread opened by Glyn and starting with an interesting post by Allan.


Now, using a kind of reasoning similar to RedEd's, let me show that any puzzle that can be solved with UR1.1 can be solved without it.
Suppose there is a puzzle P that can be solved thanks to the application of UR1.1 but that couldn't without it. Define P' as P plus one of the 3 entries in the UR1.1 pattern [supposing UR1.1 was used once; add similar entries if UR1.1 was used several times]. Then, by the very definition of P, P' can't be solved. As the entry added to P was proven from the axioms of P, it can't have introduced a contradiction in P'; nor can it have introduced a non-uniqueness problem. We thus get a contradiction.

Notice that this doesn't mean UR1.1 would be useless: it may still lead to simpler solutions. Nevertheless, given its very special status, as I'll explain later, this is enough for me not to use it. I'll give additional reasons in a later post.

Before giving further explanations, I'll let you meditate this. Is there anything wrong withRedEd's proof or with mine?
denis_berthier
2010 Supporter
 
Posts: 4197
Joined: 19 June 2007
Location: Paris

Postby StrmCkr » Sat Nov 08, 2008 10:24 pm

removed
Last edited by StrmCkr on Sat Dec 24, 2016 3:24 am, edited 1 time in total.
Some do, some teach, the rest look it up.
stormdoku
User avatar
StrmCkr
 
Posts: 1430
Joined: 05 September 2006

Postby eleven » Sun Nov 09, 2008 1:11 am

denis_berthier wrote:Notice that this doesn't mean UR1.1 would be useless: it may still lead to simpler solutions.
Thats the reason i do use it. Why not reduce your rules set to backtracking - it solves them all and you are finished.
The variety of solving techniques is the salt in the soup. When you decide to take this and drop that, your rules are as interesting as your neighbours music collection.
But this has been said before, and i know it will not change your attitude:(
eleven
 
Posts: 3150
Joined: 10 February 2008

Postby David P Bird » Sun Nov 09, 2008 1:23 am

denis_berthier wrote:
David P Bird wrote:
denis_berthier wrote:
r1c1 = 9 has the same consequences, be it a given or a deducted value.
As a result, starting from the situation in Myth UR1.1
1 2
2 13
it can't change anything to add the condition that the first 3 values were not givens.

This assertion is merely your own hypothesis which needs to be proved in all cases.

Not my hypothesis but a general logical and mathematical fact: a logical formula (e.g. r1c1 = 9) has the same consequences independent of whether it is an axiom (e.g. a given) or it is a consequence of the axioms (e.g. a decided value).
So do I take it that you retract your statement here?

Suppose there is a puzzle P that can be solved thanks to the application of UR1.1 but that couldn't without it. Define P' as P plus one of the 3 entries in the UR1.1 pattern [supposing UR1.1 was used once; add similar entries if UR1.1 was used several times]. Then, by the very definition of P, P' can't be solved. As the entry added to P was proven from the axioms of P, it can't have introduced a contradiction in P'; nor can it have introduced a non-uniqueness problem. We thus get a contradiction.
and how do rate this for opaqueness? (UR1.1 is simply a specific instance of the general case where a potential UR has been found to have a unique two-digit solution.)
David P Bird
2010 Supporter
 
Posts: 1043
Joined: 16 September 2008
Location: Middle England

Postby Red Ed » Sun Nov 09, 2008 1:25 am

StrmCkr wrote:yes there is an error in red eds proof as well,
Oh, go away.
Red Ed
 
Posts: 633
Joined: 06 June 2005

Postby denis_berthier » Sun Nov 09, 2008 2:32 am

Let's play a little longer with this riddle. I'd like someone else to find the solution.

1)
David P Bird wrote:
denis_berthier wrote:
David P Bird wrote:
denis_berthier wrote:
r1c1 = 9 has the same consequences, be it a given or a deducted value.
As a result, starting from the situation in Myth UR1.1
1 2
2 13
it can't change anything to add the condition that the first 3 values were not givens.

This assertion is merely your own hypothesis which needs to be proved in all cases.

Not my hypothesis but a general logical and mathematical fact: a logical formula (e.g. r1c1 = 9) has the same consequences independent of whether it is an axiom (e.g. a given) or it is a consequence of the axioms (e.g. a decided value).
So do I take it that you retract your statement here?

Certainly not.
But I'll let you meditate a little more time before I give further explanations.

2)
Red Ed wrote:
StrmCkr wrote:yes there is an error in red eds proof as well,
Oh, go away.


Notice I didn't say there is an error in RedEd's proof.

I said "Thanks, RedEd, for this very smart proof."
and
I asked "Is there anything wrong with RedEd's proof or with mine?"

Let me give some hint: is there any hidden hypothesis in RedEd's proof or in mine?


3) My answers 1 and 2 are equivalent.
denis_berthier
2010 Supporter
 
Posts: 4197
Joined: 19 June 2007
Location: Paris

Postby ronk » Sun Nov 09, 2008 2:37 am

denis_berthier wrote:Thanks, RedEd, for this very smart proof.

Thanks Denis, for finally seeing the light of day.
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

Postby denis_berthier » Sun Nov 09, 2008 2:39 am

ronk wrote:
denis_berthier wrote:Thanks, RedEd, for this very smart proof.

Thanks Denis, for finally seeing the light of day.

Sorry, Ronk, but the story is not yet over and you're not bringing much light to it.
denis_berthier
2010 Supporter
 
Posts: 4197
Joined: 19 June 2007
Location: Paris

Postby David P Bird » Sun Nov 09, 2008 4:16 am

Denis, please identify the hidden hypothesis in this version of Red Ed's proof.

1) The situation of interest is when by using the consequences of the givens external to the potential UR we are able to make a starting elimination of a single instance of one of a pair of competing digits because we've identified a violation to one of the one-only candidate rules were it allowed to survive.

2) This won't prevent the rectangle from being solved using the two digits, but will reduce the ways that this can be achieved from two to one.

3) If that single two-digit solution were true in the completed grid, we know we would be able to swap the digits around in these cells without violating any of the one-only rules. But our starting elimination has already established that this would violate one of those rules, so we know that this is an impossible situation.

4) Once we're able to make that starting elimination, we therefore know that there will be no two-digit solution of the potential UR involving the eliminated digit.

There is nothing new in this version that hasn't been stated in other ways previously.
David P Bird
2010 Supporter
 
Posts: 1043
Joined: 16 September 2008
Location: Middle England

PreviousNext

Return to Advanced solving techniques