Abominable TRIAL-and-ERROR and lovely BRAIDS

Advanced methods and approaches for solving Sudoku puzzles

Abominable TRIAL-and-ERROR and lovely BRAIDS

Postby denis_berthier » Tue Oct 14, 2008 10:32 pm



Abominable T&E


Immediately after guessing, Trial-and-Error (T&E) is usually considered as the abomination in Sudoku.

But my new T&E theorem obliges us to take a closer look at it.
I first posted this theorem here: http://forum.enjoysudoku.com/viewtopic.php?t=5591&postdays=0&postorder=asc&start=150, because I found it while I was studying nrczt-chains and their nrczt-braid generalisation, but, as I now have much more to say about it and in order to avoid a confusion between chains and braids, I think it should become an independent topic.

To keep this thread as self contained as possible, let me recall the main results and definitions.

The starting point for everything here is the above mentioned theorem, which definitely answers a very old open question:

T&E theorem: ANY ELIMINATION DONE BY T&E CAN BE DONE BY AN NRCZT-BRAID.

The full proof is given in the above thread.
Moreover, the proof shows how the braid able to do the same elimination can be obtained constructively from the trace of the T&E procedure.

Corollary: ANY PUZZLE SOLVABLE BY T&E IS SOLVABLE BY NRCZT-BRAIDS.

As nrczt-braids are perfectly respectable patterns, this theorem means that the usual opposition between T&E and pattern-based solutions is very tenuous - but it keeps some reality, as we shall see later.


Let me recall the general definition of T&E (parameterised by a resolution theory T, i.e. by a fixed set of resolution rules):

Definition: Given a resolution theory T (i.e. a set of resolution rules) and a candidate z, T&E(T, z) is the following resolution technique:
- start an auxiliary grid by copying the current PM; in this auxiliary grid, delete z as a candidate and add it as a decided value; apply to this auxiliary PM all the rules in T until quiescence;
- if a contradiction is thus obtained in this auxiliary PM, then eliminate z from the original one; if no contradiction is obtained, then merely go back to the original PM.


I think this is what everyone means by "using T&E(T) to eliminate candidate z".
Notice that no "guessing" is allowed: if a solution is found in the auxiliary PM, it is merely forgotten.

If T = ECP + NS + HS (Elementary Constraint Propagation rules + rules for Singles), then we put T&E = T&E(ECP+NS+HS).

Definition: Given a resolution theory T, T&E(T) is the following resolution technique (this is only conceptual, any implementation should optimise this):
a) define phase = 1;
b) apply all the rules in T;
c) set changed-PM = false; mark all the remaining candidates as "not tried";
d) if there is at least one "not-tried" candidate, then choose any of them, say z; apply T&E(T, z); if it eliminates z, then set changed-PM = true and apply all the rules in T, otherwise un-mark z; in both cases, goto d;
e) if there is no not-tried candidate:
----------- if changed-PM = true, then set phase = phase +1 and goto c);
----------- if changed-PM = false, then stop.
Said otherwise, repeat T&E(T, z) for all the candidates z, as long as any one remains, until quiescence.


Notice that this procedure allows considering the same candidate z several times.
This is reasonable, because any elimination of another candidate z' by T&E(T, z') may entail a new possibility of a contradiction appearing in a new application of T&E(T, z).
This is also necessary if one wants the result of this procedure to be independent of the order in which the candidates are tried.



To be complete, let me recall also the general definition of an nrczt-braid:
Definition: an nrczt-braid of length n for a target z is a sequence of candidates L1, R1, L2, R2, .... Ln-1, Rn-1, Ln, alternatively called left-linking and right-linking, such that:
- for any 1<= k <= n, Lk is nrc-linked to the target or to a previous right-linking candidate (some Ri, for i < k);
- for any 1 <= k < n, Lk and Rk are in some well defined rc, rn, cn or bn cell (which entails they are nrc-linked) such that each of the other candidates in this cell is nrc-linked to the target or to a previous right-linking candidate; Rk itself is not nrc-linked to any of these;
- in at least one of the four rc, rn, cn or bn cells containing Ln, each of the other candidates is nrc-linked to the target or to a previous right-linking candidate.

and the associated:
nrczt-braid elimination theorem: given an nrczt-braid, its target can be eliminated.
Proof: exactly the same as for nrczt-whips, following the total ordering of the candidates, until the last left-linking candidate, with no compatible right-linking one, is reached. The proof shows progressively that, if the target was true, then all the left-linking candidates would be false and all the right-linking candidates would be true.


The purpose of this thread is to explore some consequences of the above T&E theorem and of some of its extensions (part of which are already mentioned in the above thread).
Last edited by denis_berthier on Mon Oct 20, 2008 7:47 pm, edited 1 time in total.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby denis_berthier » Tue Oct 14, 2008 11:06 pm


The scope of T&E or (equivalently) of nrczt-braids (concrete results)


The results reported here were already present in this page: http://forum.enjoysudoku.com/viewtopic.php?t=5591&postdays=0&postorder=asc&start=150
But as they are essential for this thread, I copy them here. Next post will give new results.

1) Random collections
All the 10,000 minimal puzzles in my sudogen0 collection randomly generated by suexg are solvable by braids; that's no fresh news, as they were already all solvable by the simpler nrczt-whips (chains and lassos if you prefer the old style).

I've therefore tested 1,000,000 minimal puzzles generated with the suexg generator: all of them are solvable by nrczt-braids.
Open question: are all of them solvable by nrczt-whips (as is the case for the first 10,000)? It would be too long to check directly with SudoRules.


2) Relationship with the Sudoku Explainer rating (SER)
We know that puzzles with high SER are very rare and are difficult to obtain with a random generator. I therefore tried another collection biased towards high SER.
We already knew that nrczt-whips can solve almost any puzzle upto SER 9.3 and some puzzles at SER 9.4.
With braids, we can go a little further. Computations on gsf's collection of 8152 hardest show that:
- nrczt-braids can solve almost any puzzle in it upto SER 9.8;
- the proportion of solvable puzzles decreases as SER increases upto 10.2.
Additional results on this collection forthcoming.


3) Experimental results for T&E(B-NRCZT)

I've already shown that almost all the puzzles can be solved by ordinary T&R or, equivalently, by braids. Let's now concentrate on the hardest.

Using the equivalence between T&E(B-NRCZT) and T&E(ECP+NS+HS, 2) [i.e. T&E at depth 2 pruned by only ECP, NS and HS], which is an obvious corollary of my T&E theorem, I obtain the following experimental results.

[/b]All the known puzzles can be solved by T&E(B-NRCZT), i.e. by T&E at depth one (a single hypothesis at a time) pruned by rules for nrczt-braids.[/b]

Some time ago, I conjectured that any puzzle could be solved at depth one of T&E if nrczt-whips were used to prune the search; and I showed that this was true for EasterMonster.
I still don't know whether this conjecture is true.
But if we take braids instead of whips, then it becomes experimentally true (I have no formal proof though).

This result can be formulated in a different, though equivalent, form:

Any of the known puzzles can be solved by ECP+NS+HS or by ordinary T&E or by ordinary T&E iterated to depth 2 (i.e. considering 2 hypotheses at a time).
Notice that I have no formal proof that there can't be a puzzle that requires T&E at depth 3. But if such cases existed, they would be utterly rare.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby denis_berthier » Tue Oct 14, 2008 11:10 pm


Backdoor-size vs depth of T&E


In the previous post, I've recalled that all the known puzzles can be solved with T&E(ECP+NS+HS, d) where:
- d = 0, no T&E <==> solvable by NS+HS
- d = 1, one hypothesis at a time <==> solvable by nrczt-braids
- d = 2, two hypotheses at a time <==> solvable by T&E(nrczt-braids), i.e. with only one level of T&E pruned by nrczt-braids.

Two intrinsic constants can be associated with any puzzle:
- its (NS+HS)-backdoor size b: b= 0, 1, 2 or 3 for all the known puzzles;
- the depth of T&E(ECP+NS+HS) necessary to solve it: d= 0, 1 or 2 for all the known puzzles.
A natural question is: is there a relationship between b and d?

The answer is not obvious because the backdoor-size is based on guessing (without the constraint of having to justify the elimination of other candidates in the same rc- rn- cn- or bn- cells as the backdoors), whereas depth of T&E is based on proving contradictions in hypotheses.
None of the relations d ≤ b or b ≤ d is obvious.


------------------

d ≤ b? If a puzzle can be solved by T&E at depth d, it doesn't mean that one can choose d hypotheses to generate all the auxiliary grids necessary to the T&E procedure. But I currently have no counter-example to d ≤ b.

Notice that, if we consider gsf's FN-1 list of 1,183 puzzles with NS+HS backdoor-size 1 (b=1) or his list FN-2 of 28,948 puzzles with NS+HS backdoor-size 2 (b=2), all of them can be solved by ordinary T&E (d=1).


------------------

For b ≤ d, it is easy to find counter-examples.

If we consider gsf's list FN-2 of 28,948 puzzles with (NS+HS) backdoor-size 2 (b=2), all of them can be solved by ordinary T&E (d=1).

------------------

Even for b ≤ d+1, there are counter-examples.
If we consider gsf's list of 14 puzzles with (NS+HS) backdoor-size 3 (b=3) (AFAIK, the only such puzzles known as of today), with their names taken from gsf's hardest list and their SER (new version) computed:
Code: Select all
100000002090400050006000700050903000000070000000850040700000600030009080002000001 Easter-Monster  SER= 11.6
900000005040300060002000100080740000000020000000806070100000900030007040005000002 tarek-ultra-0300 SER= 11.3
700000004020600010005000800030910000000050000000203090800000700060009020004000005 tarek-ultra-0301 SER= 11.3
100000089000009102000000400007600000030040000900002005004070000500008010060300000 tarek-4/08 SER= 11.5
100000002003400050060000700000890040000306000009040000020000100700000006005080030 jpf-04/14/08 SER= 11.2
500000003020600010008000900040701000000030000000420070900000500010007020003000008 tarek-ultra-0302 SER= 11.2
100000002003400050060000700000050040000301000008940000020000100700000006005090030 jpf-04-10 SER= 11.2
100000006020500040003000700040850000000010000000024080007000300050009020600000001 coloin SER= 11.3
100000006020500040003000700040890000000204000000015080007000300050009020600000001 coloin-05/11/01 SER= 11.4
001000200030000040500030006000107000040000080000902000300000008060050030002000700 ocean-2007-05-29-1 SER= 9.4
300000200000540000000600000102003000000000064800000000090700050000000108050060000 gfroyle-2007-05-30-4 SER= 3.6
080090000300000060000300040000010005002000900007000800650000100000207000000004000 gfroyle-2007-05-30-3 SER= 4.2
000020580040300000010000000000600071500000200000400000200059000000000306700000000 gfroyle-2007-05-30-2 SER= 5.7
000500001308000000400003000000610000900000800000050000060700020010000300000000490 gfroyle-2007-05-30-1 SER= 6.6

then four of them can be solved by ordinary T&E (d=1):
#10 (SER= 9.4), #11 (SER=3.6), #12 (SER= 4.2), #13 (SER= 5.7) and #14 (SER= 6.6).
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby aran » Wed Oct 15, 2008 7:34 am

Denis
Immediately after guessing, Trial-and-Error (T&E) is usually considered as the abomination in Sudoku.

But my new T&E theorem obliges us to take a closer look at it.

T&E theorem: ANY ELIMINATION DONE BY T&E CAN BE DONE BY AN NRCZT-BRAID.


We know already that any T&E elimination can be re-presented as an "orthodox" elimination : for example transporting/"krakening" from all the candidates in the cell "emptied" by the
decided
candidate z will necessarily prove z false.

So it seems to me that your theorem does not per se reopen the debate (if it was ever closed, I mean)
aran
 
Posts: 334
Joined: 02 March 2007

Postby denis_berthier » Wed Oct 15, 2008 9:25 am

aran wrote:We know already that any T&E elimination can be re-presented as an "orthodox" elimination : for example transporting/"krakening" from all the candidates in the cell "emptied" by the
decided
candidate z will necessarily prove z false.

Transporing what? Krakening what? That sounds like procedures, not like a well defined resolution rule.

Can you name a well defined pattern that can be used in every case to replace a T&E elimination?

That's what my theorem allows: the pattern in question is an nrczt-braid.

If you claim that another pattern is able to do the same thing, then you'll have to prove it or give references.

If such a pattern existed, it would have to be a very recent one, because Ruud, who has been the moderator here, on Eureka and on the Sudoku programmer's forum for years and who read everything, was the one to ask me one year ago if I could replace T&E by one single rule.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby ronk » Wed Oct 15, 2008 9:41 am

denis_berthier wrote:Can you name a well defined pattern that can be used in every case to replace a T&E elimination?

That's what my theorem allows: the pattern in question is an nrczt-braid.

But but but ... your nrczt-braid rule essentially is T&E, so what's your point.
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

Postby denis_berthier » Wed Oct 15, 2008 9:59 am

ronk wrote:But but but ... your nrczt-braid rule essentially is T&E, so what's your point.

I was expecting something like that.

An nrczt-braid is a well defined pattern, the (currently) most general of a whole family of previously defined patterns , none of which were enough to replace T&E (indeed, I didn't even consider this question - I found this equivalence by mere chance).
The nrczt-braid rule is a resolution rule. T&E is an algorithm. Saying the 2 are the same thing is therefore meaningless.
My theorem allows to replace a T&E procedure by a pattern-based elimination. That's new. Or, if the equivalence is so obvious, whereas the question has been pending for so long, why didn't you or anyone else come out with this pattern long ago?

Do you have any other pattern to propose for this?
Do you have any other theory T that such T&E(T) is equivalent to any other pattern?
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby aran » Wed Oct 15, 2008 10:08 am

Denis wrote
the proof shows how the braid able to do the same elimination can be obtained constructively from the trace of the T&E procedure.

In similar vein, one can write a proof for any T&E elimination by "constructively" using those "traces" as follows :
let Z be the T&E candidate
call the logic resulting from Z true : f(Z).
let C be the empty cell resulting from f(Z).
call the candidates in C X1.....X9 (where several of those may be 0)
then
f(Z) empties C=>f(Z) places X1.....X9 in cells C1....C9 external to C and which "see" C.
Now transport from each of the candidates in C ie examine the Strong Inference Set (X1....X9) in C (=Krakening)
then X1 true=>X1 in C1 false=>Z false (by reversal of the original f(Z) chain placing X1).
and so on for all X2......X9.
Hence Z false.
aran
 
Posts: 334
Joined: 02 March 2007

Postby denis_berthier » Wed Oct 15, 2008 10:51 am

aran wrote:one can write a proof for any T&E elimination by "constructively" using those "traces" as follows :
let Z be the T&E candidate
call the logic resulting from Z true : f(Z).
let C be the empty cell resulting from f(Z).
call the candidates in C X1.....X9 (where several of those may be 0)
then
f(Z) empties C=>f(Z) places X1.....X9 in cells C1....C9 external to C and which "see" C.
Now transport from each of the candidates in C ie examine the Strong Inference Set (X1....X9) in C (=Krakening)
then X1 true=>X1 in C1 false=>Z false (by reversal of the original f(Z) chain placing X1).
and so on for all X2......X9.
Hence Z false.

Once more, you're describing a procedure, not a pattern.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby aran » Thu Oct 16, 2008 2:38 am

Denis
Once more, you're describing a procedure, not a pattern.

Subtle nuances.
A simple enough procedure v a complicated enough pattern ?
aran
 
Posts: 334
Joined: 02 March 2007

Postby denis_berthier » Thu Oct 16, 2008 2:44 am

aran wrote:Denis
Once more, you're describing a procedure, not a pattern.

Subtle nuances.

It is not a subtle nuance, but a major error in categories. A procedure is not a resolution rule (i.e. a logical formula) exactly in the same way as an animal is not a vegetable.

aran wrote:A simple enough procedure v a complicated enough pattern ?

No: a well defined pattern (a relatively simple one for a net) vs a mostly undefined procedure.

The problem is, you make a general claim about being able to replace any application of T&E by a pattern and you don't even know which pattern.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby aran » Thu Oct 16, 2008 3:27 am

Denis
The problem is, you make a general claim about being able to replace any application of T&E by a pattern and you don't even know which pattern.

Your pattern is not recognisable ab initio.
It is dependent on the contradiction and its path.
You can't look at the grid and say "there's my pattern" until you know all about the route taken by the T&E.
So is that a "pattern" in any useful sense of the word ?
I can define my procedure in one line and prove it as a general theorem in six :
every elimination found by T&E can be expressed as a discontinuous loop.
So it does have a name.

an animal is not a vegetable
...perhaps...but some carnivores are plants

aran
 
Posts: 334
Joined: 02 March 2007

Postby denis_berthier » Thu Oct 16, 2008 3:43 am

aran wrote:Denis
The problem is, you make a general claim about being able to replace any application of T&E by a pattern and you don't even know which pattern.

Your pattern is not recognisable ab initio.
It is dependent on the contradiction and its path.
You can't look at the grid and say "there's my pattern" until you know all about the route taken by the T&E.
So is that a "pattern" in any useful sense of the word ?
I can define my procedure in one line and prove it as a general theorem in six :
every elimination found by T&E can be expressed as a discontinuous loop.
So it does have a name.

Putting a name on something that is not a pattern doesn't transform it into a pattern.
You're still unable to define your suposed pattern in any purely logical way - which all this is about.

No pattern is recognisable ab initio. You always have to look for them. If your level as a player is Naked Pairs, then braids will look very hard for you. Here, we are discussing exceptionally hard puzzles, which require exceptionally hard patterns.
It is now obvious that you mix everything and you don't know the basic definitions necessary to understand what I'm saying here.
As you're a newcomer, I suggest you read the definitions I gave in the first posts of the "concept of a resolution rule" thread.
This being said, if you're happy with your procedure and you don't want to learn anything new, it isn't a problem for me.

aran wrote:
an animal is not a vegetable
...perhaps...but some carnivores are plants

Very funny. You would be very appreciated on Eureka.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby aran » Thu Oct 16, 2008 4:19 am

Denis
Recognisable pattern : when challenged DB resorts to his well-worn procedure :
1. you don't understand
2. I am an authority
3. go away.

Juvenile really !
aran
 
Posts: 334
Joined: 02 March 2007

Postby denis_berthier » Thu Oct 16, 2008 4:54 am

aran wrote:when challenged DB

The problem is I'm not the one challenged here.
You can play all the Eureka bickerings you want, that won't change facts: you haven't provided any pattern to support your claims.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Next

Return to Advanced solving techniques