The concept of a RESOLUTION RULE and its applications

Advanced methods and approaches for solving Sudoku puzzles

The confluence property

Postby denis_berthier » Wed Sep 17, 2008 12:10 am


THE CONFLUENCE PROPERTY


In the first edition of my book (May 2007), I've introduced the confluence property of resolution theories and shown that all the resolution theories I had introduced have this property. In this forum, I've mentioned this property only occasionally before I started dealing with rating. Confluence plays a major role as soon as we speak of rating. It may be why I first recalled its full definition in the "rating" thread: http://forum.enjoysudoku.com/viewtopic.php?t=5995&postdays=0&postorder=asc&start=90

But it would better fit here, among resolution rules/theories and their properties. So let me recall it again.
Choose a fixed set of resolution rules, i.e. a resolution theory: T.
Starting from a given puzzle, you can apply different resolution rules from T. For each choice of a rule, you get a new state (values + candidates).
Considering all the states you can get in iterating this process, and putting an arrow between two states if there is a rule leading from the first to the second (a resolution step), you get a graph of "knowledge states". Nothing mystical here: by definition, a knowledge state is just what you can see on a grid (values + candidates), what you explicitly know about it, in short what is usually called the PM, at some point in the resolution process along some resolution path.

A final state is a state in which no rule can be applied. Normally, most puzzles with a unique solution should have a single final state, if T is sufficiently powerful: the solution. But this is not always the case, depending on T.

Definition: a resolution theory T has the confluence property if any two partial resolution paths can be completed to meet at a same knowledge state.
Consequence: if a resolution theory T has the confluence property, then for any puzzle P there is a single final state and all the resolution paths lead to this state. In particular, if T solves P, one can't miss the solution by choosing to apply the "wrong" rule at any time.


I've given this definition in the context of my conceptual framework, based on the well defined concept of a resolution rule (whose conditions are based on and only on the current state of knowledge) and on the view that a puzzle is solved sequentially (i.e. only one rule is applied at a time). I don't care discussing fuzzy distortions of this definition in other ill defined frameworks or in the view that several rules can be applied in parallel.

One important consequence of the confluence property of T is that you can super-impose on T any ordering of the rules you want (giving priorities to the rules is not part of first order logic). It won't change the state you'll finally get to. In pratice, this means that, if you have missed some elimination while you were using another rule (to assert values or eliminate candidates), the same rule or other rules in T will always allow you to do this elimination later. Still more concretely, it means that you, as a player, don't have to care about the order in which you apply the rules in T. This is a huge simplification in your player's life. And I think it is also a huge simplification if one wants to define a rating based on the rules in T.

This property allows to define a strategic level above the logic level (the level of the resolution rules) - which is itself above the implementation level in case the rules are implemented in a computer program.
Concretely, I'll soon (I mean as soon as I've time) give examples of how one can take advantage of this property to define a lot of different resolution strategies for a given resolution theory having it.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Confluence and rules for uniqueness

Postby denis_berthier » Wed Sep 17, 2008 12:18 am


Confluence and rules for uniqueness


By definition, resolution rules are logical consequences of the Sudoku axioms (which do not include uniqueness). If one wants to consider uniqueness, we can define similarly U-resolution rules (which are consequences of the Sudoku axioms plus the axiom of uniqueness) and U-resolution theories.

Examples of a BUG that disappears after other rules have been applied are well known.

As another example of the problems raised by such rules, let me prove the following:

Theorem: let T be any resolution theory. If UR1 (Unique Rectangles type 1) is added to it, then the resulting U-resolution theory can't have the confluence property.
Remember that, by definition, any resolution theory contains ECP (elementary constraints propagation rules) and NS (Naked-Single rule); this is the minimal reasonable assumption on a resolution theory.
Proof:
UR1 is defined by the condition pattern:
Code: Select all
{1 2} --------- {1 2}
  :               :
{1 2} --------- {1 2 3}

(all 4 cells in exactly two rows, two columns and two blocks)

and by the conclusion that 3 can be asserted in the rightmost bottom cell.

Suppose we add UR1 to T.
Suppose this patterns appears at some point in the resolution process of a puzzle P but, for any reason, rule UR1 is not applied immediately (e.g. because you haven't seen it). If any candidate in any of the other 3 cells is eliminated by any other rule in T, then, using ECP and NS, these 3 cells are reduced to one candidate and the 4th cell is reduced to {1 3} or {2 3}.
What remains is the mere pattern of bivalue cell, for which there can exist no resolution rule able to eliminate 1 or 2.
q.e.d.

Now that I've given the general principle of such proofs of non-confluence, anyone can extend the above theorem to other cases of URs or to other Uniqueness rules.
As I'm not interested by uniqueness, that's all I'll say about it.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Re: Confluence and rules for uniqueness

Postby ronk » Wed Sep 17, 2008 5:28 am

denis_berthier wrote:
Code: Select all
{1 2} --------- {1 2}
  :               :
{1 2} --------- {1 2 3}

(all 4 cells in exactly two rows, two columns and two blocks)

and by the conclusion that 3 can be asserted in the rightmost bottom cell.

Suppose we add UR1 to T.
Suppose this patterns appears at some point in the resolution process of a puzzle P but, for any reason, rule UR1 is not applied immediately (e.g. because you haven't seen it). If any candidate in any of the other 3 cells is eliminated by any other rule in T, then, using ECP and NS, these 3 cells are reduced to one candidate and the 4th cell is reduced to {1 3} or {2 3}.
What remains is the mere pattern of bivalue cell, for which there can exist no resolution rule able to eliminate 1 or 2.
q.e.d.

When none of the UR cells is a given, missing UR digits may be freely "reinvented."
q.e.d.
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

Re: Confluence and rules for uniqueness

Postby denis_berthier » Wed Sep 17, 2008 5:37 am

ronk wrote:When none of the UR cells is a given, missing UR digits may be freely "reinvented."
q.e.d.

Where do you see that candidates can be "reinvented" in my framework?
And anyway, which candidates would you reinvent when you haven't seen the UR and you are left with only a bivalue cell?
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby Myth Jellies » Thu Sep 18, 2008 12:53 am

Denis wrote:As I'm not interested by uniqueness, that's all I'll say about it.


And yet you keep on saying quite a bit, despite your lack of interest.

The simplest refutation is that UR type 1 is not completely defined by that pattern, therefore your proof is invalid.

So q.e.d. not!

Another confluence observation concerns your non-degenerate naked triple. Let us choose T to be your non-degenerate naked triple along with the singles. Seems to me that one could come up with a puzzle where the naked triple could knock out a candidate, but the pattern gets partially whacked by a single that gets applied first, and you can't use the triple deduction any more.

Interestingly, as in the UR case, this non-confluent behavior disappears when you use patterns that are potentially degenerate.:idea:
Myth Jellies
 
Posts: 593
Joined: 19 September 2005

Postby denis_berthier » Thu Sep 18, 2008 1:18 am

Myth Jellies wrote:The simplest refutation is that UR type 1 is not completely defined by that pattern, therefore your proof is invalid.

This is typical of your flawed reasoning: concluding something is false, just by negating the definitions used to prove it (but, of course, not proposing any other definition, so that no discussion is possible).
BTW, I found the definition I used here in Andrew Stuart's book. Is it all scrap (to use your elegant vocabulary)?

Myth Jellies wrote:Another confluence observation concerns your non-degenerate naked triple. Let us choose T to be your non-degenerate naked triple along with the singles. Seems to me that one could come up with a puzzle where the naked triple could knock out a candidate, but the pattern gets partially whacked by a single that gets applied first, and you can't use the triple deduction any more.

"seems to you": very convincing purely logical proof.
Seems you also failed to understand this: you can't take any set of rules and claim it has the confluence property.
The T you are defining here clearly doesn't have the confluence property: you must add Pairs to obtain it.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby ronk » Thu Sep 18, 2008 5:38 am

denis_berthier wrote:The T you are defining here clearly doesn't have the confluence property: you must add Pairs to obtain it.

True, unless the triple subsumes the degenerate case of a naked pair and a single.
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

Postby denis_berthier » Thu Sep 18, 2008 5:44 am

ronk wrote:
denis_berthier wrote:The T you are defining here clearly doesn't have the confluence property: you must add Pairs to obtain it.

True, unless the triple subsumes the degenerate case of a naked pair and a single.

As I already said, I don't use degenerate patterns.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Re: Confluence and rules for uniqueness

Postby ronk » Thu Sep 18, 2008 7:53 am

denis_berthier wrote:
ronk wrote:When none of the UR cells is a given, missing UR digits may be freely "reinvented."
q.e.d.

Where do you see that candidates can be "reinvented" in my framework?
And anyway, which candidates would you reinvent when you haven't seen the UR and you are left with only a bivalue cell?

Although it may not answer your questions directly, I defer to the discussion in progress here.
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

Re: Confluence and rules for uniqueness

Postby denis_berthier » Thu Sep 18, 2008 9:02 am

ronk wrote:
denis_berthier wrote:
ronk wrote:When none of the UR cells is a given, missing UR digits may be freely "reinvented."
q.e.d.

Where do you see that candidates can be "reinvented" in my framework?
And anyway, which candidates would you reinvent when you haven't seen the UR and you are left with only a bivalue cell?

Although it may not answer your questions directly, I defer to the discussion in progress here.

In my framework, I have no questions about URs or ghost candidates.
Thanks for the reference, but I really have no time, no interest in Uniqueness and no interest in the distorted versions of my definition of the confluence property.

I've just defined a whole class of new patterns, WHIPs, potentially a much stroger improvement over chains than lassos (here http://forum.enjoysudoku.com/viewtopic.php?t=5591&start=135). You'll understand it's much more interesting for me to spend time exploring their possibilities.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby Myth Jellies » Thu Sep 18, 2008 10:54 pm

denis_berthier wrote:
Myth Jellies wrote:The simplest refutation is that UR type 1 is not completely defined by that pattern, therefore your proof is invalid.

This is typical of your flawed reasoning: concluding something is false, just by negating the definitions used to prove it

That was just the simplest refutation concluding the proof was invalid. If you don't believe that invalidates a proof, then that explains much.
denis_berthier wrote:(but, of course, not proposing any other definition, so that no discussion is possible).

Perhaps if you would have kept the discussion in the thread I created for it instead of burying it in this one, you might have noticed that I came up with a potentially degenerate UR+1 pattern (which I also mentioned here).

denis_berthier wrote:BTW, I found the definition I used here in Andrew Stuart's book. Is it all scrap

Andrew's book is still the best one out there by far. Unfortunately it was written months ago. So if he did come up with that pattern for you and it was not just your interpretation--well, things progress.

denis_berthier wrote:(to use your elegant vocabulary)?

I don't recall ever writing "scrap". If I did it must have been a typo.

denis_berthier wrote:
Myth Jellies wrote:Another confluence observation concerns your non-degenerate naked triple. Let us choose T to be your non-degenerate naked triple along with the singles. Seems to me that one could come up with a puzzle where the naked triple could knock out a candidate, but the pattern gets partially whacked by a single that gets applied first, and you can't use the triple deduction any more.

"seems to you": very convincing purely logical proof.

Hard to argue with success:D

denis_berthier wrote:Seems you also failed to understand this: you can't take any set of rules and claim it has the confluence property.

I understand it perfectly--I'm pointing it out to you!
I understand that I CAN'T take any set of YOUR rules and claim it has the confluence property
I also understand that I CAN take any set of my potentially degenerate pattern based rules and claim it DOES possess the confluence property.
Do you understand yet?
Myth Jellies
 
Posts: 593
Joined: 19 September 2005

Postby denis_berthier » Fri Sep 19, 2008 12:53 am

Myth Jellies wrote:
denis_berthier wrote:
Myth Jellies wrote:The simplest refutation is that UR type 1 is not completely defined by that pattern, therefore your proof is invalid.

This is typical of your flawed reasoning: concluding something is false, just by negating the definitions used to prove it

That was just the simplest refutation concluding the proof was invalid. If you don't believe that invalidates a proof, then that explains much.

You should definitely learn the basics of logic, as I suggested to you more than a year ago on Eureka - my first experience with a Web forum; I have left it because I was tired of wasting my time with guys like you (to be fair, I must add that some of the people there were really interesting).
Just a hint: if you deny the definitions on which a theorem is based, that doesn't make the theorem false, that makes the whole thing meaningless.
You're confusing mathematical logic with the rhetoric of a low grade solicitor. It may impress a few un-brained groupies. But you've got no chance with me.

Myth Jellies wrote:
denis_berthier wrote:(but, of course, not proposing any other definition, so that no discussion is possible).

Perhaps if you would have kept the discussion in the thread I created for it instead of burying it in this one, you might have noticed that I came up with a potentially degenerate UR+1 pattern (which I also mentioned here).

This is the thread where my conceptual framework was introduced and is discussed; my definition of confluence takes its natural place here.
You created your thread when you understood that you needed to:
- evade a discussion in which you were drowning about AICs with ALSs based on non-existent candidates; you've been unable to provide any example;
- empty the notion of confluence of any precise meaning so as to be able to spend your time bickering about it - an activity for which I must admit you're a first class specialist.

But I've no time to waste with you. If you want to discuss with me about a pattern and its relation with confluence, it will be here (where confluence has a precise definition). And you'll have to define this pattern here. I'm not going to search the forum for it.

Myth Jellies wrote:
denis_berthier wrote:Seems you also failed to understand this: you can't take any set of rules and claim it has the confluence property.

I understand it perfectly--I'm pointing it out to you!

Thanks. I defined the concept but I didn't understand this! How stupid I am!javascript:emoticon(':(')
In my book, I defined precisely how my rules can be made into theories (sets of rules) that have the property. These sets are not arbitrary.

Myth Jellies wrote:I understand that I CAN'T take any set of YOUR rules and claim it has the confluence property

At least, that'd be a good thing.
But do you really understand it?
You had never heard this word of confluence before I introduced it (first in my book, May 2007, then in this forum). Anything you write about it proves you don't have the slightest idea of what it means. But you suddenly decided that this word could become fashionable; you want to look bright and you use it as you can.
For this purpose, you use one of your favourite methods: take a precise definition given by someone else in a well defined context, take it out of its context so as to make it meaningless, wrap all this into gibberish so as to hide what you did. You can finally make all the vague claims you want about it. If you are requested to provide examples, evade arrogantly into insults and slandering. Aren't you aware that you're transparent?

Confluence is meaningful in my sequential model of a resolution path. It is meaningless when you admit ghost candidates - which amounts to a parallel model of resolution.

Myth Jellies wrote:I also understand that I CAN take any set of my potentially degenerate pattern based rules and claim it DOES possess the confluence property.
Do you understand yet?

Yes, thanks a lot for caring, I understand very well that you haven't understood anything about confluence.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby ronk » Fri Sep 19, 2008 5:02 am

OFF TOPIC -- Hasn't Bill Richter left yet?

Oops, with decorum degenerating so rapidly here, for a minute there I thought I was on the Eureka! forum.:(
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

Postby denis_berthier » Fri Sep 19, 2008 6:52 am

ronk wrote:OFF TOPIC -- Hasn't Bill Richter left yet?
Oops, with decorum degenerating so rapidly here, for a minute there I thought I was on the Eureka! forum.:(

Great!
Can we now come back to the topics of this thread?
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby Myth Jellies » Wed Sep 24, 2008 1:16 am

I never left the topic.

If you wish to define your UR1 as the condition pattern
Code: Select all
{1 2} --------- {1 2}
  :               :
{1 2} --------- {1 2 3}

then it should be fairly obvious from what I have written that you will need extra patterns representing the remaining possibilities you have when you represent the logic by what candidates are missing.
Code: Select all
~{3-9} --------- ~{3-9}
   :                :
~{3-9} --------- ~{4-9}

Thus the generalized missing pattern (call it UR1.1) defined in terms of what candidates are present is
Code: Select all
{1} --------- {2}
 :               :
{2} --------- {1 3}
with the added proviso that the "solved" cells here were not among the original givens.


If T is a resolution theory that has the confluence propery then UR1.1 can be added T and the confluence property of T will be preserved. If T already has UR1.1, then your UR1 can be added to T and confluence will be preserved.

This contradicts your theory.

The proof regarding the confluence of patterns defined by what candidates are missing or solved is simple. Since you have no operations that can add candidates to the grid or unsolve them, once such a pattern exists it must remain for every successive solve state of the puzzle.

I cannot control what you find logical, useful, or a waste of time. Nor can I concern myself overmuch with your stated impressions of me. Time will tell in these matters. I do reserve my right to make comments and generate thought experiments on topics you present here; and will not be driven off by tactics of intimidation, misrepresentation, or ridicule.
Myth Jellies
 
Posts: 593
Joined: 19 September 2005

PreviousNext

Return to Advanced solving techniques

cron