The New Sudoku Players' Forum

[champagne]

For Fata Morgana, it's possible to separately show r5c46=3 and r5c46=6, without depending upon an exocet.

in XSUDO the exocet is never explicit, but in your 2 diagrams, it is there.

The second point to stress is that both diagrams are using the extended XSUDO logic using AURs.

The basic logic can not conclude with only the floors 136.

The three ways to show the 2 eliminations are turning around the same underlying logic.

The final question is which one is the easiest to handle and to transpose to other puzzles.

In "abi"s logic, I would personally prefer the version with 2 chains, but "abi"s version with the loop seems to have a better potential for use in "nearly" exocets as Platinum Blonde

[ronk]

For Fata Morgana, it's possible to separately show r5c46=3 and r5c46=6, without depending upon an exocet.

in XSUDO the exocet is never explicit, but in your 2 diagrams, it is there.

Sorry, but r4c2 and r6c8 are not 0-rank covers, so my statement is correct. However, to satisfy your unexpected need for precision, I amended my statement.

The second point to stress is that both diagrams are using the extended XSUDO logic using AURs. The basic logic can not conclude with only the floors 136.

That's clear in the Xsudo logic set I provided, so what's your point?

The final question is which one is the easiest to handle and to transpose to other puzzles. In "abi"s logic, I would personally prefer the version with 2 chains, but "abi"s version with the loop seems to have a better potential for use in "nearly" exocets as Platinum Blonde

If true, Platinum Blonde would have been a better example.

BTW your "abi-loops" read as 0-rank loops, but I was not able to find such an animal in Xsudo, so I'm still doubtful of their validity. It's often dangerous to know the answer, making it easier to delude oneselve into believing a deduction is valid. Xsudo doesn't permit such delusions.

[champagne]

For Fata Morgana, it's possible to separately show r5c46=3 and r5c46=6, without depending upon an exocet.

in XSUDO the exocet is never explicit, but in your 2 diagrams, it is there.

Sorry, but r4c2 and r6c8 are not 0-rank covers, so my statement is correct. However, to satisfy your unexpected need for precision, I amended my statement.

BTW your "abi-loops" read as 0-rank loops, but I was not able to find such an animal in Xsudo, so I'm still doubtful of their validity. It's often dangerous to know the answer, making it easier to delude oneselve into believing a deduction is valid. Xsudo doesn't allow such delusions.

Some contradictions in that post.

You state that XSUDO is not using the exocet logic. I don't want to fight on that minor point.
But later you contest the "abi" logic just because you can not rebuild it in XSUDO.

1) "abi" logic uses intensively the exocet logic
2) Allan Barker has added late the AUR's logic, nothing proves that the program handles it correctly in all cases

You contest the validity of the loop which is strange.
Happily we have also a solution using simple AIC's? I am interested in knowing if you contest also the validity of them and why.

The logic used by "abi" is so simple that I have difficulties to think something can be wrong.
I checked and re checked it before using it and "abi" has shown she is highly reliable as far as logic is concerned.


It would be better to contest on precise logic facts.

the rest is not important

[David P Bird]

Hi champagne

I guess that which proof someone finds easiest to understand depends on the direction they are coming from.

In my case I'm using the arguments used in the development of the proof of the JExocet theorem which relies on condition 3 being satisfied.

A player familiar with that theorem wouldn't need to mark any individual cells – I just use row and column markers at the edge of the grid.

Checking out the 'simple clue' as you call it using abi's method, it is directly equivalent to my "quick check" using odd/even link counts in this puzzle. I therefore trust that it will be the same for others. I suppose that players will prefer the one they find easiest to remember.

I dislike splitting a problem into cases or using net based methods when solving, but am perfectly happy to do so when formulating theorems that provide inferences that a manual solver can apply. I'm far from sure if either abi's approach or mine could be classified as a traditional pattern* and would need to test them out over a range of puzzles.

* See <here> for some of my opinions on patterns.

DPB

[ronk]

in columns 2 and 8 we have outside the target of the exocet 1 ^ 3
This is clearly a strong link (exclusive or) since the target must have one of the digits.

3r2c2 ^ 1r9c2
1r1c8 ^ 3r9c8
...
we can now redo the inferred "abi" loop (a 100% standard AIC)

1r7c1 - 1r9c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = 3r9c8 - 3r7c7 = 1r7c1
...
so where is the problem???

The "problem" must be in these two derived strong inference sets ("sis") (highlighted in red). Please post this "abi loop" with each derived sis replaced with its corresponding native sis.

[champagne]

in columns 2 and 8 we have outside the target of the exocet 1 ^ 3
This is clearly a strong link (exclusive or) since the target must have one of the digits.

3r2c2 ^ 1r9c2
1r1c8 ^ 3r9c8
...
we can now redo the inferred "abi" loop (a 100% standard AIC)

1r7c1 - 1r9c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = 3r9c8 - 3r7c7 = 1r7c1
...
so where is the problem???

The "problem" must be in these two derived strong inference sets ("sis") (highlighted in red). Please post this "abi loop" with each derived sis replaced with its corresponding native sis.

3r2c2 ^ 1r9c2
1r1c8 ^ 3r9c8

these 2 strong links are "inferred" but "native".

BTW, they are also used in David's solution

Let me show in two ways how they can be defined as native.

the column 2 if 13r5c46 is reduced to

2467 2347 9 || 13 246 5 || 8 247 1247

and for digits 13 to

. 3 . || 13 . . ||. . 1

my trivial proof for the native strong inference 3r2c2 ^1r9c2 (as above)

Code: Select all

the cell r4c2 has one and only one of the digits 13
so one digit 13 (and only one) is somewhere in the column
giving 3r2c2 ^1r9c2


Assuming you could dislike it we can write, but it is exactly the same logic

Code: Select all

r2c12589 is an als
if 13r5c46 (and exocet effect in r4c2) that als has only 2 free digits 1 and 3
so 1r2c12589 ^3r2c12589
in our case, this is reduced to 3r2c2 ^1r9c2

BTW the logic is not requiring an exclusive OR.
the als provides anyway a simple OR .
In Platinum Blonde, as we will see, we have a simple OR

[ronk]

champagne, are you pulling my chain, or do you really not know the definition of a native strong inference?

[David P Bird]

I tested my alternative proof with Platinum Blonde

Code: Select all

 *----------------------*----------------------*----------------------*
 | 35678  34589  34679  | 4679   5689   4578   | 679 #  1      2      |
 | 15678  14589  4679   | 124679 125689 124578 | 679 #  56789  3      |
>| 15678  1589   2      | 3      15689  1578   | 4      56789  6789   | < 
 *----------------------*----------------------*----------------------*
>| 237    2349   1      | 8      236    234    | 23679  234679 5      | <
 | 235    6      349    | 124    7      12345  | 8      2349   149    |
 | 23578  23458  347    | 1246   12356  9      | 12367  23467  1467   |
 *----------------------*----------------------*----------------------*
>| 1236   123    8      | 5      1239   1237   | 123679 234679 14679  | <
 | 9      123    36     | 127    4      12378  | 5      23678  1678   |
 | 4      7      5      | 129    12389  6      | 1239   2389   189    |
 *----------------------*----------------------*----------------------*
   67     9                      69     7

(4) Must be true in either r7c8 or r7c9 so there will be one of two JExocets with common cross line candidates in the other stacks
(679)JExocet:r12c7,r4c8,r7c8|9

Resulting conjugate chains if 6,7, or 9 are base digits:
(6)r4c8 ^ (6)r4c5 ^ (6)r3c5 ^ (6#2)r12c47 ^ (6#2)r12c37
(7)r4c8 ^ (7)r4c1 ^ (7)r3c1 ^ (7#2)r12c37
(9)r4c8 ^ (9)r4c2 ^ (9)r3c2 ^ (9#2)r12c37
Showing that (6) is incompatible with (7) or (9) as a base digit as either (6x)UR:r12c37 or (6x)UR:r12c47 would result

=> r12c7,r4c8,r7c89 <> 6, r47c7,r23c8,r3c9 <>79, r126c1,r128c6 <> 7, r12c3,r129c5 <> 9, [Edit] r4c8 <> 2346

There is also (4679) Shark/Multi-Fish available which can be used before or after the JExocet.

[champagne]

champagne, are you pulling my chain, or do you really not know the definition of a native strong inference?

what is your definition of a native strong inference
will be easier in that way

or may be

why my answer in not enough to make valid the "abi's loop

[champagne]

I tested my alternative proof with Platinum Blonde.

David, I am not surprised that that proof works as well with your approach.

In fact, the original "abi" loop does not use the exocet property. I added it to get a strong link, but it works as well with ALS property.

In Platinum Blonde, with the '4' locked in r7c89, we have the als r7c1256 and the same loop as in fata morgana.
(platinum Blonde has no exocet)

What I like very much in "abi"s loop is that it uses the strict minimum number of properties in the puzzle.

Another point is that we don't have here the alternative solution through chains. The added property I mentioned was linked to the exocet.

EDIT I forgot to notice that your "conditional" Jexocet in r7c8|9 is another interesting view on that puzzle.
my program does not consider such situations but this explains also why it works in the same way

[ronk]

champagne, are you pulling my chain, or do you really not know the definition of a native strong inference?

what is your definition of a native strong inference

A single native strong inference set is the set of candidates in one cell, or the set of like-valued candidates in one row, column or box. Judging from your earlier response, the "abi loop" using derived sis ...

1r7c1 - 1r9c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = 3r9c8 - 3r7c7 = 1r7c1

... becomes (continuing your notation style) ...

1r7c1 - 1r9c2 = (1-3)r4c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = (1-3)r6c8 = 3r9c8 - 3r7c7 = 1r7c1

after replacing the (red) derived sis with (blue) native sis. Now this may look like just a longer version of the same thing, but it exposes an embedded impossible loop ... (1-3)r4c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = 1r6c8 ... within the continuous loop that it appears to be. The impossible loop is impossible because it contradicts the exocet assumption that produced it.

[David P Bird]

... becomes (continuing your notation style) ...

1r7c1 - 1r9c2 = (1-3)r4c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = (1-3)r6c8 = 3r9c8 - 3r7c7 = 1r7c1

after replacing the (red) derived sis with (blue) native sis. Now this may look like just a longer version of the same thing, but it exposes an embedded impossible loop ... (1-3)r4c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = 1r6c8 ... within the continuous loop that it appears to be. The impossible loop is impossible because it contradicts the exocet assumption that produced it.

Isn't this contradiction just another way of showing that (1) can't be a member of the base set?

[champagne]

champagne, are you pulling my chain, or do you really not know the definition of a native strong inference?

what is your definition of a native strong inference

A single native strong inference set is the set of candidates in one cell, or the set of like-valued candidates in one row, column or box. Judging from your earlier response, the "abi loop" using derived sis ...

1r7c1 - 1r9c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = 3r9c8 - 3r7c7 = 1r7c1

... becomes (continuing your notation style) ...

1r7c1 - 1r9c2 = (1-3)r4c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = (1-3)r6c8 = 3r9c8 - 3r7c7 = 1r7c1

after replacing the (red) derived sis with (blue) native sis. Now this may look like just a longer version of the same thing, but it exposes an embedded impossible loop ... (1-3)r4c2 = 3r2c2 — 3r3c1 = 1r3c9 — 1r1c8 = 1r6c8 ... within the continuous loop that it appears to be. The impossible loop is impossible because it contradicts the exocet assumption that produced it.

we are missing one or 2 more posts and I'll be completely lost.



1r7c1 - 1r9c2 = 3r2c2 - 3r3c1 = 1r3c9 - 1r1c8 = 3r9c8 - 3r7c7 = 1r7c1

this is, as far as I know, an Alternate Inference Chain written strictly following the rules in that forum.

For sure, each strong inference is depending on the initial assumption (13r5c46) but this is true for the 4 strong inferences, not only for 2 of them

If only native sis are authorised in an AIC, the garbage collectors will be filled of nearly all AIC's published in that forum.
No more basic group, no more ALS AHS groups ......



1r7c1 - 1r9c2 = (1-3)r4c2 = 3r2c2 - 3r3c1 = 1r3c9 - 1r1c8 = (1-3)r6c8 = 3r9c8 - 3r7c7 = 1r7c1

I don't know what is that animal, but for sure it's not an AIC. I am only using AIC's so I can't publish that, I just don't understand it.


To stay positive, As I am not aware of the writing rules for complex situations (if they do exist), I prefer to expose the situation step by step.

In that case

. effect of the assumption
. inferred (embedded) loop
. consequences of the inferred (embedded) loop

I have no objection to any rewriting of that logic.
I just say the logic is perfect (even without the exocet effect)

[champagne]

1r7c1 - 1r9c2 = 3r2c2- 3r3c1 = 1r3c9 - 1r1c8 = 3r9c8 - 3r7c7 = 1r7c1

Isn't this contradiction just another way of showing that (1) can't be a member of the base set?

Just one remark David, this is not a contradiction chain but a nice loop
I accept a quick reading can be misleading

[ronk]

For sure, each strong inference is depending on the initial assumption (13r5c46) but this is true for the 4 strong inferences, not only for 2 of them

A native strong inference set for an AUR would be all its cells. Take my word for it, there would still be an embedded impossible loop.

If only native sis are authorised in an AIC ...

I didn't say that.

1r7c1 - 1r9c2 = (1-3)r4c2 = 3r2c2 - 3r3c1 = 1r3c9 - 1r1c8 = (1-3)r6c8 = 3r9c8 - 3r7c7 = 1r7c1
I don't know what is that animal, but for sure it's not an AIC.

Sigh! champagne, this discussion reminds me of your posts here and here and here and here, and lastly
here, but without the apology being made to me, whose time you wasted. I don't care to travel that road again.