How do ARs Arise?

Everything about Sudoku that doesn't fit in one of the other sections

Re: How do ARs Arise?

Postby denis_berthier » Tue May 07, 2013 5:42 pm

eleven wrote:"Simple fish" only include x-wing, swordfish (and maybe jellyfish ?). Those can only eliminate none or at least 2 of the UR candidates, the latter destroying the pattern (see blues' proof).

OK, that's an interesting point.

I wonder how David selected his set of rules in such a way that a very specific property they own is necessary to prove the result.
And I wonder also which kind of more general proof he was expecting.

If you find the kite counter-example for a real 1-solution puzzle, I'm still interested.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Re: How do ARs Arise?

Postby eleven » Tue May 07, 2013 9:03 pm

denis_berthier wrote:If you find the kite counter-example for a real 1-solution puzzle, I'm still interested.

Sorry, i didn't find it, and i will not try to find another one, because i stopped my sudoku programming activities. But if you have any doubts, that one exists, you are invited to try to disprove it.
eleven
 
Posts: 1582
Joined: 10 February 2008

Re: How do ARs Arise?

Postby ronk » Tue May 07, 2013 11:22 pm

eleven wrote:... it is clear, that it is possible, that a kite bites one of the UR candidates out ...

Since a kite makes a single exclusion, this is clear to me as well.
ronk
2012 Supporter
 
Posts: 4764
Joined: 02 November 2005
Location: Southeastern USA

Kite --> AR example

Postby blue » Wed May 08, 2013 1:49 am

Here's an example.

Code: Select all
..968..14....1........25.6.6.4...15.....6..2.59.....3.3.18.....4..15..8.....7....

+-----------------+-----------+--------------+
| 27   35    9    | 6   8  37 | 257   1  4   |
| 278  356   56   | 4   1  37 | 2578  9  25  |
| 1    4     78   | 9   2  5  | 3     6  78  |
+-----------------+-----------+--------------+
| 6    278   4    | 27  3  89 | 1     5  789 |
| 78   1     3    | 5   6  89 | 4     2  789 |
| 5    9     278  | 27  4  1  | 78    3  6   |
+-----------------+-----------+--------------+
| 3    256   1    | 8   9  4  | 256   7  25  |
| 4    267   267  | 1   5  26 | 9     8  3   |
| 9    2568  2568 | 3   7  26 | 256   4  1   |
+-----------------+-----------+--------------+

Kite: 8r5c1 = 8r2c1 - 8r3c3 = 8r3c9 => r5c9<>8
AR: 89r45c69 => 7r45c9 => r3c9<>7; stte
blue
 
Posts: 573
Joined: 11 March 2013

Re: How do ARs Arise?

Postby blue » Wed May 08, 2013 2:29 am

denis_berthier wrote:And I wonder also which kind of more general proof he was expecting.

I didn't post anything about this, but on further reflection, it turned out that there is a very easy proof for the following: if the pencil marks for a puzzle, contain an embeded minimal BUG pattern, and the BUG pattern has solutions (and so, being minimal, has exactly two solutions) ... then every "rank-0" pattern that justifies the elimination of a candidate from either solution, justifies the elimination of at least one candidate from each solution.

For the proof, I considered a "rank-0" pattern, to be defined by a "base/cover" problem -- not necessarily a "single digit" problem -- that satisfies the "construction rule" from the opening post of Obi-Wahn's thread, About the arithmetic of Ultimate Fish, and has "fin sector count" equal to zero (i.e. an equal number of base and cover sectors). The eliminations that it justifies, are those specified in his "exclusion rule".

In other words: N base and N cover sectors are given. Base sectors can overlap. The the list of base sectors is allowed to contain duplicates, and the list of cover sectors is allowed to contains duplicates, and (although it's pointless), a base sector can also be a cover sector. The construction rule requires that each candidate occurs in at least as many cover as base sectors. The exclusion rule (in this case), states that any candidate that occurs in more cover than base sectors, can be eliminated.

Standard patterns of that type, include: hidden and naked N-tuples, unfinned N-fish (including "simple fish"), line/box eliminations, "continuous nice loops", grouped or ungrouped "continuous loop" AICs, SK-loops and variants, Su-de-Coq, and (?) more. "Line of sight" eliminations that follow as singles are placed, are also included, since they can be done as "one base, one cover sector" eliminations before the single is placed.

Note: Obi-Wahn's thread was short on proofs, and it's an amazing thing (to me), but I only just now realized that (at least in the opening post), his patterns were restricted to being "single digit" patterns. His assertions remain valid, even for
"non-single-digit" base/cover problems. If anyone is interested in proofs, we can open a thread on it, or continue in Obi-Wahn's thread.

For Denis and logel: Obi-Wahn's principle, extended to non-single-digit problems, as far as I know, is the most general case, where a single base\cover proof, can be given, and the valildity of the resulting eliminations, can be "easily verified" -- i.e. it's quick and easy, to verify that the "construction rule" is satisfied, and that the target candidate(s) satisfy the "exclusion rule".

"Hats off" to Obi-Wahn -- well done :!:

Blue.
Last edited by blue on Fri Jun 21, 2013 2:21 am, edited 2 times in total.
blue
 
Posts: 573
Joined: 11 March 2013

Re: How do ARs Arise?

Postby denis_berthier » Wed May 08, 2013 5:56 am

Hi Blue,

Thanks for your detailed answer. Yes, Obi-Whan has done a very good job. BTW, you too, with your proof at the start of this thread and the last one about rank 0.

Without much thinking about it, I suggested to use constructivist arguments in response to David's request for a general proof of his conjecture (and of a possibly broader one); but on second thoughts, there is no general reason why a sequence of constructive steps wouldn't lead to a situation where a non constructive rule can be applied.

I was on the verge of thinking to myself: can however a sequence of constructive steps lead to a situation where only a non constructive rule can be applied? But I hold the thought:
- that's trivially false for 1-solution puzzles: any (known) puzzle can be solved by B-braids (and probably even by B7-braids) and the property of stability for confluence of B-braids (or B7-braids) implies that this remains true for a partially solved puzzle;
- that's trivially true for multi-solution puzzles: at best a solution can be written as "[P0 and (Q1 or Q2 or ...)]" or as "[(P0 and Q1) or (P0 and Q2) or ...]", where P0 is the part common to all the solutions. But no constructive theory can prove such a formula without proving one of the (P0 or Qi). This may be very counter-intuitive for people not familiar with constructive/intuitionnistic logic in which (A or not A) is not an axiom, but that's among the basics (so, please everybody, don't shoot before checking the information in any textbook on constructive/intuitionnistic logic). In intuitive (in the natural language meaning of "intuitive") terms, this means that a constructive/intuitionnistic proof of "A or B" must be a constructive/intuitionnistic proof or A or a constructive/intuitionnistic proof of B.

This makes me think that I've forgotten to write an obvious consequence of my results with B-braids: any well-formed puzzle can be solved in a constructive pattern-based way without using uniqueness or any ARs. I had no counter-example but it seems also that there was no proof before.
Note (in order to prevent a flood of personal opinions on the use of such techniques): this is a theoretical result. It doesn't imply that:
- there may not be a "simpler" solution using them,
- even if there is no simpler solution using them, one should avoid them: anyone is free to use whatever they want.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Re: How do ARs Arise?

Postby David P Bird » Wed May 08, 2013 8:27 am

Thanks everybody, I'm learning things from these exchanges!

Denis Berthier wrote:This may be very counter-intuitive for people not familiar with constructive/intuitionnistic logic in which (A or not A) is not an axiom, but that's among the basics (so, please everybody, don't shoot before checking the information in any textbook on constructive/intuitionnistic logic). In intuitive (in the natural language meaning of "intuitive") terms, this means that a constructive/intuitionnistic proof of "A or B" must be a constructive/intuitionnistic proof or A or a constructive/intuitionnistic proof of B.

Yup as a non-mathematician I'm a member!

I was therefore ignorant that Resolution Theory was not all embracing, and couldn't provide a "neat high level theorem" to prove my conjecture. I had thought that the "one given per UA" composing constraint could be handled in the same way as the "one per cell, one per house" constraints that composers must also abide by.

The reason I specified the elementary methods that I did was because those are the ones everyone performs before they get down to some serious solving. My experiences showed me that was too soon to be including a scan for looking for Avoidable Patterns, but I wondered when that time would be and how it could be focused on particular cells following certain types of enabling eliminations.

Thinking about it afresh, it now seems to me that any eliminations that would apply to all the cells in a mini-line if they were occupied are non-starters as enablers and this will include those from subset and chain methods alike.

Particular thanks to Blue for his excellent contributions and I must now explore Obi-Whan's thread he references.

David
David P Bird
2010 Supporter
 
Posts: 960
Joined: 16 September 2008
Location: Middle England

Re: How do ARs Arise?

Postby denis_berthier » Wed May 08, 2013 9:12 am

David P Bird wrote:I was therefore ignorant that Resolution Theory was not all embracing

There is no Resolution Theory, there are Resolution Theories (depending on which set of rules you adopt). As they share a common conceptual framework, maybe you consider this as Resolution Theory - well, why not?.
In any case, sorry, you won't be able to deduce String Theory from any Resolution Theory.


David P Bird wrote:I had thought that the "one given per UA" composing constraint could be handled in the same way as the "one per cell, one per house" constraints that composers must also abide by.

I only know 4 constraints ("one per cell, one per house", as you call them).
All the rest (including any resolution rule) is elaboration of these and I would in no case speak of constraints; at best, they are "derived constraints"; of course, this also applies to any "one given per UA" rule.
Some of these elaborations are based on non-constructive proofs.
Whether you accept them in a resolution theory has nothing to do with "all embracing", it is only a matter of personal choice. As I said already, I can decide to activate e.g. UR1.1 in SudoRules, thus implicitly putting it in some resolution theory.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Re: How do ARs Arise?

Postby denis_berthier » Wed May 08, 2013 9:32 am

This may not be directly related to this thread, but is there any exhaustive list of UAs or any estimate of their number (modulo isomorphisms) ?
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Postby Afmob » Wed May 08, 2013 10:59 am

In this thread you can find all unavoidables up to size 9. There might be some other threads were more UA are listed.
Afmob
 
Posts: 130
Joined: 28 June 2011

Re:

Postby denis_berthier » Wed May 08, 2013 3:51 pm

Afmob wrote:In this thread you can find all unavoidables up to size 9. There might be some other threads were more UA are listed.

Thanks, Afmob. I had a quick look. There seems to be huge numbers of possibilities.
denis_berthier
2010 Supporter
 
Posts: 1253
Joined: 19 June 2007
Location: Paris

Previous

Return to General