The New Sudoku Players' Forum

[denis_berthier]

"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.

[eleven]

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.

[ronk]

... 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.

[blue]

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]

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.

[denis_berthier]

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.

[David P Bird]

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

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

[denis_berthier]

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.

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]

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) ?

[Afmob]

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

[denis_berthier]

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.