JExocet Pattern Definition

Advanced methods and approaches for solving Sudoku puzzles

Re: JExocet Pattern Defintion

Postby denis_berthier » Thu May 09, 2013 5:07 am

This is a copy of (part of) David's introductory post, with the slight modifications I would bring to it in order to eliminate any ambiguity.
I deal only with JExocet, leaving the JE+ extension and daj's additional eliminations for later.
I hope we can agree on a final definition, at least for this core case.
Remark: I replaced "base candidate" by "base digit" because what we generally call a candidate is a <cell, digit> pair.


JEXOCET DEFINITION

Conditions on the Pattern of Cells

Code: Select all
  *-------*-------*-------*
  | B B . | . . . | . . . |  B = Base Cell Pair, in the Base Row and the Base Block/Box
  | . . . | Q . . | R . . |   
  | . . . | Q . . | R . . |  Q = 1st Object Cell Pair
  *-------*-------*-------*  R = 2nd Object Cell Pair
  | . . S | S . . | S . . |       
  | . . S | S . . | S . . |  S = Cross-line Cells     
  | . . S | S . . | S . . |   
  *-------*-------*-------*  . = Any candidates (including base digits)
  | . . S | S . . | S . . | 
  | . . S | S . . | S . . |     
  | . . S | S . . | S . . |   
  *-------*-------*-------*

The Base Cell Pair (B) and the two Object Cell Pairs (Q and R) occur in three different blocks/boxes in the same band (the JE band).
The three "cross-lines" intersect this band as shown, passing through the Object Cell Pairs but not through the Base Cells.


Conditions on candidates

1) No base cell is decided.
Each base cell may have up to 4 candidates, but together, they contain exactly 3 or 4 digits (called the base digits).

2) Each Object Cell Pair is made of two cells: the target cell and the companion cell
Each target cell contains at least one base digit (plus possibly non-base digits)
Companion cells contain no base digit

3) For each base digit, there are two units/houses containing/covering all its occurrences in the S cells (be it as a candidate or as a decided value).



JEXOCET RULE

Theorem: if a JExocet is present in some resolution state, then its non-base digits can be eliminated from its target cells.


PROOF OF THE JEXOCET RULE

Let a and b be the (unknown) true values of the two base cells. By the rules of Sudoku, each of a and b must be the value of a cell in each of the three "cross-lines" containing the S cells.
But condition 3 entails that each of a and b can be the value of at most two S cells. Therefore (as neither a nor b can be in the Base Row or the Base Block anywhere outside the B Cells) each of a and b must also be the value of one of the Q or one of the R cells.
By condition 2, each of a and b must therefore be the value of the Q or the R target cell.
We have thus proven that the values of the two target cells are the same as those of the two base cells.
We don't know these values, but this is enough to exclude any non base digit from the target cells.



Remark: the cardinality of the set of base digits didn't play any role in the proof.
Last edited by denis_berthier on Sun May 19, 2013 12:40 pm, edited 8 times in total.
denis_berthier
2010 Supporter
 
Posts: 3972
Joined: 19 June 2007
Location: Paris

Re: JExocet Pattern Defintion

Postby denis_berthier » Thu May 09, 2013 7:57 am

blue wrote:If you were presenting me with a solution path for a puzzle, in an attempt to convince me that it only had one solution, and I was trying to verify its correctness, and at one point, you said "these cells satisfy the exocet property, and so these candidates can be eliminated", and I said: "OK, I buy that the candidates can be eliminated if the exocet property is satisfied -- prove to me that it's satisfied". At that point, the amount of text (or talk) that you would need to provide, could be quite large in the general case. On the other hand, if you knew that a JExocet pattern was associated with the cells, you could say: "Do you know about the unsatisfiability of Nx(N-1) base cover problems, and thier connection with the exocet property ? Yes ? OK, you can see the Nx(N-1) problems here, here and here" ... pointing out the instance for each base cell digit. I would be convinced, and we would move on.

Does what I said, really matter ? From the other side, you could say: "Look at this program that I wrote, to check for valid permutations. Do you belive that it functions correctly ? Yes ? When I run it against this PM state, for each digit, it answers back that there are no valid permutations after the relevant items have been forced. Run it yourself, if you don't believe me."
It's difficult to know what to say at that point. If I don't run the program, then I haven't really verified your solution path. If I do run it, then every execution step, somehow becomes part of the verification, and the number of execution steps, is on the order of the size of the "large amount of text (or talk)" that we would hope to avoid.


I think there's a fundamental difference between the two situations.

In the JExocet case (as for any resolution rule), you can refer to a "mathematical" theorem (the JExocet rule), proven once and for all. The JExocet pattern is defined in a purely factual, descriptive, non procedural, way - as in any resolution rule. You only have to exhibit it in the current PM and you get your eliminations for free.

In the Exocet case, you have to check all the relevant truth assignments in each particular situation. There's no generality, nothing that you can state once and for all (no elimination that would result only from the presence of this partial pattern). What there is is a partial pattern indicating the possibility that there might be something interesting to look for; elsewhere, I called this a heuristic. I don't mean that it cannot be useful (in addition to being the starting point for defining real full patterns), but it is certainly not what I would call a pattern, as long as, in addition to seeing it, you need some computer or some hard brain work to make complicated calculations.


By saying that the difference is fundamental, I mean in particular that it is not mainly one of complexity, as you seem to be suggesting (though it is not totally unrelated to it and I find your comments on complexity interesting).
When you refer to a theorem, it doesn't matter how hard its proof may have been. Whether the Fermat-Wiles theorem was really proven by Fermat in just a little more space than the margin of his Diophantus book (very unlikely) or whether it needed about three and a half centuries and a few thousand pages to be proven, it is no less true (provided that Wiles' proof is sound and you accept the Axiom of Choice).
Moreover, accepting it as true doesn't depend only on whether you are able to read the proof or not (only a few tens of people are currently able to read it). There is much more scientific "knowledge" that we accept as such (recalling that "knowledge" in science is always relative) on the basis of its global acceptance by the scientific community than we could ever check by ourselves. After all, I've never seen my DNA but I have little doubt about having some (it'd be harder for me to think that DNA is an invention of CIA for some obscure goal).
Of course, such questions don't arise for JExocet (or for any known resolution rule) - the proof is almost obvious, even without any knowledge of cover sets.


This discussion arose here, but it is also relevant to logel's tentative definition of a general "elimination pattern".
denis_berthier
2010 Supporter
 
Posts: 3972
Joined: 19 June 2007
Location: Paris

Re: JExocet Pattern Defintion

Postby champagne » Thu May 09, 2013 9:07 am

Hi blue,

blue wrote:Hi champagne,
champagne wrote:For me, the pattern is like a theorem. My code looks for the pattern and does not do any permutation (in that process).

For this part:
My code looks for the pattern and does not do any permutation (in that process).



I have the feeling that you are mixing the 2 cases;
I don't use the permutations when looking for JEXOCETS. Reversely, I have a permutation process to detect non JEXOCETS patterns.

blue wrote:I got a very nice speedup, by solving the puzzle beforehand, and looking only at cases where the base and target pairs, actually contain the same pair of (distinct) digits in the solution.


very good idea.I keep it in mind and will do the same. My first reaction would be "what about twin exocets"


blue wrote:
4) setting the base to true and the targets to false lead to a reasonable number of permutations

This number is actually zero, is it not ?
Do you mean a reasonable number of "partially competed permutations, that are obviously impossible to complete" ?


The correct wording would be

if it is not the searched pattern you can stop at the first valid permutation
and as you say , if it is the pattern you have a reasonable number of "partially competed permutations",

For the remaining part of the post, as I never entered (and don't plane to do in the near future) higher sizes I have no comment

regards

champagne
champagne
2017 Supporter
 
Posts: 7355
Joined: 02 August 2007
Location: France Brittany

Re: JExocet Pattern Defintion

Postby daj95376 » Thu May 09, 2013 10:09 am

[Edit: Withdrawn]
Last edited by daj95376 on Thu May 09, 2013 8:22 pm, edited 3 times in total.
daj95376
2014 Supporter
 
Posts: 2624
Joined: 15 May 2006

Re: JExocet Pattern Defintion

Postby David P Bird » Thu May 09, 2013 10:35 am

Denis, many thanks for your efforts.

It's clear that different contributors speak Sudoku in different dialects which makes penning definitions and descriptions awkward, but no more so than in our conversations in everyday life. Provided the terms in different dialects are fit for purpose and aren't ambiguous, there should be no loss of clarity, although readers may be irritated by the dialect used in any particular piece. I therefore consider that there is no need to write such things as "units/houses" in our work here.

To give one example, for several years I've been calling a row of boxes a 'tier' and a column of boxes a 'stack' which has allowed me to use a 'band' of boxes as being either a tier or a stack in the same way that a line of cells means either a row or column of them. This avoids having to use clumsy phrasing such as 'chute or tower depending on the orientation'. From their reactions, I believe that other contributors have been able to accept this as part of my dialect. Of course if I were ever to write a book I would have to provide a glossary of my terms.

Now to specifics:

I accept referring to base digits rather than base candidates and your reasoning behind it.

Denis Berthier wrote:Conditions on candidates

1) No base cell is decided.
Each base cell may have up to 4 candidates, but together, they contain only digits (called the base digits) taken from a set of cardinality 3 or 4: {a, b, c (and d)}

2) Each Object Cell Pair is made of two cells: the target cell and the companion cell
Each target cell contains at least one target digit (plus possibly non-target digits)
Companion cells contain no target digit

3) For each target digit, there are two units/houses (different from the cross-lines) containing/covering all its occurrences in the S cells (be it as a candidate or as a decided value).

Remark: the units/houses may be rows or blocks (in case of the above graphics), resp. columns or blocs (in case the graphics is rotated).

Here you've switched from using base candidates in (1) to target digits in (2) and (3)

I don't see 1) as being much of an improvement on the original
1) The base cells must be restricted to a set of three or four digits (the base candidates)
I also consider the reference to cardinality to be a big turn-off for the majority of readers, and in the light of your closing remarks a bit of over-kill.

2) I can accept

3) Is neater but I consider that "(different from the cross lines)" is not a condition. When a cross line is also a containing house the partial sword fish degenerates into a partial X-wing but it makes no difference to the truth counts.

If the examples are provided, the remark should be unnecessary.

I like your Proof of the JExocet Rule - I always suspected that mine could be improved. I would only want to change your word order in some places.

Generally the way JExocet pattern is defined and proved should pave the way for the JE+ definition and proof, so it would be best to wait until that is covered too before anything is finally decided. This is one of the reasons I posted my piece on partial fish – the other is that it may open the door to other single band inference patterns that could be used in combination with them.
David P Bird
2010 Supporter
 
Posts: 1043
Joined: 16 September 2008
Location: Middle England

Re: JExocet Pattern Defintion

Postby blue » Thu May 09, 2013 2:08 pm

Hi champagne,

champagne wrote:I have the feeling that you are mixing the 2 cases;
I don't use the permutations when looking for JEXOCETS. Reversely, I have a permutation process to detect non JEXOCETS patterns.

Correct. When you said "pattern", I didn't read "JEXOCET pattern".

champagne wrote:
blue wrote:I got a very nice speedup, by solving the puzzle beforehand, and looking only at cases where the base and target pairs, actually contain the same pair of (distinct) digits in the solution.


very good idea.I keep it in mind and will do the same. My first reaction would be "what about twin exocets"

I don't look for twins, specifically. I only find both, when they exist.

champagne wrote:
blue wrote:
4) setting the base to true and the targets to false lead to a reasonable number of permutations

This number is actually zero, is it not ?
Do you mean a reasonable number of "partially competed permutations, that are obviously impossible to complete" ?


The correct wording would be

if it is not the searched pattern you can stop at the first valid permutation
and as you say , if it is the pattern you have a reasonable number of "partially competed permutations",

Right. I should have said that it's zero or one, in the search for valid instances, and some number of "partially completed permutations" in both cases.

Regards,
Blue.
blue
 
Posts: 979
Joined: 11 March 2013

Re: JExocet Pattern Defintion

Postby denis_berthier » Thu May 09, 2013 2:54 pm

David P Bird wrote:Here you've switched from using base candidates in (1) to target digits in (2) and (3)

I don't see 1) as being much of an improvement on the original

3) Is neater but I consider that "(different from the cross lines)" is not a condition. When a cross line is also a containing house the partial sword fish degenerates into a partial X-wing but it makes no difference to the truth counts.

If the examples are provided, the remark should be unnecessary.


I made a few corrections along these lines.


When I said I wanted a final definition, I didn't mean one that couldn't be re-formulated into an equivalent form. I only meant one on the meaning of which everybody agrees.
Last edited by denis_berthier on Thu May 09, 2013 3:41 pm, edited 1 time in total.
denis_berthier
2010 Supporter
 
Posts: 3972
Joined: 19 June 2007
Location: Paris

Re: JExocet Pattern Defintion

Postby blue » Thu May 09, 2013 3:40 pm

Hi Denis,

denis_berthier wrote:I think there's a fundamental difference between the two situations.

In the JExocet case (as for any resolution rule), you can refer to a "mathematical" theorem (the JExocet rule), proven once and for all.

(...)

By saying that the difference is fundamental, I mean in particular that it is not mainly one of complexity, as you seem to be suggesting (though it is not totally unrelated to it and I find your comments on complexity interesting).
When you refer to a theorem, it doesn't matter how hard its proof may have been.

(...)

I understand, but I would add one caution.

If an "exocet property" has been verified by computer, you could list the cells, and refer to "Theorem Exocet-X-B-T" ... "certainly provable, and in fact just proved by my computer" ... where X represents the PM state and B and T are the base and target specifications. An odd twist.

If you want to say that that sort of thing is inapproriate ... and I do want to say that ... then it seems like the thing to do, is to note that there are an infinite number of theorems like that, not all proven (of course), and introduce the idea that the solution paths may to refer (without proof), to only a finite number of pre-designated theorems. Any other theorem used to support the validity of the path, would be required to have a supporting proof included. With that, the complexity issue re-surfaces, and requiring that proofs for the pre-designated theorems be included as well, wouldn't change the complexity analysis.

denis_berthier wrote:This discussion arose here, but it is also relevant to logel's tentative definition of a general "elimination pattern".

Exactly.

If it could be shown that not-necessarily-minimal instances of the "pattern", could be verified in polynomial time in the puzzle size, it would follow that (P = NP).
If it could be shown that minimal instances of the "pattern" ("his patterns"), could be verified in polynomial time in the puzzle size, it would follow that (Co-NP = NP).

You may be familiar with this, but ...

Co-NP is the class of decision problems that ask the complementary question for an NP problem. The (NP-complete) sudoku problem, asks "does this puzzle have a solution ?". The associated (Co-NP-complete) problem, asks "is this a puzzle with no solution ?". (Co-NP = NP) would follow from (P = NP), if it were true, and people have tried (with no luck) to prove that Co-NP and NP are distinct. If that could be shown, it would follow that P and NP are distinct. People who believe in (P = NP), have presumably tried proving that (Co-NP = NP), since it would be provide "supporting evidence" for the (P = NP) conjecture. Like the (P = NP) conjecture, it hasn't been proven one way or another (to my knowledge).

Regards,
Blue.
blue
 
Posts: 979
Joined: 11 March 2013

Re: JExocet Pattern Defintion

Postby denis_berthier » Fri May 10, 2013 5:24 am

blue wrote:If you want to say that that sort of thing is inapproriate ... and I do want to say that ... then it seems like the thing to do, is to note that there are an infinite number of theorems like that, not all proven (of course), and introduce the idea that the solution paths may to refer (without proof), to only a finite number of pre-designated theorems. Any other theorem used to support the validity of the path, would be required to have a supporting proof included. With that, the complexity issue re-surfaces, and requiring that proofs for the pre-designated theorems be included as well, wouldn't change the complexity analysis.

Complexity analysis has probably some part to play in saying that "that sort of thing is inappropriate". But I think there is also some non formalisable aspect, something that revolves around the ideas that a theorem has to have some meaning for us or that a proof has to be elegant/beautiful. A mathematician is not a theorem prover; he is first a kind of visionary (I'm thinking of some of our local people: Schwartz, Neveu, Thom, Grothendiek; you probably have yours also); and, when acting as a theorem prover, he doesn't work like a formal one.
Another way of putting it is, a "theorem" in the sense of formal logic (i.e. a formula proven to be true) - e.g. the "infinite number of theorems like that" you are mentioning - would in most cases not qualify as a theorem in the usual sense.


denis_berthier wrote:If it could be shown that not-necessarily-minimal instances of the "pattern", could be verified in polynomial time in the puzzle size, it would follow that (P = NP).
If it could be shown that minimal instances of the "pattern" ("his patterns"), could be verified in polynomial time in the puzzle size, it would follow that (Co-NP = NP).

Yes, but... would you engage in such an adventure?


denis_berthier wrote:Like the (P = NP) conjecture, it hasn't been proven one way or another (to my knowledge).

Oh no. If it had been settled, you'd see it in all the newspapers.

BTW, the conjecture is not P = NP, but P <> NP. From a formal POV, it may seem to be the same thing. But, in practice, a vast majority of people dealing with it believe that NP <> P. [OK, maths isn't a matter of polling].
From my experience with classification in Sudoku[9] (instances becoming extremely harder as they become extremely rarer) and a brief look into larger ones, I have the feeling that as size increases, the possibilities for such worst cases increase almost exponentially. Of course, this feeling may be wrong, but that's enough for deterring me from trying to prove P=NP.
As for proving P<>NP, it's a lifetime job and I'll keep it for some future life if any - but not the next, nor even the second next; there are so many other things I'd like to do before! Indeed, if I had to work on this, what'd I'd probably try to prove is not P<>NP, but that it is undecidable.
denis_berthier
2010 Supporter
 
Posts: 3972
Joined: 19 June 2007
Location: Paris

Re: JExocet Pattern Defintion

Postby David P Bird » Fri May 10, 2013 7:51 am

Denis Berthier wrote: When I said I wanted a final definition, I didn't mean one that couldn't be re-formulated into an equivalent form. I only meant one on the meaning of which everybody agrees.

No worries then as you have satisfied yourself that you understand the JExocet pattern and therefore I suppose the JE+ pattern. I also appreciate you've got other fish to fry at the moment.

If and when you turn to daj's case, twin JExocets and ABI loops I'll be interested in you’re your reactions. I don't consider either daj's case or ABI loops fully qualify as patterns. Twin JExocets are very powerful though. The multiple eliminations they provide arise from combining the inferences provided by different parts of the pattern in different ways.

I feel rather out of place anyway as I'm the only manual solver here and will only accept branching when it's confined to recognisable patterns. So I'll hold this topic in abeyance for now and turn to frying other fish as well.
David P Bird
2010 Supporter
 
Posts: 1043
Joined: 16 September 2008
Location: Middle England

Re: JExocet Pattern Defintion

Postby denis_berthier » Fri May 10, 2013 8:33 am

David P Bird wrote:I don't consider either daj's case or ABI loops fully qualify as patterns.


I don't know what an abi loop is, but if it's some of the stuff that can only be defined via some obscure procedure, I don't even want to know.
denis_berthier
2010 Supporter
 
Posts: 3972
Joined: 19 June 2007
Location: Paris

Re: JExocet Pattern Defintion

Postby David P Bird » Fri May 10, 2013 8:56 am

denis_berthier wrote:
David P Bird wrote:I don't consider either daj's case or ABI loops fully qualify as patterns.

I don't know what an abi loop is, but if it's some of the stuff that can only be defined via some obscure procedure, I don't even want to know.

They're a way to reduce the possible pairings of the base digits that can be true that champagne uses. He can describe them better than me.
David P Bird
2010 Supporter
 
Posts: 1043
Joined: 16 September 2008
Location: Middle England

Re: JExocet Pattern Defintion

Postby denis_berthier » Fri May 10, 2013 9:01 am

David P Bird wrote:I feel rather out of place anyway as I'm the only manual solver here.

I don't think the discussion with Blue about what can be called a pattern is really alien to your POV as a manual player. Probably you will accept fewer patterns than can be defined by factual/descriptive/logical/non-procedural conditions only, but I'm quite certain that you wouldn't accept more.
denis_berthier
2010 Supporter
 
Posts: 3972
Joined: 19 June 2007
Location: Paris

Re: JExocet Pattern Defintion

Postby champagne » Fri May 10, 2013 10:13 am

David P Bird wrote:
denis_berthier wrote:
David P Bird wrote:I don't consider either daj's case or ABI loops fully qualify as patterns.

I don't know what an abi loop is, but if it's some of the stuff that can only be defined via some obscure procedure, I don't even want to know.

They're a way to reduce the possible pairings of the base digits that can be true that champagne uses. He can describe them better than me.


the "abi loop" is a clear process, nothing "obscure", but it uses the uniqueness property, so Denis is not interested anyway
champagne
2017 Supporter
 
Posts: 7355
Joined: 02 August 2007
Location: France Brittany

Re: JExocet Pattern Defintion

Postby denis_berthier » Fri May 10, 2013 10:37 am

champagne wrote:the "abi loop" is a clear process

First reason for not being interested, if it can only be described as a process, i.e. a procedure.

champagne wrote:but it uses the uniqueness property, so Denis is not interested anyway

Right
denis_berthier
2010 Supporter
 
Posts: 3972
Joined: 19 June 2007
Location: Paris

Next

Return to Advanced solving techniques