The New Sudoku Players' Forum

[eleven]

... 1744614 - which was a good deal slower than any of the others. Has that puzzle previously been thought to be uniquely hard?

Obi-Wahn's puzzle
5.6...7...1.3.....8...5.9.....1...2.....8.6.7.....2.4.7...9...6.3...42....5......
in the initial pencilmark grid has a 4x4 MSLS (r1357,c2468) eliminating 16 candidates (i suppose, Space or David Bird would have spotted it manually), which reduces the ER to 9.2. So no, not extremely hard.

[Added:] how to spot it: 56789 - 1234

Code: Select all

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

[marek stefanik]

TLC can solve any sudoku using just the rules TLTT and L*T!.
The proof is again based on Resolution, there are these three differences:

Hidden Text: Show

We resolve each link ¬c1 ∨ ¬c2 with a truth including c1 but not c2, then we resolve the resolvent and a truth containing c2 but not c1.

That's just one application of the TLTT rule.

Otherwise we iteratively resolve T1 with each link ¬c ∨ ¬c', s.t. T contains c'. We then resolve with T2 and the final result represents the resolvent obtained by Resolution.

We start with T1 and iteratively use the TLTT rule with T2.
Example (c=2r2c2):
T1 = <1r1c1, 2r1c2, 4r2c2>
T2 = <2r2c2, 3r3c3, 5r2c2>
T1 >r2c2< T2 -> T3 = <1r1c1, 2r1c2, 3r3c3>
T3 >2c2< T2 -> T4 = <1r1c1, 3r3c3, 5r2c2>

Whenever Resolution derives the elimination ¬c, we derive it by iteratively resolving the corresponding truth with links ¬c ∨ ¬c', s.t. T contains c'.

One application of the L*T! rule.

I have not found any PM grid that has a braid but resists TLC (i.e. from which no elimination can be deduced using these rules), nor indeed any that even needs TLTT

I won't go over the proof, but TLC without the TLTT rule can indeed prove all braids.
You just build links between the target and each candidate seeing a RLC.
When you add a variable, you merge the links via the LLLL rule and then use the LTLL rule to create links between the target and candidates which see the new RLC.
At the end, you use the L*T! rule.

TLTT is necessary to prove triples or TH, so I assume that most of the known T&E(3) puzzles need TLTT.

Marek

[ag24ag24]

Thanks so much guys for the feedback! I've been cranking through the 11.8ers over the past 48 hours and there is only one still standing. Meanwhile my next step will be to improve the output of proofs, which currently includes a lot of mentions of superfluous candidates in the LHS of arrows, leading to inclusion of superfluous deductions; it's not at all trivial to identify and remove these automatically, but once that's working I am optimistic that these proofs will be comprehensible enough to lead to the discovery of new patterns (via the identification of a bunch of relatively concise proofs of similar structure that eliminate from PM grids that lack any currently known pattern).

[ag24ag24]

TLC can solve any sudoku using just the rules TLTT and L*T!.
=

Thanks. I think this is the same as a proof that I came up with showing that TLTT and L*T! can prove any elimination that is proved by the "truth covering" method of Allan Barker. Barker introduced a lot of concepts like rank and "dark logic", but I'm pretty sure that his method is fully encompassed by the following:

A candidate c=v can be eliminated from a PM grid if the grid's initial resolution state includes a set T of n truths and a set L of n-1 links, with n>=1, such that:
- c=v does not appear in any member of either T or L; and
- no candidate appears in a member of L and also in more than one member of T; and
- all candidates that appear in T but not L are linked (by links not in L) to c=v.

The proof that TLTT and L*T! can emulate this consists of repeatedly using TLTT to replace two truths and a link that intersects with both truths (at different candidates) - such a trio must always exist - by a single truth containing all candidates that are in either of the truths but not in the link, and then finishing the job with one L*T!.

The reason I didn't consider this a proof of the omnipotence of TLC was that I was not aware of any proof that the Barker method could prove any valid elimination. But against that, the Barker method is extremely dependent computationally on how many links and truths are included initially, so it looks to me as though ATLC indeed derives a lot of computational efficiency from consisting of rules all but one of which have only two premises.

[eleven]

I am neither familiar with with resolution rules nor Alan Barkers concepts.
My question is: Shouldn't your rules be able to find all (n-digit) templates eliminations ? (If so, they can solve all sudokus.)

[ag24ag24]

I don't think there is any simple way to determine whether my rules can find all template eliminations. (I's assuming that you mean "find all eliminations that can be proven using a template".) However, my focus is not on whether my rules can solve all sudokus: empirically it seems that it can, and moreover Marek has presented a proof that it can. Instead, my focus is on (a) whether it can solve all sudokus reasonably efficiently, and even more importantly (b) whether the logic that it discovers for solving sudokus that otherwise need T&E (whether it's T&E(Singles,2) or T&E(braids,1) or whatever) can lead to the identification of new patterns.

[eleven]

Well i would have preferred a proof, which does not rely on Lee’s Theorem.
I doubt, that your rules can lead to something more efficient than known methods. Concerning fnding new patterns i wish you good luck.

[ag24ag24]

Thank you I will of course report back. Concerning efficiency, I of course realise that when one allows T&E things can be far more efficient - I was only saying that T&E(ATLC,0) may be much more efficient than T&E(TLC,0) or the Barker method.

[ag24ag24]

By the way - since some here are evidently unfamiliar with it, here is the page where Barker describes his method:

https://sudoku.allanbarker.com/sweb/general.htm

[denis_berthier]

By the way - since some here are evidently unfamiliar with it, here is the page where Barker describes his method:
https://sudoku.allanbarker.com/sweb/general.htm

To be more precise, this is the page where he describes his method, without any of the "programming details" that radically modify it for making it computable.
.

[denis_berthier]

.
Just in order to talk of something precise, without all the complexities of hard puzzles that make any solution illegible, can you give the output of your program for the following puzzle?

Code: Select all

    +-------+-------+-------+
     ! . . 3 ! 4 . . ! . . . !
     ! . 5 . ! . . 9 ! 1 2 . !
     ! 7 . . ! . 2 . ! . . . !
     +-------+-------+-------+
     ! . 1 . ! 5 . 7 ! . . 8 !
     ! 6 . . ! . 9 . ! . . 7 !
     ! . . . ! . . . ! . 3 4 !
     +-------+-------+-------+
     ! . . 2 ! . . . ! . . . !
     ! . . . ! . . . ! . 9 . !
     ! 9 . . ! . 6 1 ! . 7 5 !
     +-------+-------+-------+
..34......5...912.7...2.....1.5.7..86...9...7.......34..2.............9.9...61.75

.

[marek stefanik]

A candidate c=v can be eliminated from a PM grid if the grid's initial resolution state includes a set T of n truths and a set L of n-1 links, with n>=1, such that:
- c=v does not appear in any member of either T or L; and
- no candidate appears in a member of L and also in more than one member of T; and
- all candidates that appear in T but not L are linked (by links not in L) to c=v.

This cannot prove any elimination.
A slightly stronger rule would be:
A candidate c can be eliminated from a PM grid if the grid's initial resolution state includes a set T of n truths and a set L of n-1 links, with n>=1, such that:
Each candidate which appears in more members of T than of L is linked to c.

This rule is equivalent to T&E(rank0 logic), which cannot prove TH.

Hidden Text: Show

Code: Select all

,---------------------------------,---------------------------------,---------------------------------,
| 123        456789     456789    | 123        456789     456789    | 123456789  123456789  123456789 |
| 456789     123        456789    | 456789     123        456789    | 123456789  123456789  123456789 |
| 456789     456789     123       | 456789     456789     123       | 123456789  123456789  123456789 |
:---------------------------------+---------------------------------+---------------------------------:
| 123        456789     456789    | 123456789  123456789  123456789 | 123456789  123456789  123456789 |
| 456789     123        456789    | 123456789  123456789  123       | 123456789  123456789  123456789 |
| 456789     456789     123       | 123456789  123        123456789 | 123456789  123456789  123456789 |
:---------------------------------+---------------------------------+---------------------------------:
| 123456789  123456789  123456789 | 123456789  123456789  123456789 | 123456789  123456789  123456789 |
| 123456789  123456789  123456789 | 123456789  123456789  123456789 | 123456789  123456789  123456789 |
| 123456789  123456789  123456789 | 123456789  123456789  123456789 | 123456789  123456789  123456789 |
'---------------------------------'---------------------------------'---------------------------------'

123r4c4 are the only candidates which don't appear in any solution.

Suppose you try to eliminate (WLOG) 1r4c4 by T&E(rank0 logic).
That means you set 1r4c4 and can only make rank0 steps until you reach a contradiction.
Rank0 logic generalises to fractional sudoku, but the grid with 1r4c4 still has fractional solutions, such as this one (each candidate's truth value is 1/# of candidates in its cell):

Code: Select all

,------------,------------,------------,
| 1   4   5  | 23  6   7  | 23  8   9  |
| 6   23  8  | 4   23  9  | 5   1   7  |
| 7   9   23 | 5   8   1  | 23  4   6  |
:------------+------------+------------:
| 23  6   7  | 1   5   8  | 4   9   23 |
| 5   23  4  | 7   9   23 | 1   6   8  |
| 9   8   1  | 6   23  4  | 7   23  5  |
:------------+------------+------------:
| 23  7   6  | 8   4   23 | 9   5   1  |
| 4   5   23 | 9   1   6  | 8   7   23 |
| 8   1   9  | 23  7   5  | 6   23  4  |
'------------'------------'------------'

Therefore you cannot reach a contradiction with rank0 logic, so T&E(rank0 logic) cannot prove TH.

Well i would have preferred a proof, which does not rely on Lee’s Theorem.

Same, but I have no idea how to go about it.
Your template idea seems interesting, but you would need a stronger induction assumption – that the rules can construct all possible n-template truths.
You might be able to bypass Lee's theorem that way, but it seems complicated.
Even just n=1, what omnipotent theory do we have for SDPs other than Resolution?

Marek

[ag24ag24]

A candidate c=v can be eliminated from a PM grid if the grid's initial resolution state includes a set T of n truths and a set L of n-1 links, with n>=1, such that:
- c=v does not appear in any member of either T or L; and
- no candidate appears in a member of L and also in more than one member of T; and
- all candidates that appear in T but not L are linked (by links not in L) to c=v.

This cannot prove any elimination.

Very interesting! I had not heard of fractional Sudoku before. Does this approach also show that TLC cannot resolve TH? (I have found empirically that ATLC can solve TH, though it only does it with a lot of work.)

EDIT: Of course you already showed that TLC is omnipotent - what I meant to ask is, Does this approach also show that TLTT and L*T! on their own (without LTLL or LLLL) cannot resolve TH?

[ag24ag24]

.
Just in order to talk of something precise, without all the complexities of hard puzzles that make any solution illegible, can you give the output of your program for the following puzzle?

Code: Select all

    +-------+-------+-------+
     ! . . 3 ! 4 . . ! . . . !
     ! . 5 . ! . . 9 ! 1 2 . !
     ! 7 . . ! . 2 . ! . . . !
     +-------+-------+-------+
     ! . 1 . ! 5 . 7 ! . . 8 !
     ! 6 . . ! . 9 . ! . . 7 !
     ! . . . ! . . . ! . 3 4 !
     +-------+-------+-------+
     ! . . 2 ! . . . ! . . . !
     ! . . . ! . . . ! . 9 . !
     ! 9 . . ! . 6 1 ! . 7 5 !
     +-------+-------+-------+
..34......5...912.7...2.....1.5.7..86...9...7.......34..2.............9.9...61.75

.

Sure, but it's still really verbose (even though the program derives a complete solution in only a few seconds). I can provide the sequence of eliminations, or the proof of one specific elimination - but probably it's best if I complete my current task of stripping the proofs of extraneous candidates and steps. Working on it!

[ag24ag24]

In the meantime, I would like to come back to the observation I briefly described in my original RESULTS post, namely that a very high proportion (more than 1/3) of the ph_2010 puzzles with SER exactly 11.0 seem to have tridagons. I came across this because those puzzles hit a wall (a state from which they take many hours to progress) at a number of remaining candidates from which no other puzzle lasts for more than a few minutes - always under 180 and often under 150. (Actually, to be scrupulously accurate, I did find one puzzle that behaves this way and has SER 11.1, not 11.0.) It seems to me that if my program had magically existed 15 years ago, tridagons would have been discovered a lot sooner. Here's an example with only 137 candidates:

Code: Select all

9   8   7   6   124   234   135   145   125
126   146   136   5   78   2349   368   469   267
256   456   356   14   78   2349   368   1469   2679
4   7   156   8   3   156   2   1569   59
156   2   8   9   1456   1456   7   3   156
3   156   9   2   156   7   156   8   4
7   3   156   14   9   1456   156   2   8
8   156   4   7   1256   1256   9   156   3
156   9   2   3   156   8   4   7   156


which originated from puzzle 2591825 in ph_2010. I'm very much a tridagon novice, but if I understand the concept, boxes 4, 6, 7 and 9 have a tridagon on digits 1, 5 and 6, leading to the deduction that cell D8 must be 9. Please let me know if I'm getting that wrong.

But the main reason I mention this is that one of the dozen or so puzzles that behaved this way seems to be a variant of the tridagon pattern, and I would be most interested to learn whether it is new. Here it is:

Code: Select all

9   8   7   6   145   1345   1345   2   145
6   125   12345   12458   9   13458   1345   145   7
1234   125   12345   1245   7   1345   8   9   6
5   4   189   19   6   7   2   3   18
128   126   12689   14589   3   1458   1456   7   1458
138   7   1368   1458   145   2   156   145   9
124   9   1245   145   8   6   7   145   3
148   3   1458   7   2   145   9   6   145
7   156   456   3   145   9   145   8   2


originating from ph_2010 puzzle 3044455 and possessing 152 candidates. Boxes 8 and 9 look tridagon-like on digits 1,4 and 5, but boxes 34 and 56 do not seem to complete the pattern, and I can't see any other quartet of boxes that work either. Am I missing something, or is this a known variant of tridagons, or is it genuinely new?