A concise and seemingly omnipotent Sudoku resolution theory
48 posts
• Page 1 of 4 • 1, 2, 3, 4
A concise and seemingly omnipotent Sudoku resolution theory
by ag24ag24 » Mon Mar 24, 2025 4:31 pm
I would greatly appreciate a critique from the experts here of a new (or so I believe!) resolution theory that seems to be extremely powerful, deriving full solutions - purely stepwise, i.e. in T&E(0) - for many (looks like most; conceivably all...) puzzles that are in ph_2010, as well as everything easier that I've tried it on. I'll split this into a few sections: preliminaries, braid-like resolution theory, new resolution theory, algorithm, results, next steps (along with some details of the results), code (with two example proofs). I hope the above has piqued your interest enough to get you to slog through the rest!
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:32 pm
PRELIMINARIES. I define a puzzle's resolution state as the set of links and truths (collectively termed "assertions"), each consisting of a set of individually undecided candidates, that have thus far ben shown to be true of a PM grid and that are not trivially implied by another one in the set. An assertion consists of a set of >=2 candidates, and if it is a link it has the meaning that at most one of the set is true in the solved grid, whereas if it is a truth it means that at least one is. (So assertion A trivially implies assertion B if either (i) they are both links and every candidate in B is also in A, or (ii) they are both truths and every candidate in A is also in B.) Thus, a grid's initial resolution state is the set of links and truths that arise directly from its unsolved cells and units (rows, columns or boxes): each such assertion contains either the set of >=2 candidates that refer to the same cell, or else the set of >=2 candidates that all refer to the same value and to cells that are in a given unit. The initial set of assertions thus includes both a link and a truth on each such set of candidates, since exactly one member of each such set is true in the solved grid. New assertions and eliminations are then derived from the existing set according to a set of resolution rules; these must include the two "singles" rules (a single-candidate truth is a proof of that candidate, and a link containing a proven candidate is an elimination of all its other candidates) and the "irrelevance" rule (any assertion containing an eliminated candidate gets that candidate removed). Single-candidate links, and truths containing a proven candidate, are truisms and are discarded outright. A resolution process terminates with either (a) resolution, i.e. all assertions have been discarded, which equates to the puzzle being solved, or (b) quiescence, i.e. there are no sets of assertions that trigger a rule whose derived assertion is new and not trivially implied.
I write the above just for clarity and disambiguation - I don't think any of it is in any way new or controversial, but please shout if I'm wrong! The one thing that I realise may be unorthodox is that resolution rules can derive new assertions, whereas in all the RTs I've seen discussed here (and elsewhere) they always derive eliminations in one step.
I write the above just for clarity and disambiguation - I don't think any of it is in any way new or controversial, but please shout if I'm wrong! The one thing that I realise may be unorthodox is that resolution rules can derive new assertions, whereas in all the RTs I've seen discussed here (and elsewhere) they always derive eliminations in one step.
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:32 pm
BRAID-LIKE RESOLUTION THEORY. In order to prepare the ground for my new RT, I will first present a set of resolution rules that seems to recapitulate all the many types of chains/whips/braids, essentially by removing two assertions (always one link and one truth) from a chain - but with rather more generality, mostly as a result of lacking any restriction to two-candidate assertions (bi-valued cells etc). Each rule derives a new assertion from three existing ones (the "premises"), except that the last rule can have any number >=2 of premises. The rules are as follows (notation explained below):
LLLL: >A,B,D,G< + >B,C,E,G< + >A,C,F,G< gives >A,B,C,G<
TLTT: <A,B,D,G> + >B,C,E,G< + <A,C,F,G> gives <A,D,F,G>
LTLL: >A,B,D,G< + <B,C,G> + >A,C,F,G< gives >D,F,G<
L*T!: >A,B1,C1< + >A,B2,C2< + ... + <B1,B2,...> gives !A (elimination of A)
I'm going to call this theory "TLC", for "truth-link contraction", because TLTT and LTLL essentially "contract" a chain of three assertions into one.
Notation:
- Inward-pointing angle brackets ">...<" denote links.
- Outward-pointing angle brackets "<...>" denote truths.
- The rule names "LLLL", "TLTT", "LTLL" come from whether the assertions are links vs truths.
- Each letter stands for a (possibly empty) SET of candidates, not just one candidate.
- Each letter denotes the candidates present in a certain subset of the rule's candidate sets: e.g. in rule TLTT, "A" encompasses all candidates that appear in both truths but not the link. Hence, the sets denoted by different letters are always disjoint (except that in L*T! the B's are allowed to intersect with each other - as are the C's, though no candidate can be in _all_ the C's since then it would instead be in A). Thus, the absence of "E" in rule LTLL says that all candidates in the truth must also be in one or both of the links, or else the rule is not triggered.
Simple AICs can be contracted all the way to an elimination by using only LTLL, but more complex networks need LLLL too. 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'd be grateful for any counterexamples. Grids that lack braids but yield to TLC do exist, in the form of cases where L*T! is triggered with three or more links and no other information. Similarly, anything that yields to the Barker "truth-covering" method will also yield to TLC, indeed to just TLTT and L*T!, because TLTT can replace two truths and a link intersecting both of them them but not including A (which will always exist) with a single truth until all links not including A and all but one truth are gone, at which point L*T! finishes the job. However, I would not be surprised (though I have not proved! - see below) if a lot of PM grids in T&E(Singles,2) resist TLC.
By having resolution rules that derive new assertions, rather than only ones that derive eliminations, I obtain the useful feature that most rules can have a fixed number of premises - three, for all the rules in TLC except L*T! - whereas braids may need arbitrarily many. I think this difference helps a lot in terms of determining the strength of a resolution theory (though I recognise that that is offset by the drawback that it only defines a procedure rather than a pattern). So...
LLLL: >A,B,D,G< + >B,C,E,G< + >A,C,F,G< gives >A,B,C,G<
TLTT: <A,B,D,G> + >B,C,E,G< + <A,C,F,G> gives <A,D,F,G>
LTLL: >A,B,D,G< + <B,C,G> + >A,C,F,G< gives >D,F,G<
L*T!: >A,B1,C1< + >A,B2,C2< + ... + <B1,B2,...> gives !A (elimination of A)
I'm going to call this theory "TLC", for "truth-link contraction", because TLTT and LTLL essentially "contract" a chain of three assertions into one.
Notation:
- Inward-pointing angle brackets ">...<" denote links.
- Outward-pointing angle brackets "<...>" denote truths.
- The rule names "LLLL", "TLTT", "LTLL" come from whether the assertions are links vs truths.
- Each letter stands for a (possibly empty) SET of candidates, not just one candidate.
- Each letter denotes the candidates present in a certain subset of the rule's candidate sets: e.g. in rule TLTT, "A" encompasses all candidates that appear in both truths but not the link. Hence, the sets denoted by different letters are always disjoint (except that in L*T! the B's are allowed to intersect with each other - as are the C's, though no candidate can be in _all_ the C's since then it would instead be in A). Thus, the absence of "E" in rule LTLL says that all candidates in the truth must also be in one or both of the links, or else the rule is not triggered.
Simple AICs can be contracted all the way to an elimination by using only LTLL, but more complex networks need LLLL too. 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'd be grateful for any counterexamples. Grids that lack braids but yield to TLC do exist, in the form of cases where L*T! is triggered with three or more links and no other information. Similarly, anything that yields to the Barker "truth-covering" method will also yield to TLC, indeed to just TLTT and L*T!, because TLTT can replace two truths and a link intersecting both of them them but not including A (which will always exist) with a single truth until all links not including A and all but one truth are gone, at which point L*T! finishes the job. However, I would not be surprised (though I have not proved! - see below) if a lot of PM grids in T&E(Singles,2) resist TLC.
By having resolution rules that derive new assertions, rather than only ones that derive eliminations, I obtain the useful feature that most rules can have a fixed number of premises - three, for all the rules in TLC except L*T! - whereas braids may need arbitrarily many. I think this difference helps a lot in terms of determining the strength of a resolution theory (though I recognise that that is offset by the drawback that it only defines a procedure rather than a pattern). So...
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:33 pm
NEW RESOLUTION THEORY. My new RT uses not only links and truths but also a third type of assertion, which I will call an arrow. An arrow is a truth contingent on another truth - it says that if any of a given set of candidates (I'll call this the left-hand side, LHS) is true in the solved grid, then at least one of the candidates in a second set (the RHS) also is. Thus, if the LHS is empty then the arrow is a truism, and if the RHS is empty then the arrow equates to the falsehood of all candidates in the LHS. However, unlike links and truths, either (or both) of the LHS and RHS can consist of only one candidate. No candidate appears in both the LHS and RHS of an arrow, because if any did, it could be deleted from the LHS without changing the meaning.
Arrows may sound innocent enough at first: seemingly they are just merges of two steps in a standard AIC (a link followed by a truth). However, in their full generality they turn out to be far more powerful than that.
I will write arrows thusly:
|L>>R|
and I will again use capital letters to denote the (possibly empty) sets of candidates appearing in each subset of a rule's sets of candidates. (As just explained, no letter ever appears in both sides of an arrow.) I believe that the power afforded by arrows is fully captured by the following six resolution rules (again named by reference to the various constituent assertion types):
LLLL: >A,B,D,G< + >B,C,E,G< + >A,C,F,G< gives >A,B,C,G< (unchanged from TLC)
LTA: >A,B< + <B,C> gives |A>>C|
ALA: |A,B>>C,D| + >A,C,E< gives |A>>D|
ATT: |A,B>>C,D| + <A,C,E> gives <C,D,E>
ALL: |A,B>>C| + >A,C,E< gives >b,E< for each maximal link b within B (note: no "D")
AAA: |A,B,E>>C,D| + |A,C,G>>B,D,H| gives |A,C,E,G>>B,D,H| (note: no "F")
and I'm calling this theory "ATLC", for "arrow-truth-link contraction". (But you can call it "Aubrey's tender loving care" if you like
)
Rule LLLL is the same as in TLC. All the other rules have two premises rather than three, and that seems to be where much of the power (see RESULTS) comes from. There's no explicit elimination rule, but that's fine, because eliminations arise when LTA or ALA derive an arrow with an empty RHS or when ATT derives a single-candidate truth. The absence of "D" in ALL says that all candidates in the arrow's RHS must also appear in the link. Similarly, the absence in rule AAA of a letter appearing in the RHS of the first arrow but nowhere else says that all candidates in the first arrow's RHS must also appear in one or other side of the second arrow. In rule ALL, "maximal link" means any subset of B that is also a subset of some link and is not a subset of a larger such subset of B. This is needed because the whole of B may not be a subset of a link.
ATLC is easily seen to be at least as powerful as TLC, because the TLC rules TLTT, LTLL and L*T! can be reconstituted by combining ATLC rules:
LTA: >B,C,E,G< + <A,C,F,G> gives |B,E>>A,F|
ATT: |B,E>>A,F| + <A,B,D,G> gives <A,F,D,G>
------------------------------------------------------------
TLTT: <A,B,D,G> + >B,C,E,G< + <A,C,F,G> gives <A,D,F,G>
LTA: >A,B,D,G< + <B,C,G> gives |A,D>>C|
ALL: |A,D>>C| + >A,C,F,G< gives >D,F,G< (because D is a subset of a link)
------------------------------------------------------------
LTLL: >A,B,D,G< + <B,C,G> + >A,C,F,G< gives >D,F,G<
LTA: >A,B1,C1< + <B1,B2,...Bn> gives |A,C1>>B2,...Bn|
ALA: |A,C1>>B2,...Bn| + >A,B2,C2< gives |A>>B3,...Bn| repeated n-2 times
ALA: |A>>Bn| + >A,Bn,Cn< gives |A>>|
------------------------------------------------------------
L*T!: >A,B1,C1< + >A,B2,C2< + ... + <B1,B2,...> gives |A>>|
and additional power arises (or does it?? - see below) from the presence of rule AAA and the fact that rule ALA can generate arrows that are not eliminations (i.e. that have a non-empty RHS), as well as the ability to combine the rules in other ways than the above. We also have two new ways in which assertion A trivially implies assertion B: one is if they are both arrows, every candidate in B's LHS is also in A's LHS, and every candidate in A's RHS is also in B's RHS, and the other is if A is a truth, B is an arrow, and every candidate in A is also in B's RHS.
So obviously I wrote a solver (i.e., a resolution-path-discoverer) based on ATLC...
Arrows may sound innocent enough at first: seemingly they are just merges of two steps in a standard AIC (a link followed by a truth). However, in their full generality they turn out to be far more powerful than that.
I will write arrows thusly:
|L>>R|
and I will again use capital letters to denote the (possibly empty) sets of candidates appearing in each subset of a rule's sets of candidates. (As just explained, no letter ever appears in both sides of an arrow.) I believe that the power afforded by arrows is fully captured by the following six resolution rules (again named by reference to the various constituent assertion types):
LLLL: >A,B,D,G< + >B,C,E,G< + >A,C,F,G< gives >A,B,C,G< (unchanged from TLC)
LTA: >A,B< + <B,C> gives |A>>C|
ALA: |A,B>>C,D| + >A,C,E< gives |A>>D|
ATT: |A,B>>C,D| + <A,C,E> gives <C,D,E>
ALL: |A,B>>C| + >A,C,E< gives >b,E< for each maximal link b within B (note: no "D")
AAA: |A,B,E>>C,D| + |A,C,G>>B,D,H| gives |A,C,E,G>>B,D,H| (note: no "F")
and I'm calling this theory "ATLC", for "arrow-truth-link contraction". (But you can call it "Aubrey's tender loving care" if you like
)Rule LLLL is the same as in TLC. All the other rules have two premises rather than three, and that seems to be where much of the power (see RESULTS) comes from. There's no explicit elimination rule, but that's fine, because eliminations arise when LTA or ALA derive an arrow with an empty RHS or when ATT derives a single-candidate truth. The absence of "D" in ALL says that all candidates in the arrow's RHS must also appear in the link. Similarly, the absence in rule AAA of a letter appearing in the RHS of the first arrow but nowhere else says that all candidates in the first arrow's RHS must also appear in one or other side of the second arrow. In rule ALL, "maximal link" means any subset of B that is also a subset of some link and is not a subset of a larger such subset of B. This is needed because the whole of B may not be a subset of a link.
ATLC is easily seen to be at least as powerful as TLC, because the TLC rules TLTT, LTLL and L*T! can be reconstituted by combining ATLC rules:
LTA: >B,C,E,G< + <A,C,F,G> gives |B,E>>A,F|
ATT: |B,E>>A,F| + <A,B,D,G> gives <A,F,D,G>
------------------------------------------------------------
TLTT: <A,B,D,G> + >B,C,E,G< + <A,C,F,G> gives <A,D,F,G>
LTA: >A,B,D,G< + <B,C,G> gives |A,D>>C|
ALL: |A,D>>C| + >A,C,F,G< gives >D,F,G< (because D is a subset of a link)
------------------------------------------------------------
LTLL: >A,B,D,G< + <B,C,G> + >A,C,F,G< gives >D,F,G<
LTA: >A,B1,C1< + <B1,B2,...Bn> gives |A,C1>>B2,...Bn|
ALA: |A,C1>>B2,...Bn| + >A,B2,C2< gives |A>>B3,...Bn| repeated n-2 times
ALA: |A>>Bn| + >A,Bn,Cn< gives |A>>|
------------------------------------------------------------
L*T!: >A,B1,C1< + >A,B2,C2< + ... + <B1,B2,...> gives |A>>|
and additional power arises (or does it?? - see below) from the presence of rule AAA and the fact that rule ALA can generate arrows that are not eliminations (i.e. that have a non-empty RHS), as well as the ability to combine the rules in other ways than the above. We also have two new ways in which assertion A trivially implies assertion B: one is if they are both arrows, every candidate in B's LHS is also in A's LHS, and every candidate in A's RHS is also in B's RHS, and the other is if A is a truth, B is an arrow, and every candidate in A is also in B's RHS.
So obviously I wrote a solver (i.e., a resolution-path-discoverer) based on ATLC...
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:33 pm
ALGORITHM. I maintain a list of assertions, each with two flags: used/unused and live/dead. The algorithm is as follows:
1) Construct a list of the truths and links directly described by the current PM grid (candidates referring to the same cell; candidates referring to the same number for cells all within a given unit). Mark all truths as live/used and all links as live/unused.
2) Pick a live/unused assertion P. Mark P as live/used. (Which we choose only affects speed.)
3) Generate all the new assertions arising from applying resolution rules to P and some live/used assertion - or, in the case of LLLL, to P and some pair of live/used assertions.
4) If any new assertion is an arrow with empty RHS or a single-candidate truth, remove all relevant candidates from the grid, do Singles and return to 1.
5) Discard any new assertion that is implied by another new assertion or by some existing live (used or unused) assertion.
6) Mark as dead any existing assertion (used or unused) that is implied by any remaining new assertion. (Keep hold of these, though, for reporting of the proof of any future elimination.)
7) Add any remaining new assertions as live/unused; store their premises for later reporting.
8) If there are any live/unused assertions (new or pre-existing), return to 2.
9) Halt. If there are still some live/used assertions, that means the final PM grid has resisted ATLC. Otherwise, i.e. if there are no live assertions, then there must also be no surviving candidates, i.e. the puzzle has been solved.
In my current code, to speed things up I do more than Singles at step 4: I also check (but only if there has just been a regular elimination) for truths all of whose candidates are linked to a candidate not in the truth (i.e. L*T!, allowing elimination of that candidate) and also pairs of arrows whose left-hand sides intersect and whose right-hand sides are disjoint and pairwise linked (allowing elimination of the candidates in the intersection of the arrows' left-hand sides: basically a generalisation of five-component AICs). Also, when a new arrow is derived, I check whether any existing arrow (or any other new arrow) has the same RHS, and if so I merge them at once (so effectively collapsing LTA+AAA or ALA+AAA or AAA+AAA into a single derivation with three premises, in the special case where the AAA rule has B, C and H all null). (Note that this does not trigger a return to step 1, since it's not an elimination.) It is of course possible to add more such shortcuts (after proving that they are implied by the ATLC rules), but I haven't identified any that I think would save much time.
Another thing I exploit in order to speed up the code is that, even though any letter in any rule can be null (i.e., represent zero candidates), in reality some letters can be assumed to be non-null, because if they were null then the derived assertion would be trivially implied by one of the premises (or even be a truism).
1) Construct a list of the truths and links directly described by the current PM grid (candidates referring to the same cell; candidates referring to the same number for cells all within a given unit). Mark all truths as live/used and all links as live/unused.
2) Pick a live/unused assertion P. Mark P as live/used. (Which we choose only affects speed.)
3) Generate all the new assertions arising from applying resolution rules to P and some live/used assertion - or, in the case of LLLL, to P and some pair of live/used assertions.
4) If any new assertion is an arrow with empty RHS or a single-candidate truth, remove all relevant candidates from the grid, do Singles and return to 1.
5) Discard any new assertion that is implied by another new assertion or by some existing live (used or unused) assertion.
6) Mark as dead any existing assertion (used or unused) that is implied by any remaining new assertion. (Keep hold of these, though, for reporting of the proof of any future elimination.)
7) Add any remaining new assertions as live/unused; store their premises for later reporting.
8) If there are any live/unused assertions (new or pre-existing), return to 2.
9) Halt. If there are still some live/used assertions, that means the final PM grid has resisted ATLC. Otherwise, i.e. if there are no live assertions, then there must also be no surviving candidates, i.e. the puzzle has been solved.
In my current code, to speed things up I do more than Singles at step 4: I also check (but only if there has just been a regular elimination) for truths all of whose candidates are linked to a candidate not in the truth (i.e. L*T!, allowing elimination of that candidate) and also pairs of arrows whose left-hand sides intersect and whose right-hand sides are disjoint and pairwise linked (allowing elimination of the candidates in the intersection of the arrows' left-hand sides: basically a generalisation of five-component AICs). Also, when a new arrow is derived, I check whether any existing arrow (or any other new arrow) has the same RHS, and if so I merge them at once (so effectively collapsing LTA+AAA or ALA+AAA or AAA+AAA into a single derivation with three premises, in the special case where the AAA rule has B, C and H all null). (Note that this does not trigger a return to step 1, since it's not an elimination.) It is of course possible to add more such shortcuts (after proving that they are implied by the ATLC rules), but I haven't identified any that I think would save much time.
Another thing I exploit in order to speed up the code is that, even though any letter in any rule can be null (i.e., represent zero candidates), in reality some letters can be assumed to be non-null, because if they were null then the derived assertion would be trivially implied by one of the premises (or even be a truism).
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:33 pm
RESULTS. Well, I'm pretty excited by my algorithm's performance. It's coded in Mathematica, and my only hardware is a reasonably standard-issue MacBook, so I've only tested about 500 puzzles so far, but...
First I tried all the examples in the help pages on Andrew Stuart's site sudokuwiki.org. I really only used those for debugging, because I was pretty confident that ATLC would solve everything there except things that relied on deadly patterns. In fact, though, it actually solved everything including the deadly-pattern cases (and other oddities such as 3D Medusa and BUGs), quickly, except for the Exocet example:
090000030200000000003010907006000000000060370000108006008030001007080003000400050
of which more below. The examples for all the patterns that I had feared might resist ATLC, such as SK loops or fireworks or pattern overlay, also yielded.
So then I moved on to the so-called "unsolvables" on Andrew's site, whose SE rankings are not provided so I'm guessing a lot of them are under 10 and maybe not even in T&E(Singles 2), but which don't yield to any of the patterns included in his online solver. I started archiving them several months ago, so I was able to start at #500. I was astonished to find that my code found solutions for all of these too (mostly in minutes, though a few took several hours). I should note that my timings stated here and below should be taken with a bit of a pinch of salt, because it wasn't until rather late in this testing process that I finally fixed a memory-leak issue that had been slowing the program down several-fold (and had also made it crash before cracking the hardest cases).
So... I tried Escargot, and it succumbed quite quicky... so I went back to that Exocet case above, and the program solved it too, though only after several hours. (Note, however, that it may have done so by a route other than Exocet per se; see below.) So I then tried Inkala's second puzzle (what is its SER?):
800000000003600000070090200050007000000045700000100030001000068008500010090000400
and it took more than a day but my algorithm eventually found a complete solution.
So... I moved on to ph_2010. Since my implementation took several hours to get through the sudokuwiki "unsolvables", of which there are 137 that I have accessed, I wanted a sample of about that same number of cases. So as to ensure good diversity, I sorted 02_index.txt and picked the first of each set defined by leading substring terminated at the fifth digit. This gave me 128 puzzles with SER between 10.3 and 11.3. As I'd expected, since they've already been filtered to have a high SER, these were a great deal more challenging than the unsolvables. However, they have slowly but surely yielded; after a total execution time of about a week using 16 cores, the program found solutions for all of them, and indeed only a few lasted more than a day.
One thing I've been looking out for is a "wall of death", where every (or almost every) elimination that's found is found in at most N hours and then any puzzle that survives sees no further eliminations for, say, 10N hours. That would be reasonable evidence that there's no way for ATLC to proceed, even though the algorithm has not run to completion. But I haven't seen that - I'm seeing a pretty smooth exponential decay of how long a solution takes to be found, with some eliminations (including for the lower-SER cases) cropping up only after many hours of effort.
An intriguing observation is that a very high proportion (nearly half) of the puzzles with SER exactly 11.0 took a particularly long time, and that the difficult stage was very late, i.e. when the number of remaining candidates had fallen below 180 (several below 150, in fact) - a point from which no other puzzles have survived more than ten minutes or so. The three longest holdouts from the entire set of 128 were in this group. A cursory inspection indicates that these may be tridagons, but I'm not sufficiently familiar with those to know for sure.
Since everything with SER 10.5 and lower was solved fairly fast but there were very few test cases with SER 10.3 or 10.4 (1 and 4 respectively, as against 45 with SER 10.5), I then tested 40-45 cases with each of those two SERs - every 3000th line from 01_file1.txt for each, to be precise. It demolished almost all of them in 24 hours and the rest in another day or so, and I again did not see any wall of death (some of the eliminations took many hours to be discovered, one of them over a day), so I feel this is good enough evidence that we don't need to go to SER lower than 10.6 in order to explore the limits of what ATLC can do. Perhaps this can in fact be proved by reference to the rules that SE uses to assign SER values, but I don't have a list of such rules; I'd be delighted if someone here can help with that. Indeed, since all 38 puzzles that I sampled at 10.6 through 10.9 also yielded, maybe puzzles of those SERs can also be proven never to resist.
Anyway, so of course I finally attacked the nine famous puzzles rated at 11.9. And... I've sure had to be patient, but every one of them has been solved. These are, in increasing order of time to solve, the puzzles with indices 4, 2 ("second flush"), 11523, 6, 5, 248078, 1 (champagne dry), 3 (Golden Nugget) and 1744614 - which was a good deal slower than any of the others. Has that puzzle previously been thought to be uniquely hard?
Also I remembered that "Easter Monster" is a particularly famous puzzle, so I pulled it out along with all the other ones that have interesting names (Lightsaber, Silver_Plate, Bronze_Medalian, Cloudy_Bay), just in case anyone here has particular interest. THe program solved them all; unexpectedly (to me!), Bronze_Medalian took by far the longest, followed by Silver_Plate.
To give some reality to this, I'm putting my Mathematica notebook including the program's proof for the first Golden Nugget elimination, consisting of a DAG with 681 nodes, in the next post - as both the Mathematica notebook and a plain text document for anyone Mathematica-lly challenged. I should stress that this particular elimination is relatively benign, in that it was found in only about ten minutes, as against many hours for some other ones; I'm therefore guessing, though I haven't checked, that the hardest ones have at least 100,000 nodes.
Notes on the proof:
1) Each line lists the premises and then the derivation, first by index in the internal list of assertions, then spelled out as candidates. All premises in a given line are derived (or directly described by the PM grid) in earlier lines. I use indentation to denote steps in the logic: in other words, each line is indented by one more space than the greatest indentation of any premise.
2) The short-cut of merging arrows whose RHSs are the same results in a lot of collapsing of two derivations into one (with three premises), which for simplicity I just denote by the fake rule names "LTAA", "ALAA" and "AAAA".
3) Arrows often end up with really long LHSs; there's nothing I can see to do about that with AAA (or with LTAA etc), but with ATT and ALA I just print the arrow premise's number of candidates that are encompassed by "B", since candidates in B play no role in those rules' logic and do not appear in the derived truth.
4) The last line in a proof is the elimination itself, denoted by "LT!" or "AL!" depending whether the null-RHS arrow arose using LTA or ALA respectively.
I'm sure I can improve this format! - please shout if you need it explained further. Since the difficult eliminations are really long, I have a variable "printproofs" which specifies how many eliminations to print the proofs of, after which the program just prints the eliminations themselves and the updated grid. Setting printproofs=-1 makes the program quit the puzzle entirely after finding (and printing the proof of) the first elimination. The notebook I'm posting has printproofs=-1; it examines only two puzzles, an easy one (a recent sudokuwiki "unsolvable", though actually that specific elimination is found by Andrew's solver) just so that you have a simple example to look at, and then Golden Nugget itself.
First I tried all the examples in the help pages on Andrew Stuart's site sudokuwiki.org. I really only used those for debugging, because I was pretty confident that ATLC would solve everything there except things that relied on deadly patterns. In fact, though, it actually solved everything including the deadly-pattern cases (and other oddities such as 3D Medusa and BUGs), quickly, except for the Exocet example:
090000030200000000003010907006000000000060370000108006008030001007080003000400050
of which more below. The examples for all the patterns that I had feared might resist ATLC, such as SK loops or fireworks or pattern overlay, also yielded.
So then I moved on to the so-called "unsolvables" on Andrew's site, whose SE rankings are not provided so I'm guessing a lot of them are under 10 and maybe not even in T&E(Singles 2), but which don't yield to any of the patterns included in his online solver. I started archiving them several months ago, so I was able to start at #500. I was astonished to find that my code found solutions for all of these too (mostly in minutes, though a few took several hours). I should note that my timings stated here and below should be taken with a bit of a pinch of salt, because it wasn't until rather late in this testing process that I finally fixed a memory-leak issue that had been slowing the program down several-fold (and had also made it crash before cracking the hardest cases).
So... I tried Escargot, and it succumbed quite quicky... so I went back to that Exocet case above, and the program solved it too, though only after several hours. (Note, however, that it may have done so by a route other than Exocet per se; see below.) So I then tried Inkala's second puzzle (what is its SER?):
800000000003600000070090200050007000000045700000100030001000068008500010090000400
and it took more than a day but my algorithm eventually found a complete solution.
So... I moved on to ph_2010. Since my implementation took several hours to get through the sudokuwiki "unsolvables", of which there are 137 that I have accessed, I wanted a sample of about that same number of cases. So as to ensure good diversity, I sorted 02_index.txt and picked the first of each set defined by leading substring terminated at the fifth digit. This gave me 128 puzzles with SER between 10.3 and 11.3. As I'd expected, since they've already been filtered to have a high SER, these were a great deal more challenging than the unsolvables. However, they have slowly but surely yielded; after a total execution time of about a week using 16 cores, the program found solutions for all of them, and indeed only a few lasted more than a day.
One thing I've been looking out for is a "wall of death", where every (or almost every) elimination that's found is found in at most N hours and then any puzzle that survives sees no further eliminations for, say, 10N hours. That would be reasonable evidence that there's no way for ATLC to proceed, even though the algorithm has not run to completion. But I haven't seen that - I'm seeing a pretty smooth exponential decay of how long a solution takes to be found, with some eliminations (including for the lower-SER cases) cropping up only after many hours of effort.
An intriguing observation is that a very high proportion (nearly half) of the puzzles with SER exactly 11.0 took a particularly long time, and that the difficult stage was very late, i.e. when the number of remaining candidates had fallen below 180 (several below 150, in fact) - a point from which no other puzzles have survived more than ten minutes or so. The three longest holdouts from the entire set of 128 were in this group. A cursory inspection indicates that these may be tridagons, but I'm not sufficiently familiar with those to know for sure.
Since everything with SER 10.5 and lower was solved fairly fast but there were very few test cases with SER 10.3 or 10.4 (1 and 4 respectively, as against 45 with SER 10.5), I then tested 40-45 cases with each of those two SERs - every 3000th line from 01_file1.txt for each, to be precise. It demolished almost all of them in 24 hours and the rest in another day or so, and I again did not see any wall of death (some of the eliminations took many hours to be discovered, one of them over a day), so I feel this is good enough evidence that we don't need to go to SER lower than 10.6 in order to explore the limits of what ATLC can do. Perhaps this can in fact be proved by reference to the rules that SE uses to assign SER values, but I don't have a list of such rules; I'd be delighted if someone here can help with that. Indeed, since all 38 puzzles that I sampled at 10.6 through 10.9 also yielded, maybe puzzles of those SERs can also be proven never to resist.
Anyway, so of course I finally attacked the nine famous puzzles rated at 11.9. And... I've sure had to be patient, but every one of them has been solved. These are, in increasing order of time to solve, the puzzles with indices 4, 2 ("second flush"), 11523, 6, 5, 248078, 1 (champagne dry), 3 (Golden Nugget) and 1744614 - which was a good deal slower than any of the others. Has that puzzle previously been thought to be uniquely hard?
Also I remembered that "Easter Monster" is a particularly famous puzzle, so I pulled it out along with all the other ones that have interesting names (Lightsaber, Silver_Plate, Bronze_Medalian, Cloudy_Bay), just in case anyone here has particular interest. THe program solved them all; unexpectedly (to me!), Bronze_Medalian took by far the longest, followed by Silver_Plate.
To give some reality to this, I'm putting my Mathematica notebook including the program's proof for the first Golden Nugget elimination, consisting of a DAG with 681 nodes, in the next post - as both the Mathematica notebook and a plain text document for anyone Mathematica-lly challenged. I should stress that this particular elimination is relatively benign, in that it was found in only about ten minutes, as against many hours for some other ones; I'm therefore guessing, though I haven't checked, that the hardest ones have at least 100,000 nodes.
Notes on the proof:
1) Each line lists the premises and then the derivation, first by index in the internal list of assertions, then spelled out as candidates. All premises in a given line are derived (or directly described by the PM grid) in earlier lines. I use indentation to denote steps in the logic: in other words, each line is indented by one more space than the greatest indentation of any premise.
2) The short-cut of merging arrows whose RHSs are the same results in a lot of collapsing of two derivations into one (with three premises), which for simplicity I just denote by the fake rule names "LTAA", "ALAA" and "AAAA".
3) Arrows often end up with really long LHSs; there's nothing I can see to do about that with AAA (or with LTAA etc), but with ATT and ALA I just print the arrow premise's number of candidates that are encompassed by "B", since candidates in B play no role in those rules' logic and do not appear in the derived truth.
4) The last line in a proof is the elimination itself, denoted by "LT!" or "AL!" depending whether the null-RHS arrow arose using LTA or ALA respectively.
I'm sure I can improve this format! - please shout if you need it explained further. Since the difficult eliminations are really long, I have a variable "printproofs" which specifies how many eliminations to print the proofs of, after which the program just prints the eliminations themselves and the updated grid. Setting printproofs=-1 makes the program quit the puzzle entirely after finding (and printing the proof of) the first elimination. The notebook I'm posting has printproofs=-1; it examines only two puzzles, an easy one (a recent sudokuwiki "unsolvable", though actually that specific elimination is found by Andrew's solver) just so that you have a simple example to look at, and then Golden Nugget itself.
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:33 pm
NEXT STEPS. So, well, the question inescapeably arises: is ATLC omnipotent? Does it (eventually!) derive an elimination from ANY valid PM grid (or indeed sukaku)?
Here I've come up against an issue of compute power. The underlying reason why the execution times are so long is that the resolution rules can often derive many thousands of assertions, even not counting trivially-implied ones, and hard PM grids tend to require quite long resolution paths. Some of the cases above are still going after a few days, but they are still generating new assertions; I haven't been able to get anywhere close to running out of pairs of assertions to try to derive new assertions from. My algorithm is based on an acknowledgement of this: I have a FAIRLY good heuristic for which pairs of assertions are good to use as premises, but it's far from perfect, so basically I just choose randomly among the more promising-looking ones, and after a certain point I give up and start again because there are too many live/used assertions to juxtapose each new P with.
Thus, irritatingly, I'm not currently in a position to get a definite negative answer (a PM grid from which ATLC can't derive any eliminations); all I can do is see how many positive answers (solutions) I get, and whether the ratio of solved (and time to solve) to undecided correlates with SER, BxB etc. Also, the same puzzle often takes rather different amounts of time to be solved when I do multiple runs on it. The implication is that most if not all puzzles succumb to ATLC, just that some have more routes to a solution than others. But of course that says nothing about whether it's "all" or only "most".
Of course if the solutions that ARE found were found much more quickly, I could throw the program at a lot more puzzles, and the longer its empirical omnipotence persists, the more likely it becomes that it really is omnipotent. But I think I've sped it up as much as I can.
Hence I feel that now is the right time to appeal to this group for help, in any of the following forms:
1) really serious hardware
2) willingness to reimplement my algorithm in a language that's much faster than Mathematica
3) insights on how to guess promising pairs of assertions much better than I'm doing. Currently the only thing I'm taking into account is the number of candidates in the assertion (or in each side of the assertion in the case of arrows). Is there something smarter?
4) some other big improvement of my algorithm
5) identification of proofs that specific patterns are within ATLC's scope, just really hard to find (of which Exocets and tridagons are prime candidates at present). All other patterns known to me (other than deadly patterns) are pretty easy to prove as within ATLC's scope, but they are also pretty easy for the algorithm to find without a hard-coded shortcut, so the only ones I've added are L*T! and the arrow-arrow-link pattern, which are fast enough to be worth it (see ALGORITHM).
6) an analytical approach that could prove or disprove the omnipotence of ATLC (maybe a generalisation of braids?)
7) a determination of whether TLC and ATLC are in fact equal in power. This is what I will probably work on next. I described above a proof that ATLC is at least as powerful as TLC, but whether it's strictly more powerful is far from obvious to me, because the use of L*T! with more than two links definitely makes TLC more powerful than braids. ATLC is probably preferable even if the two RTs are equivalent, simply because all but one rule having only two premises makes the search far faster - but this would still be good to know.
8) scrutiny of the proofs of eliminations, to identify new patterns that directly deliver eliminations. I don't know how feasible that is, but the rapid demolition of all the (hitherto!) unsolvable puzzles at sudokuwiki.org suggests that those are a good place to start - there will be plenty of points during the process where Andrew's solver runs out of ideas but the proof found by my program is not all that big.
Another thing I propose to do, in concert with any help of the above forms, is to create/maintain a database of PM grids from which ATLC has tried but (so far!) failed to eliminate any candidate. I think that will be much more useful for exploring ATLC than a database of puzzles.
Any takers? I will of course be very happy to contribute in any way I can. I will attach my Mathematica notebook to the next post, with apologies for my perhaps idiosyncratically dense coding format and for any over-conciseness of comments.
Here I've come up against an issue of compute power. The underlying reason why the execution times are so long is that the resolution rules can often derive many thousands of assertions, even not counting trivially-implied ones, and hard PM grids tend to require quite long resolution paths. Some of the cases above are still going after a few days, but they are still generating new assertions; I haven't been able to get anywhere close to running out of pairs of assertions to try to derive new assertions from. My algorithm is based on an acknowledgement of this: I have a FAIRLY good heuristic for which pairs of assertions are good to use as premises, but it's far from perfect, so basically I just choose randomly among the more promising-looking ones, and after a certain point I give up and start again because there are too many live/used assertions to juxtapose each new P with.
Thus, irritatingly, I'm not currently in a position to get a definite negative answer (a PM grid from which ATLC can't derive any eliminations); all I can do is see how many positive answers (solutions) I get, and whether the ratio of solved (and time to solve) to undecided correlates with SER, BxB etc. Also, the same puzzle often takes rather different amounts of time to be solved when I do multiple runs on it. The implication is that most if not all puzzles succumb to ATLC, just that some have more routes to a solution than others. But of course that says nothing about whether it's "all" or only "most".
Of course if the solutions that ARE found were found much more quickly, I could throw the program at a lot more puzzles, and the longer its empirical omnipotence persists, the more likely it becomes that it really is omnipotent. But I think I've sped it up as much as I can.
Hence I feel that now is the right time to appeal to this group for help, in any of the following forms:
1) really serious hardware
2) willingness to reimplement my algorithm in a language that's much faster than Mathematica
3) insights on how to guess promising pairs of assertions much better than I'm doing. Currently the only thing I'm taking into account is the number of candidates in the assertion (or in each side of the assertion in the case of arrows). Is there something smarter?
4) some other big improvement of my algorithm
5) identification of proofs that specific patterns are within ATLC's scope, just really hard to find (of which Exocets and tridagons are prime candidates at present). All other patterns known to me (other than deadly patterns) are pretty easy to prove as within ATLC's scope, but they are also pretty easy for the algorithm to find without a hard-coded shortcut, so the only ones I've added are L*T! and the arrow-arrow-link pattern, which are fast enough to be worth it (see ALGORITHM).
6) an analytical approach that could prove or disprove the omnipotence of ATLC (maybe a generalisation of braids?)
7) a determination of whether TLC and ATLC are in fact equal in power. This is what I will probably work on next. I described above a proof that ATLC is at least as powerful as TLC, but whether it's strictly more powerful is far from obvious to me, because the use of L*T! with more than two links definitely makes TLC more powerful than braids. ATLC is probably preferable even if the two RTs are equivalent, simply because all but one rule having only two premises makes the search far faster - but this would still be good to know.
8) scrutiny of the proofs of eliminations, to identify new patterns that directly deliver eliminations. I don't know how feasible that is, but the rapid demolition of all the (hitherto!) unsolvable puzzles at sudokuwiki.org suggests that those are a good place to start - there will be plenty of points during the process where Andrew's solver runs out of ideas but the proof found by my program is not all that big.
Another thing I propose to do, in concert with any help of the above forms, is to create/maintain a database of PM grids from which ATLC has tried but (so far!) failed to eliminate any candidate. I think that will be much more useful for exploring ATLC than a database of puzzles.
Any takers? I will of course be very happy to contribute in any way I can. I will attach my Mathematica notebook to the next post, with apologies for my perhaps idiosyncratically dense coding format and for any over-conciseness of comments.
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:37 pm
OK, I'm having trouble attaching files, I'm getting "Sorry, the board attachment quota has been reached", so I will resort to pasting. Here is the proof of the easier elimination:
*** ELIMINATION from 001000700600800020000010069080904002000035000900000600050000903040000050008070000
candidate 40 aka B6=9 leaving 202 candidates after 2791 total asses 08:55:31
*** ELIMINATION from 001000700600800020000010069080904002000035000900000600050000903040000050008070000
candidate 40 aka B6=9 leaving 202 candidates after 2791 total asses 08:55:31
Hidden Text: Show
Last edited by ag24ag24 on Mon Mar 24, 2025 8:25 pm, edited 1 time in total.
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:39 pm
And here's the proof of the first elimination from Golden Nugget, split into two posts because of the 100,000-character limit:
Hidden Text: Show
Last edited by ag24ag24 on Mon Mar 24, 2025 8:26 pm, edited 1 time in total.
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:41 pm
Second half of the Golden Nugget elimination proof. I'll wait to post the code until someone tells me how.
Hidden Text: Show
Last edited by ag24ag24 on Mon Mar 24, 2025 8:27 pm, edited 1 time in total.
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 4:43 pm
Hm, I see that the system has removed all the indentation from the proofs. Ah well.
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by rjamil » Mon Mar 24, 2025 7:14 pm
Hi ag24ag24
If you wish to keep all your indentation, you need to write your text under [ code ] [ /code ] block as follows:
R. Jamil
ag24ag24 wrote:Hm, I see that the system has removed all the indentation from the proofs. Ah well.
If you wish to keep all your indentation, you need to write your text under [ code ] [ /code ] block as follows:
- Code: Select all
Hi,
Hope you are now understand correctly.
R. Jamil
- rjamil
- Posts: 830
- Joined: 15 October 2014
- Location: Karachi, Pakistan
Re: A concise and seemingly omnipotent Sudoku resolution the
by nazaz » Mon Mar 24, 2025 7:34 pm
You might also stuff the "code" block inside a "hidden" block, to be easier on the eyes, by editing your posts to look like this:
As to the main topic: it would be interesting to see examples of puzzles that don't yield to TLC. Those puzzles are "hard" in some sense. I'm curious to know if they are "hard" with respect to the usual set of sudoku-solving techniques as well, e.g. as measured by SER.
If you can prove that ATLC (or perhaps even TLC) is complete w.r.t. single-solution sudoku grids, that would be something new.
- Code: Select all
[hidden][code]
your
enormous
proof
[/code][/hidden]
As to the main topic: it would be interesting to see examples of puzzles that don't yield to TLC. Those puzzles are "hard" in some sense. I'm curious to know if they are "hard" with respect to the usual set of sudoku-solving techniques as well, e.g. as measured by SER.
If you can prove that ATLC (or perhaps even TLC) is complete w.r.t. single-solution sudoku grids, that would be something new.
-
nazaz - Posts: 36
- Joined: 06 November 2018
Re: A concise and seemingly omnipotent Sudoku resolution the
by ag24ag24 » Mon Mar 24, 2025 8:15 pm
Many thanks for the indentation workaroound - I'll use that in future.
Clearly the ultimate goal is indeed to prove that ATLC (or perhaps even TLC) is complete w.r.t. single-solution sudoku grids, but at ths point a way to do that is way beyond me. However, I'm proposing that the empirical fact that ATLC can solve lots of puzzles that are agreed to be exceptionally hard is also something new (and interesting enough to explore).
Clearly the ultimate goal is indeed to prove that ATLC (or perhaps even TLC) is complete w.r.t. single-solution sudoku grids, but at ths point a way to do that is way beyond me. However, I'm proposing that the empirical fact that ATLC can solve lots of puzzles that are agreed to be exceptionally hard is also something new (and interesting enough to explore).
- ag24ag24
- Posts: 37
- Joined: 19 July 2024
Re: A concise and seemingly omnipotent Sudoku resolution the
by nazaz » Mon Mar 24, 2025 8:19 pm
I think exploring TLC would be more interesting. You've got a chance of finding puzzles both provable and not. What distinguishes those two classes?
Please edit your earlier post to place "hidden" and "code" tags around the giant proof.
Please edit your earlier post to place "hidden" and "code" tags around the giant proof.
Last edited by nazaz on Mon Mar 24, 2025 8:22 pm, edited 1 time in total.
-
nazaz - Posts: 36
- Joined: 06 November 2018
48 posts
• Page 1 of 4 • 1, 2, 3, 4
