The New Sudoku Players' Forum

by **yzfwsf** » Fri Apr 17, 2020 6:14 am

Code: Select all: .1..9..4.4......52..2...7..5....74...3.8...7...7.3....1....32......4...6.8.1.....

SE:9.0 \ Hodoku Rate:24866 \YZF_SUDOKU Rate:10900

by **RSW** » Sat Apr 18, 2020 9:05 am

I'll make no claims as to the elegance of this solution, but since I've been working on my solver to have it prove non junior exocets, I thought I might as well post this.

Code: Select all: 1 2 3 4 5 6 7 8 9 +-------------------+-------------------+-------------------+ 1| 3678 1 3568 | 23567 9 2568 | 368 b4 b38 | 2| 4 679 t3689 | 367 1678 168 | 13689 5 2 | 3| 3689 569 2 | t3456 1568 14568 | 7 13689 1389 | +-------------------+-------------------+-------------------+ 4| 5 269 1689 | 269 126 7 | 4 123689 1389 | 5| 269 3 1469 | 8 1256 124569 | 169 7 159 | 6| 2689 2469 7 | 24569 3 124569 | 1689 12689 1589 | +-------------------+-------------------+-------------------+ 7| 1 45679 4569 | 5679 5678 3 | 2 89 47 | 8| 2379 2579 359 | 2579 4 2589 | 13589 1389 6 | 9| 23679 8 34569 | 1 2567 2569 | 359 39 47 | +-------------------+-------------------+-------------------+

Exocet: GE2: 348 R1C89, r2c3 r3c4

Proof of Generic Exocet:
+4r1c8 & -4r2c3 & -4r3c4 -> Leads to contradiction using basics.
+3r1c9 & -3r2c3 & -3r3c4 -> *1st non contradiction. A second instance will be a fail.
+8r1c9 & -8r2c3 & -8r3c4 -> Leads to contradiction using basics.
All Base/Target mutual exclusions, except one, lead to contradiction.
Generic Exocet is proven.
GE2: 348 R1C89, r2c3 r3c4 -> -3r1c9 -356r3c4 -369r2c3

Code: Select all: 1 2 3 4 5 6 7 8 9 +----------------+------------------+-------------+ 1| 67 1 56 | 2567 9 256 | 3 4 8 | 2| 4 679 8 | 3 167 16 | 19 5 2 | 3| 3 59 2 | 4 15 8 | 7 6 19 | +----------------+------------------+-------------+ 4| 5 26 t169 | 269 126 7 | 4 8 3 | 5| 269 3 1469 | 8 1256 124569 | b169 7 b159 | 6| 8 46 7 | 569 3 t14569 | 169 2 159 | +----------------+------------------+-------------+ 7| 1 4567 456 | 567 8 3 | 2 9 47 | 8| 279 257 3 | 2579 4 259 | 8 1 6 | 9| 2679 8 469 | 1 267 269 | 5 3 47 | +----------------+------------------+-------------+

Exocet: GE2: 1569 R5C79, r4c3 r6c6

Proof of Generic Exocet:
+1r5c7 & -1r4c3 & -1r6c6 -> Leads to contradiction using singles.
+6r5c7 & -6r4c3 & -6r6c6 -> *1st non contradiction. A second instance will be a fail.
+9r5c7 & -9r4c3 & -9r6c6 -> Leads to contradiction using singles.
+1r5c9 & -1r4c3 & -1r6c6 -> Leads to contradiction using singles.
+5r5c9 & -5r4c3 & -5r6c6 -> Leads to contradiction using basics.
+9r5c9 & -9r4c3 & -9r6c6 -> Leads to contradiction using singles.
All Base/Target mutual exclusions, except one, lead to contradiction.
Generic Exocet is proven.
GE2: 1569 R5C79, r4c3 r6c6 -> -1r4c3 -1r5c79 -149r6c6 -5r6c4
stte

by **eleven** » Sat Apr 18, 2020 7:00 pm

RSW wrote:Exocet: GE2: 348 R1C89, r2c3 r3c4

Proof of Generic Exocet:
+4r1c8 & -4r2c3 & -4r3c4 -> Leads to contradiction using basics.
+3r1c9 & -3r2c3 & -3r3c4 -> *1st non contradiction. A second instance will be a fail.
+8r1c9 & -8r2c3 & -8r3c4 -> Leads to contradiction using basics.

[Second try:]
I am not happy with this kind of "exocet".
In the first step you just prove by contradiction 4r3c4 (since 4 is given in r1c8 and r2c1).
Then 3r1c9 obviously implies 3r2c4 (no target).
But your 2nd line would prove, that 3r1c8 => 3r2c3. I.e. r1c9 cannot be 3.
Your 3rd line then is the same as eliminating 8r1c3 (or r4c3) by contradiction.

So with the same deductions you just can eliminate 3 digits to get the same results without an exocet (a bit easier).

by **RSW** » Sun Apr 19, 2020 12:35 am

@eleven
I appreciate your comments. This is still a work in progress, and my solver uses a very limited set of techniques to prove the exocet. As you pointed out, the fact that the one of the base cells is a given, the proof could have been much simpler. I'm in the process of adding program logic to take advantage of the givens in base cells and target cells. However, givens that appear elsewhere in the exocet band may be more difficult to deal with.

I admit that I don't particularly like this kind of exocet either. My reason for trying to develop a solving technique using non junior exocets, was that it's something that a computer program can easily identify, and if it's able to prove them, then it often results in a large number of exclusions, and can therefore solve some very difficult puzzles, even if the solution isn't very pretty.

Website · by **denis_berthier** » Sun Apr 19, 2020 9:09 am

I'll use this puzzle (a member of W9) to show how whips and t-whips (a special case in which the pattern doesn't depend on the target) can work together.
Until recently, I rarely activated t-whips because they don't allow more puzzles to be solved, but they are interesting in their own right: 1) for not depending on the target and 2) for allowing to find alternative resolution paths.
Contrary to braids that rarely appear when whips are active, t-whips are relatively frequent.
(Notice that, the priorities are standardly set as follows: t-whips[k] > whips[k] > braids[k], i.e. from the most specific to the most general.)

Hidden Text: Show

RSW wrote:My solver uses a very limited set of techniques to prove the exocet

My opinion about Exocets hasn't changed: J-Exocets are a well-defined pattern, Excocets are not. Excocets may be an interesting starting point for defining a whole family of patterns, but that can only happen if additional logical conditions are clearly defined. Any obscure procedure claiming "a contradiction is reached" is useless. Unfortunately, since the pseudo-definition of Excocets and apart from David's definition of J-Excocets, I've seen zero progress in this direction.
So, if your "solver uses a very limited set of techniques to prove the exocet", it might be a good omen for new patterns; it might be interesting to first write these techniques in an explicit logical form, so that they could be used to write extensions to the basic J-Excocets.
Could you give some examples of this set of techniques?

by **champagne** » Sun Apr 19, 2020 1:09 pm

RSW wrote:I'll make no claims as to the elegance of this solution, but since I've been working on my solver to have it prove non junior exocets, I thought I might as well post this.
Code: Select all
1 2 3 4 5 6 7 8 9 +-------------------+-------------------+-------------------+ 1| 3678 1 3568 | 23567 9 2568 | 368 b4 b38 | 2| 4 679 t3689 | 367 1678 168 | 13689 5 2 | 3| 3689 569 2 | t3456 1568 14568 | 7 13689 1389 | +-------------------+-------------------+-------------------+ 4| 5 269 1689 | 269 126 7 | 4 123689 1389 | 5| 269 3 1469 | 8 1256 124569 | 169 7 159 | 6| 2689 2469 7 | 24569 3 124569 | 1689 12689 1589 | +-------------------+-------------------+-------------------+ 7| 1 45679 4569 | 5679 5678 3 | 2 89 47 | 8| 2379 2579 359 | 2579 4 2589 | 13589 1389 6 | 9| 23679 8 34569 | 1 2567 2569 | 359 39 47 | +-------------------+-------------------+-------------------+

Exocet: GE2: 348 R1C89, r2c3 r3c4

Proof of Generic Exocet:
+4r1c8 & -4r2c3 & -4r3c4 -> Leads to contradiction using basics.

Hi RSW,

Flying over this thread, I saw your proposal.
This was the first attempt to apply the exocet logic with a given, so I had a look to your exocet.

As your 4 r1c8 is a given, if we have an exocet pattern, we must have 4 r3c4 (4 is not possible in the other target)
So this should be the first move.

In the exocet logic, the "proof per digit is assumed easy just because it appears in a single digit map.

the '4' digit map is

Code: Select all: ... ... .4. 4.. ... ... ... 4.4 ... ... ... 4.. ..4 ..4 ... .4. 4.4 ... .44 ... ..4 ... .4. ... ..4 ... ..4

forcing -4r3c4 (the usual way to establish the proof) we come to

Code: Select all: ... ... .4. 4.. ... ... ... ..4 ... ... ... 4.. ..4 ... ... ... 4.. ... .4. ... ... ... .4. ... ... ... ..4

so in the single digit map, we still have a solution. This is not a classical exocet pattern .

For sure if in the general context this solution is not valid, then we enter the field of "extended exocets", but this is IMO only for "potential hardest" puzzles,
and again, 4r1c8 being a given, this immediately gives 4r3c4.

If I assume this correct (in fact we have 4r3c4 in the solution) the proof can not work for the digit '3' and in fact I get

Code: Select all: ... ... ..3 ... 3.. ... 3.. ... ... ... ... .3. .3. ... ... ... .3. ... ... ..3 ... ..3 ... 3.. ..3 ... 3..

four possible solutions if '3' is in the base and not in the targets. '3' is not an exocet digit

by **champagne** » Sun Apr 19, 2020 1:25 pm

RSW wrote: My reason for trying to develop a solving technique using non junior exocets, was that it's something that a computer program can easily identify, and if it's able to prove them, then it often results in a large number of exclusions, and can therefore solve some very difficult puzzles, even if the solution isn't very pretty.

My recent experimentation in the potential hardest field shows me that coupling exocets (including a junior exocet) with the same base can be very efficient. No need here to have "false" exocets. I am only considering the standard proof using the single digit pm.

I am working on a counter example on the puzzle N° 2 of the data base of potential hardest, but just back from the southern hemisphere, I have problems with my laptop and I have first to restart it to get back part of the data that I have prepared.

by **RSW** » Tue Apr 21, 2020 4:36 pm

champagne wrote:My recent experimentation in the potential hardest field shows me that coupling exocets (including a junior exocet) with the same base can be very efficient. No need here to have "false" exocets. I am only considering the standard proof using the single digit pm.

I should clarify that I wasn't specifically looking for exocets that contain givens, but neither was I rejecting them. I had programmed my solver to find Junior Exocets, and was finding that most of the prospective patterns failed the cover line test. These failed patterns seemed to be worthy of further examination. So, for the cases that fail the cover test, my solver attempts to prove them as valid exocets using other means. I have been referring to these patterns as non-junior, or generic exocets, but that terminology may imply that I'm looking at a much wider range of patterns than I really am. I am only looking at patterns where the base and target cells are all in the same chute and would have been verified as a junior exocet except for the failed cover test. It might be more accurate to call them Almost Junior Exocets.

The exocet patterns where a base or target is a given, may be an opportunity to arrive at a simpler proof, and I will explore this further.

by **champagne** » Wed Apr 22, 2020 7:37 am

RSW wrote:
champagne wrote:My recent experimentation in the potential hardest field shows me that coupling exocets (including a junior exocet) with the same base can be very efficient. No need here to have "false" exocets. I am only considering the standard proof using the single digit pm.

I should clarify that I wasn't specifically looking for exocets that contain givens, but neither was I rejecting them. I had programmed my solver to find Junior Exocets, and was finding that most of the prospective patterns failed the cover line test. These failed patterns seemed to be worthy of further examination. So, for the cases that fail the cover test, my solver attempts to prove them as valid exocets using other means. I have been referring to these patterns as non-junior, or generic exocets, but that terminology may imply that I'm looking at a much wider range of patterns than I really am. I am only looking at patterns where the base and target cells are all in the same chute and would have been verified as a junior exocet except for the failed cover test. It might be more accurate to call them Almost Junior Exocets.

The exocet patterns where a base or target is a given, may be an opportunity to arrive at a simpler proof, and I will explore this further.

The exocet definition is quite clear and has no chute constraint.
The proof must be done using exclusively each digit pm. (out of the "locket digit extension")

The "single digit pm proof" is not as such a constraint of the exocet property, but I have 2 reasons to push in this direction

. a "per digit" proof is always easy to establish
. most of the known exocets (all JE and many others) are in this group.

The problem with the extended proof is that it can be a highly complex logic. If a simple logic can be applied, I see no reason to reject such exocets.

by **RSW** » Wed Apr 22, 2020 7:47 pm

champagne wrote:The exocet definition is quite clear and has no chute constraint.

Unfortunately, I've spent hours going through the thousands of posts on this forum that discuss exocets, and I've failed to locate the official definition. If you could point me to the appropriate post, I would be extremely grateful.

Having been unable to find a clear definition, I decided to work with the Junior Exocet subset that has been written up in David P. Bird's detailed series of articles. As the Junior Exocets have the base and target cells in the same chute, I decided to restrict my research to those cases.

by **champagne** » Fri Apr 24, 2020 2:37 am

RSW wrote:
champagne wrote:The exocet definition is quite clear and has no chute constraint.

Unfortunately, I've spent hours going through the thousands of posts on this forum that discuss exocets, and I've failed to locate the official definition. If you could point me to the appropriate post, I would be extremely grateful.

Having been unable to find a clear definition, I decided to work with the Junior Exocet subset that has been written up in David P. Bird's detailed series of articles. As the Junior Exocets have the base and target cells in the same chute, I decided to restrict my research to those cases.

You can find the definition of an exocet in the first posts if this thread http://forum.enjoysudoku.com/exotic-patterns-a-resume-t30508.html
The first posts are summarizing what I considered as key information for this topic

The definition of the basic exocet has been given years ago (before the extension to targets with locked candidates).

by **RSW** » Fri Apr 24, 2020 8:51 pm

Thank you very much. I'd somehow overlooked that post.

The New Sudoku Players' Forum

Extreme Puzzle No.3

Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3

Re: Extreme Puzzle No.3