The concept of a RESOLUTION RULE and its applications

Advanced methods and approaches for solving Sudoku puzzles

Postby denis_berthier » Fri Nov 14, 2008 11:30 pm

re'born wrote:
Denis wrote:I've mentioned other possibilities of using two nrczt-chains, here http://forum.enjoysudoku.com/viewtopic.php?t=5591&postdays=0&postorder=asc&start=120
It is very inefficient. I can't prove this formally but I've tried.

Thank you, Denis. Until I see evidence to the contrary, I'll take your word for it.

There's another possibility: you can try to find examples such that there's no chain no longer than the sum of the lengths of the two chains and allowing the same elimination.
You'll see at least how hard it is to deal with two chains at the same time.
denis_berthier
2010 Supporter
 
Posts: 4234
Joined: 19 June 2007
Location: Paris

Postby re'born » Sat Nov 15, 2008 12:41 am

denis_berthier wrote:
re'born wrote:
Denis wrote:I've mentioned other possibilities of using two nrczt-chains, here http://forum.enjoysudoku.com/viewtopic.php?t=5591&postdays=0&postorder=asc&start=120
It is very inefficient. I can't prove this formally but I've tried.

Thank you, Denis. Until I see evidence to the contrary, I'll take your word for it.

There's another possibility: you can try to find examples such that there's no chain no longer than the sum of the lengths of the two chains and allowing the same elimination.
You'll see at least how hard it is to deal with two chains at the same time.

For me, chain length was never a very reliable measure of how difficult it was to find. Incidentally, have you read Bud's recent post? He is combining chains in a different way in a simple case: 2 xy-wings.
re'born
 
Posts: 551
Joined: 31 May 2007

Postby denis_berthier » Sat Nov 15, 2008 1:02 am

re'born wrote:For me, chain length was never a very reliable measure of how difficult it was to find.

Not reliable in the absolute, I agree. But very meaningful statistically (see the "rating rules" thread: http://forum.enjoysudoku.com/viewtopic.php?t=5995)

re'born wrote:Incidentally, have you read Bud's recent post? He is combining chains in a different way in a simple case: 2 xy-wings.

Thanks for the reference. I'll have a look.
Trying to combine simple patterns into new ones may be interesting if it leads to eliminations that weren't available by a mere application of these patterns and of other more basic rules.
The problem is different with longer chains: complexity is squared.
denis_berthier
2010 Supporter
 
Posts: 4234
Joined: 19 June 2007
Location: Paris

Postby re'born » Sat Nov 15, 2008 4:20 am

denis_berthier wrote:
re'born wrote:For me, chain length was never a very reliable measure of how difficult it was to find.

Not reliable in the absolute, I agree. But very meaningful statistically (see the "rating rules" thread: http://forum.enjoysudoku.com/viewtopic.php?t=5995)

Yes, I can see why it is a natural way for you to break up chains (in terms of cataloging). For the manual solver, the difficulty of finding certain chains depends only vaguely on length, e.g., chains such that consecutive candidates form a conjugate pair, remote naked pairs, xy-chains or extended w-wings.

re'born wrote:Incidentally, have you read Bud's recent post? He is combining chains in a different way in a simple case: 2 xy-wings.


Denis wrote:Thanks for the reference. I'll have a look.
Trying to combine simple patterns into new ones may be interesting if it leads to eliminations that weren't available by a mere application of these patterns and of other more basic rules.

For a computer, probably. For a manual solver, it isn't as clear cut. Start with a puzzle whose difficulty is unknown. As you begin solve it, you notice an xy-wing, make the elimination and move on. Later, you go post your solution and udosuk informs you it could be solved with singles. Should I have taken the xy-wing move?
re'born
 
Posts: 551
Joined: 31 May 2007

Postby denis_berthier » Sat Nov 15, 2008 4:34 am

re'born wrote:For the manual solver, the difficulty of finding certain chains depends only vaguely on length, e.g., chains such that consecutive candidates form a conjugate pair, remote naked pairs, xy-chains or extended w-wings.

The manual sover has to find useful chains amo,ng lots of useless ones. He is no better at this than the computer.

re'born wrote:For a manual solver, it isn't as clear cut. Start with a puzzle whose difficulty is unknown. As you begin solve it, you notice an xy-wing, make the elimination and move on. Later, you go post your solution and udosuk informs you it could be solved with singles. Should I have taken the xy-wing move?

Any move you take is OK.
But the problemis: how likely is this example?
denis_berthier
2010 Supporter
 
Posts: 4234
Joined: 19 June 2007
Location: Paris

Postby re'born » Sat Nov 15, 2008 12:45 pm

denis_berthier wrote:
re'born wrote:For a manual solver, it isn't as clear cut. Start with a puzzle whose difficulty is unknown. As you begin solve it, you notice an xy-wing, make the elimination and move on. Later, you go post your solution and udosuk informs you it could be solved with singles. Should I have taken the xy-wing move?

Any move you take is OK.
But the problemis: how likely is this example?

Well, I won't speak for other solvers, but for me this particular scenario happens consistently if I'm in the mood to look at bivalue cells. Replace xy-wing with x-wing, however, and it becomes better than even money. Replace x-wing with locked candidates and it's a mortal lock.
re'born
 
Posts: 551
Joined: 31 May 2007

Postby denis_berthier » Sat Nov 15, 2008 9:22 pm

re'born wrote:Incidentally, have you read Bud's recent post? He is combining chains in a different way in a simple case: 2 xy-wings.

Nothing really new. No new elimination: sequence of 2 xy-wings and an xy-chain.
denis_berthier
2010 Supporter
 
Posts: 4234
Joined: 19 June 2007
Location: Paris

Postby aran » Mon Nov 17, 2008 11:44 am

Denis
aran wrote:

Let (a,b) be an ordered cell source cell for xyt chain A.
Then (b,a) is an ordered cell from which there may be an xyt chain B different from A.
Whatever the length of A, and whatever the length of B, each and every right hand link of A is strongly linked to each and every right hand link of B.

Completely absurd.

It's a few days back, but in the interval I hope it has dawned that the absurd party wasn't the one being targeted...

Re'born : this is the real Aran speaking:) ...wrote
If you have an xyt-chain (a b) - ... - (w x) (where (w x) might be modulo some t-candidates)
and if you have another xyt-chain (b a) - ... - (y z) (where, again, (y z) might be modulo some t-candidates),
then we can read the first chain as saying if a is not true, then x is true and the second as saying if b is not true then z is true. Since a or b is true, we conclude x or z is true, i.e., x is strongly linked to z.

Aran, is this what you are saying?

I am saying that but more than that.
All of the right-hand links in the ordered cells in the respective xyt chains (starting from cell C respectively ordered (a,b) and (b,a)) are strong-linked : not merely the final cell.
Think of it in terms of transport : each of the right-hand links in the starting cell ie b for (a,b) and a for (b,a) is in effect transported by the xyt chain (remembering that the "backward-looking" t candidates by virtue of their seeing preceding "truths" in the chain do not hinder chain progression).
Then each T (as in Truth) in the first chain is strong-linked to each T in the second.
This generates multiple strong-links.
What I was saying (and Denis seems unable to see this point) is that within his own system, if he wants it to be efficient, or less inefficient, he could easily (ie for little extra work) examine these links for possible eliminations.
Note that eliminations found in this way might not necessarily be found by any xyt chain examined singly. One cannot in fact say at what point they would emerge in that system.

As to the example I gave, it is entirely well-founded.
Here it is again :
Suppose that P and Q are nrc-linked cells in the respective chains.
Say the ordered cells are P (257) and Q (1345) (ie t candidates 5 and 34)
=>7P 5Q strongly linked
=>given the nrc-link : P <5>.
Thus whether or not there was a z elimination, there is a t elimination in this example.

(Apparently I'm misusing "nrc-linked" which in any case just means "sees")
So P and Q see each other and are in the respective chains.
Therefore their right-hand links (or "True" candidates) are strongly-linked.
Hence either 7 is true in P or 5 in Q or both, and whatever, 5 must be eliminated from P.
In this example, it so happens that a "t" candidate is eliminated.

I did not say and am not saying that there will necessarily be t eliminations, nor indeed any eliminations.
If I used the "t" elimination in my example it was to illustrate the curiosity of setting out to target "z" eliminations (plural because of both chains) and ending up...paradoxically... with a "t" one.

Of course, a second type of possible elimination arises where the respective right-hand links are strongly linked on the same candidate, say w. In this case any w seen by both is eliminated (which does not impose the condition that the strong-link candidates see each other).
aran
 
Posts: 334
Joined: 02 March 2007

Postby denis_berthier » Mon Nov 17, 2008 9:28 pm

Aran,
In my framework, a rule asserts value(s) and eliminates candidate(s). There's no intermediate goal of computing all the possible indirect "strong links".
If you want to propose a new rule that asserts "strong links" or that eliminates t-candidates, based on some combination of xyzt or nrczt chains, and dealing with notions completely alien to my framework, such as "strong links", I suggest you open a new thread for this.
We're eager to learn about efficiency matters from you.
denis_berthier
2010 Supporter
 
Posts: 4234
Joined: 19 June 2007
Location: Paris

Postby re'born » Tue Nov 18, 2008 4:26 am

aran wrote:I am saying that but more than that.
All of the right-hand links in the ordered cells in the respective xyt chains (starting from cell C respectively ordered (a,b) and (b,a)) are strong-linked : not merely the final cell.

I think we're on the same page. My view of an xyt-chain is that you can remove the last cell and it remains an xyt-chain. Therefore, what you said is an immediate consequence of what I said.
re'born
 
Posts: 551
Joined: 31 May 2007

Postby aran » Tue Nov 18, 2008 8:19 am

Re'born
aran wrote:

I am saying that but more than that.
All of the right-hand links in the ordered cells in the respective xyt chains (starting from cell C respectively ordered (a,b) and (b,a)) are strong-linked : not merely the final cell.

I think we're on the same page. My view of an xyt-chain is that you can remove the last cell and it remains an xyt-chain. Therefore, what you said is an immediate consequence of what I said.


Indeed you are right.

Denis

Aran,
In my framework, a rule asserts value(s) and eliminates candidate(s). There's no intermediate goal of computing all the possible indirect "strong links".
If you want to propose a new rule that asserts "strong links" or that eliminates t-candidates, based on some combination of xyzt or nrczt chains, and dealing with notions completely alien to my framework, such as "strong links", I suggest you open a new thread for this


The rule doesn't eliminate candidates de nihilo : patterns aren't identified without being looked for, and any eliminations arising result from strong links at the chain ends. Even if you don't give them a name nor refer to them.

We're eager to learn about efficiency matters from you.

I know this is well meant so here is a point to be going on with :
E1 : Efficiency of Presentation.
Present all your eliminations in rc-space regardless of what space you found them in.
Benefits : make your work accessible to a wider public.
aran
 
Posts: 334
Joined: 02 March 2007

Postby denis_berthier » Wed Nov 19, 2008 3:27 am

aran wrote:
Aran,
In my framework, a rule asserts value(s) and eliminates candidate(s). There's no intermediate goal of computing all the possible indirect "strong links".
If you want to propose a new rule that asserts "strong links" or that eliminates t-candidates, based on some combination of xyzt or nrczt chains, and dealing with notions completely alien to my framework, such as "strong links", I suggest you open a new thread for this

The rule doesn't eliminate candidates de nihilo : patterns aren't identified without being looked for

Of course, you have to look for patterns. There's no miracle. But, in my approach, you don't have to look for all the possible indirect "strong links" independently of patterns (Pairs, chains, whips, ...) in which you know in advance they will be useful. That's all the difference with what you were suggesting.

aran wrote:Present all your eliminations in rc-space regardless of what space you found them in.

AFAIK, that's what I do. I always write an elimination "=> rc <> n", as everybody.
denis_berthier
2010 Supporter
 
Posts: 4234
Joined: 19 June 2007
Location: Paris

Postby denis_berthier » Wed Dec 10, 2008 7:16 pm


FROM CONSTRAINTS TO RESOLUTION RULES


Many real world problems, such as resource allocation, temporal reasoning or scheduling, naturally appear as constraint satisfaction problems (CSP).
Constraints satisfaction is a main sub-area of Artificial Intelligence.

A finite CSP is defined by a finite number of variables with values in some fixed finite domains and a finite set of constraints (i.e. of relations they must satisfy); it consists of finding a value for each of these variables, such that they globally satisfy all the constraints. It can be formulated as a First Order Logic (FOL) theory.

Sudoku is obviously a CSP. The "natural" variables are the Xrc (one variable for each row r and each column c), with range the set of numbers {1 2 3 4 5 6 7 8 9} that can occupy these cells; but it is convenient to add auxiliary variables Xbs, Xrn, Xcn, Xbn to take into account the natural symmetries and super-symmetries of the problem.

Variants of Sudoku are CSPs and so are many other "logic games".


Most of what I've done for Sudoku can be extended to any finite CSP:

* the whole general conceptual framework in Multi-Sorted First Order Logic (MS-FOL);
* definition of candidates and elaboration of their logical epistemic status;
* definition of candidates being linked by a direct contradiction or simply "linked" (what I've called "nrc-linked" in Sudoku);
* definitions of a resolution rule, a resolution theory, the solution of a CSP according to a resolution theory, a resolution strategy;
* definition of a chain and a target;
* definition of a bivalue variable and a bivalue chain (which corresponds to an xy-chain or to an nrc-chain, depending on which set of variables we take as primitive);
* definitions of t-, z- and zt- chains, whips and braids;
* proof of the zt- chain, whip and braid elimination theorems;
* proof of the confluence property for naturally defined zt-braid resolution theories;
* proof of the T&E vs zt-braids elimination theorem.

Details can be found in two presentations I've done at the CISSE'08 conference (http://www.cisse2008online.org).
pdf preprints of the associated papers can be found on my Web pages dedicated to Sudoku: http://www.carva.org/denis.berthier/HLS (permanent URL).
denis_berthier
2010 Supporter
 
Posts: 4234
Joined: 19 June 2007
Location: Paris

Re: The concept of a RESOLUTION RULE and its applications

Postby denis_berthier » Tue Nov 30, 2010 3:51 pm

The missing pages of this thread, lost due to the May 2009 crash, are available on my website:
http://www.carva.org/denis.berthier/HLS/SPF/CRR/index.html

Note 1: at the time I made this backup, it was for my private use only (I couldn't imagine the previous managers of the forum didn't make backups) and I didn't care about compatibility with browsers other than Safari on my Mac. It is therefore in the webarchive format. But it can be read most easily on Windows by first downloading Safari for Windows. For other ways of reading them, see the "real distribution of minimal puzzles" thread in the "general" section.

Note 2: I put these old Forum files online, as a historical reference, but a synthesis of all this has been available for a long time on my usual web pages for those who are not interested in details: http://www.carva.org/denis.berthier/HLS/index.html
denis_berthier
2010 Supporter
 
Posts: 4234
Joined: 19 June 2007
Location: Paris

Re: The concept of a RESOLUTION RULE and its applications

Postby JasonLion » Sat Mar 26, 2011 12:36 pm

Thanks to denis_berthier we now have PDF files of posts made to this topic between December 2009 and January 2010.

Page 22
Page 23
User avatar
JasonLion
2017 Supporter
 
Posts: 642
Joined: 25 October 2007
Location: Silver Spring, MD, USA

Previous

Return to Advanced solving techniques