more on whips, braids, T&E...

Advanced methods and approaches for solving Sudoku puzzles

Re: more on whips, braids, T&E...

Postby denis_berthier » Sat Apr 16, 2011 7:07 am

ronk wrote:
denis_berthier wrote:As for the techniques SE uses in the puzzles rated above ~8 (which was the main question raised by my post), I'd like to believe I'm the only one that doesn't understand what all its types of "forcing chains" are (this is what is at stakes in the 8-12 range). But I fear I'm not. Even after scanning the whole SE cloning thread, I couldn't find any definition of them (nor any claim that they were clearly understood by anyone). At least, there was a positive result for me: I lost most of my initial interest in trying to understand them.

I don't think the "SE cloning thread" ever got as far along as the "forcing chains", so how you can comment about what anyone there understands is beyond me.

It's true that there's not much in that thread about "forcing chains" but I saw a few indications that some participants had had a look at them. I can't tell how much time they spent on them.
I was not commenting about "what anyone understands" (I can see in nobody's mind - not even always in mine), but about the easily checkable absence of any definition and any claim of understanding them. What I remember is something by Paul more or less assimilating "dynamic forcing chains" with T&E (sorry, I don't remember his exact wording, I didn't keep the precise reference and the thread is too long for me to check it in the very little time I have for Sudoku).

Of course, I'd like to be wrong. If anyone could provide a definition (in English or in pseudo-code) of the different types of forcing chains and of the notion of "node" they use, it would certainly be a great step in understanding the upper part of SER.
Moreover, if the overall goal of that thread remains to code a faster clone or almost-clone of SER, shouldn't the hardest (and most time consuming) techniques be considered first (as was already suggested in that thread) or at least in parallel with the easy ones?
Sure, if such a clone existed and was largely accepted, I'd use it instead of SE.

But, as I said previously, I'd be much more interested in a radically new rater including modern techniques (even if this can only be a longer term goal). For ALS or AIC addicts, I can't imagine they wouldn't like to have them taken into consideration in the ratings. In this context, my interest for the various "forcing chains" (in the SE sense) was (and would still be if we had a clear definition of them): where do they stand in the landscape (among ALS chains, AICs of all kinds, whips, g-whips, braids, generalised whips and braids)?
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: more on whips, braids, T&E...

Postby David P Bird » Sat Apr 16, 2011 10:32 am

Denis Berthier wrote:If anyone could provide a definition (in English or in pseudo-code) of the different types of forcing chains and of the notion of "node" they use, it would certainly be a great step in understanding the upper part of SER.

I thought the meaning of "node" has always been fairly clear as being a set of candidates in a set of cells that can be considered to be Booleans that are true if they contain a requisite number of truths and false otherwise. So for example an ALS (abc=d)ABC represents two nodes and requires the notation conventions to be known to be interpreted.

My understanding of a forcing chain is one which must be read in one direction only. Hence if a starting node is assumed to have a truth state the states of the following ones will be known, but the reverse won't hold. I have no idea how SE categorises them beyond that, but I would class some of your chains as "accumulating forcing chains" in that they remember the states of previous nodes visited. For me they are equivalent to a restricted type of forcing net.

As I have a self-imposed discipline to only use bi-directional chains with every inference being stand-alone, I'm afraid I haven't been following the advancements you've made. However I allow myself to embed a range of recognisable patterns which, as you've previously pointed out, may involve proof by iterating cases. I've found it impossible to draw clear cut acceptance boundaries on these patterns though, and it is a matter I have open for periodic review.

So, although we're at opposite ends of the solving spectrum, SE suits neither of us. In my case it's because it resorts to employing forcing chains far too early because it misses opportunities to use combinations of embedded patterns – but that’s quite a coding challenge and one I'm not expecting to be undertaken.
David P Bird
2010 Supporter
 
Posts: 1043
Joined: 16 September 2008
Location: Middle England

Re: more on whips, braids, T&E...

Postby denis_berthier » Sat Apr 16, 2011 2:20 pm

David P Bird wrote:
Denis Berthier wrote:If anyone could provide a definition (in English or in pseudo-code) of the different types of forcing chains and of the notion of "node" they use, it would certainly be a great step in understanding the upper part of SER.

I thought the meaning of "node" has always been fairly clear as being a set of candidates in a set of cells that can be considered to be Booleans that are true if they contain a requisite number of truths and false otherwise. So for example an ALS (abc=d)ABC represents two nodes and requires the notation conventions to be known to be interpreted.

It seems that SE vocabulary doesn't always have the usual meaning, e.g. "forcing chain" doesn't mean the same thing in SE as in Sudopedia - so, maybe "node" in SE doesn't mean what I'd consider as a node. BTW, my definition of a node in a pattern is very simple: it is a 2D-cell (rc, rn, cn or bn cell) necessary to describe the pattern; it depends on no notation convention.

David P Bird wrote:My understanding of a forcing chain is one which must be read in one direction only.

In SE, there are also "bidirectional forcing chains" - I guess they are the same thing as basic AIcs (with no embedded subsets, nrc-chains in my terminology).

David P Bird wrote:I have no idea how SE categorises them beyond that,

That's my whole point about SE. I wonder if anyone has a clear idea of what all these types of "forcing chains" are.

David P Bird wrote:So, although we're at opposite ends of the solving spectrum, SE suits neither of us. In my case it's because it resorts to employing forcing chains far too early because it misses opportunities to use combinations of embedded patterns – but that’s quite a coding challenge and one I'm not expecting to be undertaken.

If this last sentence suggests that coding efficiently AICs with embedded subsets is difficult, I do agree. I had never looked closely at the computational complexity of these AICs, but it seems that the number of almost subsets of sizes n = 1, 2, 3, 4 increases very fast with n. When trying to combine them into AICs of increasing lengths, then the number of such combinations also increases very fast (exponentially with total length, I think). So that, finally, the computational complexity of AICs may not be better than that of nrczt-chains in spite of their reversibility.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: more on whips, braids, T&E...

Postby ronk » Sat Apr 16, 2011 4:52 pm

denis_berthier wrote:If anyone could provide a definition (in English or in pseudo-code) of the different types of forcing chains and of the notion of "node" they use, it would certainly be a great step in understanding the upper part of SER.

I agree the "SE clone" project has no written definitions for the forcing chains, Nicolaus Juillerat never provided any AFAIK. I believe PIsaacson and champagne are still working on it, so you should go over there and help them out. But don't expect a lot, we never even agreed on a definition for the project.

As for your commenting about what people do or do not understand, I stand by my prior statement.
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

Forcing whips and braids, a bad idea

Postby denis_berthier » Sun Apr 17, 2011 4:21 am


.

Maybe I should explain how I became interested in SE forcing chains. This will also explain why my sudden interest for this topic has now subsided.

1) Forcing chains a la sudopedia
All started with the definition of forcing chains I found in Sudopedia. Unfortunately, their server seems to have been down for some time now, and I can't reproduce their exact definition here (I'll add it later, when it works again).

According to sudopedia, there are two kinds of forcing chains, both starting with 2 candidates, say C1 and C2, in a bivalue/bilocal relationship.
Now the idea of forcing chains a la sudopedia can be generalised/refined in the following way. Consider any well defined type of chain/net, say W-chain (W for "whatever", not in reference to WXYZ-something), with alternating left- and right- linking candidates. Consider two W-chains, W1 starting with C1 as its potential target, and W2 starting with C2.
First kind of W-forcing-chain: if W1 and W2 have a common right-linking candidate C, then assert C as true.
Second kind of W-forcing-chain: if the last right-linking candidates of W1 and W2 are D1 and D2, and both D1 and D2 are nrc-linked to the same candidate C, then delete C.
The proof of both rules is obvious (reasoning by cases).
(The two types may be interverted in Sudopedia, I don't remember)

It is also easy to define the length of such a W-forcing-chain: if we want it to be compatible with the definition of length for W-chains, there's no choice, it has to be 1 + the sum of the lengths of its two components (the +1 is there for the C1-C2 bivalue/bilocal node).

First obvious observation: if W-chains are reversible, this definition doesn't allow more eliminations/assertions than the W-chains themselves.
The notion can therefore be interesting only when W-chains are not reversible, e.g. when we consider whips or braids.

Second observation: at first, it may seem that checking for W-forcing-chains shouldn't be too expensive as it requires "only" the combination of already found W-chains. Unfortunately, checking for W-forcing-chains of length n supposes that, for each C1-C2 bivalue/bilocal pair and each n, either you recompute or you keep in memory all combinations of W-chains of lengths p, q, with p+q+1=n. Finally, the computational complexity (time and/or memory) is very bad.

But we can still ask: is there any return on investment for this added complexity?
I tried again with my new version of SudoRules. I had already experimented with this long ago (for nrczt-chains) and found that it was very disappointing; I was therefore not expecting miracles. But, as the new version is faster and it needs less memory, I could run larger experiments on whips instead of the slightly less general nrczt-chains. But the results are still very bad. After trying 1,300+ puzzles, I found no case of a forcing-whip. (In these experiments, forcing-whips were given lower priority than whips of same length, but higher priority than whips of longer length).

2) Forcing chains in SE
Facing the above result and based only on the name of the hardest techniques used in SE (which I considered a blackbox), I wondered how SE could solve all the known puzzles. Was there in SE a smarter way to combine two chains, such that the combination more or less amounts to a second level of T&E? I now have the answer: no. "Forcing chain" in SE is not related in any way to "forcing chain" in sudopedia. The added power is not in "forcing chains" but in their "dynamic" forcing chains, which seem to implement a second level of T&E.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: Forcing whips and braids, a bad idea

Postby eleven » Sun Apr 17, 2011 9:50 am

Just could make a quick look at the last posts, because i dont have much time either. So dont take my comments too serious.

denis_berthier wrote:Moreover, if the overall goal of that thread remains to code a faster clone or almost-clone of SER, shouldn't the hardest (and most time consuming) techniques be considered first (as was already suggested in that thread) or at least in parallel with the easy ones?

Hehe, you are only number 3 after Red Ed and me to say that.
denis_berthier wrote:Facing the above result and based only on the name of the hardest techniques used in SE (which I considered a blackbox), I wondered how SE could solve all the known puzzles. Was there in SE a smarter way to combine two chains, such that the combination more or less amounts to a second level of T&E? I now have the answer: no. "Forcing chain" in SE is not related in any way to "forcing chain" in sudopedia. The added power is not in "forcing chains" but in their "dynamic" forcing chains, which seem to implement a second level of T&E.

I am no expert in SE techniques, but as i see it, it uses forcing chains as you described them above, including ones starting with more than 2 cells in a unit (e.g. all 3 cells, where a digit can be in a unit), and contradiction chains, which in fact are contradiction nets to eliminate the starting candidate, something you probably would call T&E(non chaining SE techniques,1). Since this does not solve the hardest, a second level was introduced. (I dont have the SE here for the names).
eleven
 
Posts: 3081
Joined: 10 February 2008

Re: Forcing whips and braids, a bad idea

Postby ronk » Sun Apr 17, 2011 11:56 am

eleven wrote:Just could make a quick look at the last posts, because i dont have much time either. So dont take my comments too serious.

denis_berthier wrote:Moreover, if the overall goal of that thread remains to code a faster clone or almost-clone of SER, shouldn't the hardest (and most time consuming) techniques be considered first (as was already suggested in that thread) or at least in parallel with the easy ones?

Hehe, you are only number 3 after Red Ed and me to say that.

Hehe, I agreed with Red Ed and solicited ideas on how to obtain pencilmarks from Explainer (at the point of the forcing chain) , so I count myself as number 2. ;)
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

re: "forcing chains" and "forcing nets"

Postby Pat » Sun Apr 17, 2011 2:30 pm

denis_berthier wrote:The only thing that seems clear to me is,
the expression "forcing chain" in SE
doesn't mean the same thing as in Sudopedia.

  • i'd say forget SuDoPedia,
    use the definitions given by Jeff (2006)

  • but in SuDoku Explainer,
    the term "Forcing Chains" is obviously given a wider definition
    and includes both
    • "forcing chains"
    • "forcing nets"
    (not that this will help with his sub-types---)
User avatar
Pat
 
Posts: 4056
Joined: 18 July 2005

Re: Forcing whips and braids, a bad idea

Postby denis_berthier » Sun Apr 17, 2011 3:54 pm

Thanks for your answers. They confirm my conclusion that "forcing chains" (à la sudopedia, à la SE and now also à la Jeff) don't allow by themselves to go beyond T&E(1).
As this was the reason for my interest in them, it closes the SE topic for me.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

re: "forcing chains" and "forcing nets"

Postby Pat » Wed Apr 20, 2011 7:13 am

Pat wrote:

  • in SuDoku Explainer,
    the term "Forcing Chains" is obviously given a wider definition
    and includes both
    • "forcing chains"
    • "forcing nets"


i should mention that his FAQ states,
    not implemented and not already covered by the implemented techniques --
    • Forcing nets (Forcing Chains with bifurcations)

but when his solution-path uses "Dynamic Forcing Chains",
his description will include this text --
The chains can be dynamic,
which means that the conclusions of multiple sub-chains must be combined in some cases.

so, his "Dynamic" is a "net" ( not a "chain" )
User avatar
Pat
 
Posts: 4056
Joined: 18 July 2005

re: T&E(2)

Postby Pat » Fri Apr 22, 2011 8:32 am

his FAQ also tells us something about the ratings --


  • 8.0 - 9.0: Cell/Region Forcing Chains
  • 8.5 - 9.5: Dynamic Forcing Chains
  • 9.0 - 10.0: Dynamic Forcing Chains (+)
  • > 9.5: Nested Forcing Chains

-- these Nested Forcing Chains do provide T&E(2)

    see examples rated 11.x

    Here's an example: (the 4 at the bottom are the Nested Forcing Chains type)
    SuDoku Explainer wrote:
      ///
      8 x Forcing Chain
      2 x Nishio Forcing Chains
      9 x Dynamic Contradiction Forcing Chains
      3 x Dynamic Region Forcing Chains
      1 x Dynamic Cell Forcing Chains
      1 x Dynamic Cell Forcing Chains (+)
      4 x Dynamic Contradiction Forcing Chains (+)
      4 x Dynamic Contradiction Forcing Chains (+ Forcing Chains)
      4 x Dynamic Contradiction Forcing Chains (+ Multiple Forcing Chains)
      3 x Dynamic Contradiction Forcing Chains (+ Dynamic Forcing Chains)
      1 x Dynamic Cell Forcing Chains (+ Dynamic Forcing Chains)
User avatar
Pat
 
Posts: 4056
Joined: 18 July 2005

Re: more on whips, braids, T&E...

Postby pjb » Sun Sep 11, 2011 2:41 pm

Regarding the puzzle: .............1.....123.456...........23...78..47.6.12...........318.764..58...23.
the solutions discussed here seem to be unnecessarily complicated, since following the basic moves (locked sets, sashimi swordfish followed by finned swordfish), standard POM analysis finds no less than 20 eliminations of 9's, following which the puzzle solves at once.
pjb
2014 Supporter
 
Posts: 2552
Joined: 11 September 2011
Location: Sydney, Australia

Postby Pat » Sun Sep 11, 2011 2:54 pm

pjb wrote:Regarding the puzzle
    .............1.....123.456...........23...78..47.6.12...........318.764..58...23.
the solutions discussed here seem to be unnecessarily complicated,
since following the basic moves (locked sets, sashimi swordfish followed by finned swordfish), standard POM analysis finds no less than 20 eliminations of 9's, following which the puzzle solves at once.

hi pjb,

Mauricio's puzzle is known to be a pure Jellyfish puzzle --
but denis_berthier is presumably looking for a different type of solution-path
User avatar
Pat
 
Posts: 4056
Joined: 18 July 2005

Re: more on whips, braids, T&E...

Postby denis_berthier » Sun Sep 11, 2011 5:20 pm

pjb wrote:Regarding the puzzle: .............1.....123.456...........23...78..47.6.12...........318.764..58...23.
the solutions discussed here seem to be unnecessarily complicated, since following the basic moves (locked sets, sashimi swordfish followed by finned swordfish), standard POM analysis finds no less than 20 eliminations of 9's, following which the puzzle solves at once.

Hi pjb,
If you read the 2nd post of this thread, where I introduced this example (taken from Mauricio), the first "normal" solution I give is with a Quad, a Jellyfish and 3 short simple chains. It seems much simpler than POM, at least to me.

As mentioned by Pat, my main purpose with this example is different. It is to show an exceptional case of non-subsumption of Fish by whips or braids; it is also to show the added power of g-whips, for which maximum size 4 is enough to solve the puzzle.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

CONSTRAINT RESOLUTION THEORIES

Postby denis_berthier » Thu Oct 06, 2011 12:39 am





CONSTRAINT RESOLUTION THEORIES



As I have mentioned long ago, most of what I have done for Sudoku can be generalised to any finite Constraint Satisfaction Problem (CSP). I have already given references to a few papers I've published on this topic. In the past few months and thanks to summer holidays, I had a little time to develop these ideas more extensively and in a more systematic way than can be done on a forum and I've now published a new book: "Constraint Resolution Theories" (CRT in the sequel) about advanced resolution rules meaningful for any CSP.

Details about CRT can be found on the part of my website dedicated to it: http://www.carva.org/denis.berthier/CRT/ (permanent URL).

The following chapters are available in pdf format:
- table of contents: http://www.carva.org/denis.berthier/CRT/ToC.pdf,
- introduction: http://www.carva.org/denis.berthier/CRT/ch01-Introduction.pdf,
- final remarks: http://www.carva.org/denis.berthier/CRT/ch12-Final-Remarks.pdf.

A third of CRT is about the application of the general theory to Sudoku; there are also examples from n-Queens to illustrate how whips or Subsets can look in a different CSP.

I've been striving to make an electronic version; but I'm still having some trouble with the epub format.



WARNING:
Being more general, the approach in this new book is also in some places more abstract and/or more formal than my previous book on Sudoku (HLS). In particular, it includes detailed proofs of confluence.
I tried to make it self-contained by introducing basics in logic. Also, the chapters on concrete resolution rules (whips, ...) can be read without reading those on formal logic and the general resolution framework. But self-containment is seldom a fully achievable goal.


For the readers of HLS or for those who have read my posts on this forum, here are a few indications about how CRT is related to HLS :

1) About the general framework

The general formal logic framework introduced in CRT, when applied to Sudoku, is globally the same as in HLS. Only two slight differences appear: I now use Gentzen’s “natural logic” instead of Hilbert’s axioms; and, when dealing with the resolution states (formerly called “knowledge states” in HLS), I refer to modal logic (the logic of necessitation) instead of epistemic logic (or logic of knowledge). None of these changes has any practical consequences; in particular, resolution theories should still be understood as theories in intuitionistic (or constructive) logic.
The definition of a resolution theory was slightly less precise in HLS.

But the main difference with HLS is that Sudoku is now considered as a CSP in a more systematic way than it was there; in particular:
- the cells in the Extended Sudoku Board are now explicitly interpreted as representations of CSP variables;
- the nrc notation introduced in HLS2 as a convenient way of representing chains/whips/braids, now appears as an obvious special case of a natural notation for any CSP;
- basic interactions (“pointing” and “claiming”) are systematically written as instances of whip[1];
- Subsets rules are first formulated in a general way, meaningful for any CSP, in terms of CSP variables and transversal sets, before being re-expressed for Sudoku in the usual terms of numbers, rows, columns and blocks; Naked, Hidden and Super-Hidden (Fish) Subsets are not only related by symmetry as they were in HLS; from the CSP point of view, they are now the very same rule, because the symmetries have been used at a higher level to introduce new CSP variables; (of course, this does not change anything for all practical purposes);
- the main change brought by this new perspective of Subsets is, it allows to introduce their “grouped” version (g-Subsets) as a natural generalisation (in the same way as several chain patterns have a grouped version) and to re-interpret the well-known Franken and Mutant Fish as g-Subsets.


2) New resolution rules and new ratings

For the parts of CRT specifically dedicated to the Sudoku CSP, they are very far from constituting a third edition of HLS (none of the examples, specialised versions of resolution rules or independence theorems present in HLS2 has been reproduced in CRT). Indeed, these parts start where HLS2 ended.
I first introduced most of the following patterns, resolution rules and/or topics (that were not in HLS2) on this Forum in 2008. But in CRT, most of them are now presented in the more general CSP framework (with a somewhat different, simpler terminology - see below):
- whips (which are a more synthetic view of both nrczt- chains and lassoes);
- braids, with a detailed proof of the confluence property of braid resolution theories;
- definition of the Trial-and-Error procedure (T&E) and proof of the “T&E vs braids” theorem;
- definition of the controlled bias generator; comparison of various kinds of generators; unbiased statistics for the W rating for a much larger sample than in HLS; [detailed numerical results about the number of puzzles solved by each type of rule had been given in HLS, but they were still based on the biased samples produced by the currently available generators];
- g-whips and g-braids; proofs of the associated confluence property and “gT&E vs g-braids” theorem;
- detailed subsumption theorems for whips and braids, showing that they capture “almost all” but not all the cases of Subset rules;
- Reversible Sp-chains, obtained by allowing the insertion of Subsets as right-linking objects in bivalue chains; proof that these chains are the same thing as grouped AICs or Nice Loops (but my definition does not involve the notion of a “restricted common”); proof of the confluence property for the associated resolution theories;
- Sp-whips and Sp-braids, obtained by allowing the insertion of Subsets as right-linking objects in whips and braids; proofs of the associated confluence property and “T&E(Sp) vs Sp-braids” theorem; analysis of their scope;
- gSp-Subsets, the “grouped” version of Subsets, a generalisation allowed by considering Subset patterns (Sp-subsets) from the general CSP point of view; they provide a new view of Franken and Mutant Fish;
- Reversible gSp-chains, gSp-whips and gSp-braids, obtained by allowing the insertion of g-Subsets of maximum size p as right-linking objects in bivalue chains, whips and braids;
- Wp-whips and Bp-braids, obtained by allowing the insertion of whips / braids of maximal length p as right-linking objects in whips / braids; proofs of the associated confluence property and “T&E(Bp) vs Bp-braids” theorem;
- relation of B-braids with T&E(2), providing a finite BB rating for all the known minimal puzzles (including the recent ones generated by eleven).



3) New terminology
With the introduction of rules with embedded patterns, the terminology I used in HLS and on this forum was becoming more and more cumbersome. Here are the correspondences between the new one and the old one. I write them only for whips; of course, there are similar ones for braids.

Patterns:
whips......nrczt-whips
g-whips......whips(BI)
Sp-whips......nrczt-whips(Subsets-p)
Wp-whips......nrczt-whips(Whips[p])

Ratings:
W......pure nrczt rating
gW......pure nrczt-whip(BI) rating
S......Subsets rating
S+W......nrczt rating
SpW......nrczt-whip(Sp) rating
WpW......nrczt-whip(Wp) rating
BB......nrczt-braid(nrczt-braid) rating
Last edited by denis_berthier on Sat Nov 05, 2011 10:31 am, edited 4 times in total.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

PreviousNext

Return to Advanced solving techniques