The New Sudoku Players' Forum

[denis_berthier]

There are no CSP variables for uniqueness contradictions, which makes it impossible to write it as a whip.
However, much like in a whip[1].

Whips are not a hotpot where anything can be put in. Thats' what allows to develop some theory about them. The obvious counterpart is, not everything can be written as a whip. So, you're perfectly right that this cannot be written as a whip.
I've defined some extension of whips such as S-whips and W-whips (accepting resp. Subsets and other whips as inner right-linking objects), but I've never defined (and will never define) anything including uniqueness patterns. In my view, uniqueness has to be proven along resolution. I know this is a personal choice that no one has to accept.

it's a candidate causing an immediate conflict, ... I said what candidate it was and then described the contradiction.
I don't know what else I should have done...

You first said "otherwise 35 would be unresolvable in the rest of the grid". At that point, it was only T&E(XX).
Then, in a new post, you added "It looks like an extended UR"- which I didn't comment, because I know of no name for this extended pattern.

[Edit]: For fun, starting from the RS after Singles and whips[1]

Code: Select all

Resolution state after Singles and whips[1]:
   +----------------+----------------+----------------+
   ! 5    7    6    ! 8    2    1    ! 9    3    4    !
   ! 9    1    2    ! 7    3    4    ! 8    56   56   !
   ! 3    8    4    ! 69   5    69   ! 2    7    1    !
   +----------------+----------------+----------------+
   ! 8    356  9    ! 356  4    2    ! 7    1    356  !
   ! 4    356  7    ! 1    8    356  ! 35   2    9    !
   ! 2    356  1    ! 3569 7    3569 ! 4    56   8    !
   +----------------+----------------+----------------+
   ! 6    4    8    ! 35   1    7    ! 35   9    2    !
   ! 1    2    35   ! 4    9    35   ! 6    8    7    !
   ! 7    9    35   ! 2    6    8    ! 1    4    35   !
   +----------------+----------------+----------------+

I tried if n5r2c8 could be eliminated directly* by any of the chain rules in CSP-Rules (whips, braids, g-whips, g-braids...). The answer is no.

(*) this can be done with command : (try-to-eliminate-candidates (nrc-to-label 5 2 8))

[marek stefanik]

Whips are not a hotpot where anything can be put in.

I've never said they were. I only mentioned them after you had told me:

"if I suppose n5r2c8 is True, then I get a contradiction" ... is T&E

and I tried to avoid calling the pattern a whip, but I could have formulated it better.

You first said "otherwise 35 would be unresolvable in the rest of the grid". At that point, it was only T&E(XX).
Then, in a new post, you added "It looks like an extended UR"- which I didn't comment, because I know of no name for this extended pattern.

If the 3 were given anywhere else in the grid (we would have a 3 outside the UR but not inside), then "-35r2c8 (otherwise 35 would be unresolvable in r123c158)" would be imo a valid description of the extended UR. I don't see anything T&E-like in that logic.
In the second post I only rephrased it, using extended UR as a reference.

Now, there may be other ways of presenting your reasoning, e.g. as some chain, but this is not what you did.

Assuming chains have multiple inferences, I indeed did not. I only described it as one inference, since it only consists of one inference.

[Ngisa]

Code: Select all

+----------------+-------------------+-----------------+
| 5    7      6  | 8       2    1    | 9     3     4   |
| 9    1      2  | 7       3    4    | 8     56    56  |
| 3    8      4  |f69      5   g69   | 2     7     1   |
+----------------+-------------------+-----------------+
| 8    356    9  |e356     4    2    | 7     1    d356 |
| 4    356    7  | 1       8   h356  |c35^   2     9   |
| 2    356    1  | 3569    7    3569 | 4     56    8   |
+----------------+-------------------+-----------------+
| 6    4      8  |a35*     1    7    |b35    9     2   |
| 1    2      35 | 4       9    5-3  | 6     8     7   |
| 7    9      35 | 2       6    8    | 1     4     35  |
+----------------+-------------------+-----------------+


A Net
(3=5*)r7c4 - r7c7 = (5^-3)r5c7 = (3)r4c9 - (35*=6)r4c4 - r3c4 = (6)r3c6 - (65^=3)r5c6 => - 3r8c6; stte

Clement

[eleven]

Does anyone know what the technique is called?

3 and 5 are only given in band 1, therefore 5 cannot be in r2c8, creating a uniqueness pattern.

Code: Select all

 *-------------------------------------------------------*
 | *5  7     6    |  8      2  1      |  9   *3    4     |
 |  9  1     2    |  7     *3  4      |  8   -5    .     |
 | *3  8     4    |  .     *5  .      |  2    7    1     |
 |----------------+-------------------+------------------|

This is called a reverse BUG, e.g. see here.

[eleven]

Not solving it, but another approach:

Code: Select all

 *-------------------------------------------------------*
 |  5  7     6    |  8      2  1      |  9    3    4     |
 |  9  1     2    |  7      3  4      |  8    56   56    |
 |  3  8     4    |  69     5  69     |  2    7    1     |
 |----------------+-------------------+------------------|
 |  8  356   9    | #356    4  2      |  7    1    356   |
 |  4  356   7    |  1      8 #356    | A35   2    9     |
 |  2  356   1    | #359-6  7  359-6  |  4    56   8     |
 |----------------+-------------------+------------------|
 |  6  4     8    | A35     1  7      | B35   9    2     |
 |  1  2     35   |  4      9  35     |  6    8    7     |
 |  7  9     35   |  2      6  8      |  1    4    35    |
 *-------------------------------------------------------*

3 and 5 cannot be both in r4c4, r5c6 and r6c4 (one is both in r7c4 and r5c7)
=> 6 and 9 must be there, r6c4=9, -6r6c6

[marek stefanik]

...or we could say that 35 can only appear two times each in the whole thing. Nice find!

I'm wondering, does this count as an Exocet?
base 35r7c7, target r5c2, cross-lines 35r5c4, cover-houses 35b5 => -6r5c2

It's interesting that the MSLS with fish links provides different eliminations than the Exocet(?), even though we then reach the same state with singles.

[Cenoman]

In one step, with two almost S-Wings:

Code: Select all

 +------------------+----------------------+-------------------+
 |  5    7     6    |   8      2    1      |  9     3    4     |
 |  9    1     2    |   7      3    4      |  8     56   56    |
 |  3    8     4    |   69*    5    69*    |  2     7    1     |
 +------------------+----------------------+-------------------+
 |  8    356   9    |CBa356#   4    2      |  7     1   C356#  |
 |  4    356   7    |   1      8 Acb356^   |Cc35^#  2    9     |
 |  2    356   1    |   3569*  7    3569*  |  4     56   8     |
 +------------------+----------------------+-------------------+
 |  6    4     8    | Cc35^#   1    7      |Cc5-3^ #9    2     |
 |  1    2     35   |   4      9   c35^    |  6     8    7     |
 |  7    9     35   |   2      6    8      |  1     4    35    |
 +------------------+----------------------+-------------------+

UR(69)r36c46 using externals:
(6)r4c4 - r5c6 = [(3)r7c4 = r8c6 - (3=*5)r5c6 - r5c7 = (5)r7c7] (^)
(6)r5c6 - r4c4 = [(3)r5c7 = r4c9 - (3=*5)r4c4 - r7c4 = (5)r7c7] (#)
--------------
=> -3 r7c7; ste

[eleven]

I'm wondering, does this count as an Exocet?
base 35r7c7, target r5c2, cross-lines 35r5c4, cover-houses 35b5 => -6r5c2

Never seen that kind of single cell exocet. I don't think, that the Exocet inventors would count it as such (or look for it).

[RSW]

There are actually four unproven exocets that lead to a singles solution:
(3569)r4c23, r6c4 r5c7 => -3r4c4 -356r6c4 -6r4c2 -69r6c6
(359)r5c79, r4c3 r6c6 => -3r6c2 -3r5c26 -3r4c49 -356r6c4 -56r4c2 -569r6c6
(456)r6c78, r5c1 r4c4 => -36r5c2 -36r4c4 -5r6c246 -5r4c29 -5r5c67
(235)r79c4, r1c5 r6c6 => -3r46c4 -3r58c6 -569r6c6

When enabled, my solver attempts to prove these exocets by demonstrating that all converse combinations lead to contradiction. This proof succeeds with all but the first first one in the above list. However, I'm not convinced that the logic of these "proofs" is correct, and need to do more work on it.

[marek stefanik]

From what I've seen, every junior exocet has a MSLS companion (some senior exocets are tricky, they seem to only reduce to rank1 even with fish links) and vice versa (if we count these as exocets).

I'm now going through the old threads looking for ideas and it seems that the two base cells didn't always use to be a requirement.
Here champagne briefly mentions something similar:

base one cell 2 digits

but there is no example provided (maybe I will find one later on in the thread).

I'm assuming that they were established later on when trying to reduce the T&E then associated with exocets. Similarly the exocet(?) in Hanabi is not really considered an exocet by today's standards (and I haven't found anything similar in the old threads, either) due to its split-up base, but the logic seems identical to me.

There are actually four unproven exocets that lead to a singles solution

The first and third example cannot be proven using single digits, so even though there could be an elegant proof, I don't have much to say about them.

The second and fourth are actually equivalent. We can simplify them to:
Br5c7, Tr6c6 (cross-'lines' r7b5, cover-houses 35c4) => -69r6c6
Br7c4, Tr6c6 (cross-'lines' c7b5, cover-houses 35r5) => -69r6c6
Together with mine they are all equivalent to eleven's MSLS, but these two even provide the same eliminations directly.

Your solver then goes on to prove 3 the true base digit, as the puzzle either solves or produces a contradiction with singles only.

[RSW]

even though there could be an elegant proof

My work on proving exocets began after a conversation on another forum that suggested a proof could be quite straightforward. As I looked deeper into this, I concluded that the original premise was flawed. The proof would require the evaluation of a very large number of base/target combinations, and was not the slightest bit elegant. At that point I lost interest in it. Someday, I'll look at it again, but there are more interesting things to pursue first.

[denis_berthier]

even though there could be an elegant proof

My work on proving exocets began after a conversation on another forum that suggested a proof could be quite straightforward. As I looked deeper into this, I concluded that the original premise was flawed. The proof would require the evaluation of a very large number of base/target combinations, and was not the slightest bit elegant. At that point I lost interest in it. Someday, I'll look at it again, but there are more interesting things to pursue first.

This summarises the whole story about exocets.
It started as a remark by champagne that some "pattern" appeared often in puzzles considered by Allan Barker. The "pattern" was never really defined, only a few relations between some candidates were supposed to hold and for the rest, a contradiction was proven by "the program". As any candidate that is not in the solution is contradictory with the givens, this amounted to saying nothing.

Some exocets got the real status of a resolution rule when David P. Bird provided a full definition of J-Exocets. Needless to say, their coverage was much smaller than the largely undefined "pattern" over-promoted by champagne, and a lot of work ensued to try and generalise them.
That's when I lost any interest in exocets: David's J-Exocets are already a complex pattern. If one needs hundreds of different generalisations to make them effective*, no one will ever try to find them in a puzzle.

(*) As I've shown here http://forum.enjoysudoku.com/pattern-based-constraint-satisfaction-2nd-edition-t32567.html#p303970, J-Exocets (plus other exotic patterns) cannot change any of the ratings in a collection of 21,375 controlled-bias puzzles, meaning they are essentially useless, except possibly for the hardest puzzles (those not in T&E(1)).

[marek stefanik]

David's J-Exocets are already a complex pattern.

Indeed they are, but they are also quite easy to spot manually. Most of the time I can spot them more quickly than singles.

If one needs hundreds of different generalisations to make them effective...

So far I was able to prove every exocet I've seen (except for those that require multiple digits to be proven) just by adding one cross-line and one cover-house. That seems easy enough.

To add an example, this one is the only exocet I've seen that YZF_Sudoku misses:
98.7..6..5...8..4...3.2...84.........6...72.....26...3.9..7.8....59.8.2.........1
(it's the first puzzle posted here by Danny (daj95376))

(after eliminating 9r46 by pointing candidates/whip[1])
1345r46c6, r1c5, r8c5 => -1r1c5, -34r8c5, -1r12379c6

345 use r157c5 as cross-lines and b8 + 2 columns as cover-houses.
This is itself enough to prove 1 a true base digit and eliminate it from the target, or we can give it c5 as a cross-line and get the exocet described above.

I am assuming that YZF_Sudoku just dismisses it as a senior exocet because it thinks that an exocet in one stack would be found as a JE (which does not account for a 'cross'-line that does not cross the stack but is entirely contained in it).

When writing this post I realised that according to my understanding this exocet should not be rank0, yet it is and there is a corresponding MSLS, but the fish links come from endofinned fishes and are very complex (and r5c5 is used twice). This can be applied to every other exocet I assumed not to be rank0.

So unless there is another family of exocets that I don't know of, every exocet that can be proven using singular digits (true in base and false in all targets => contra. with that digit only) is rank0 with fish links.

[denis_berthier]

David's J-Exocets are already a complex pattern.

they are also quite easy to spot manually. Most of the time I can spot them more quickly than singles.

The main claim is probably the

If one needs hundreds of different generalisations to make them effective...

So far I was able to prove every exocet I've seen (except for those that require multiple digits to be proven) just by adding one cross-line and one cover-house. That seems easy enough.

The question is, can you define such additional structure or such modifications of the standard J-Exocet in a way totally independent of the context or do you have an ad hoc proof each time? As for me, I've never seen any consistent definition of exocets as a pattern beyond David's.

[marek stefanik]

The only difference between senior and junior exocet is that JE only considers basic fishes while SE considers mutant fishes as well.
A consistent definition would therefore rely on mutant fishes. If you consider fishes in general valid patterns, then it's possible.

The cross-lines are easily identifiable due to either an excessive number of non-base givens contained or crossing the box which contains the base.
The cover-houses are apparent once the cross-lines have been identified, one just needs to count them.

Examples with one base cell (or any unusual count) or split-up base can be defined in the same manner, however, in the latter a digit could end up occupying more than one base cell, which has to be accounted for.
This part can be tricky, as only if a digit appears in the base enough times to be forced into a target, it is considered to be a true base digit. Other occurences can be seen as reducing the number of base cells (and thus the number of targets alowed).

All of that can be defined very easily with fish links (base + n cross-lines have to be covered by an n-link and the targets), but the way JEs have been being proven for years is much simpler and can be generalised as described above.