Sudoku Players' Forum (clone)

.
Today's update on GitHub includes
- cosmetic changes with no consequence for the user (fusion of the code for the blocked and non-blocked versions of chain rules)

- addition of blocked versions for z-chains (typed or not)

- addition of blocked versions for oddagons

- update of the User Manual to reflect these changes

(Reminder: blocked versions of rules allow to make all the eliminations valid for a pattern, before a simpler rule made available by the first eliminations may be applied.
Blocked versions of rules are important when trying to reduce the number of steps in a resolution path.)

.
Today's (early morning) update on GitHub brings a single (but IMO very useful) novelty: the possibility of setting preferences among groups of rules.

Another change is the publication (and inclusion in the Docs folder) of the Second Edition of the Basic User Manual [BUM2]. It includes all the changes (mainly additions) made since the first release of CSP-Rules-V2.1 and listed in the previous posts. Notice that the core of CSP-Rules (say the resolution rules and the basic simplest-first strategy) hasn't been changed and that's why it has remained V2.1 all the time. What has been added is possibly useful user functions.


As an example of using preferences, take Myth's puzzle (see more details in [BUM2]):

Code: Select all

     +-------+-------+-------+
     ! . . . ! . . . ! 1 . . !
     ! . . 1 ! 2 . . ! . . 3 !
     ! . 4 . ! . 5 . ! . 2 . !
     +-------+-------+-------+
     ! . 5 . ! . 6 . ! . 4 . !
     ! . . 7 ! 3 . . ! . . 6 !
     ! . . . ! . . 7 ! 3 . . !
     +-------+-------+-------+
     ! 2 . . ! . . . ! . . . !
     ! . . 8 ! 7 . . ! . . 1 !
     ! . 6 . ! . 4 . ! . 5 . !
     +-------+-------+-------+
......1....12....3.4..5..2..5..6..4...73....6.....73..2..........87....1.6..4..5.

As Myth is known for providing puzzles with exceptionally many Subsets and Finned Fish, it is natural to want to find as many of them as possible before we try any other rules.
Before this update there was only one possibility and that involved two stages:
1) load SudoRules with only Subsets and Finned Fish, use function "solve" and get the final resolution state thus obtained.
2) load SudoRules with the previous rules plus whatever chains you want and apply function "solve-sukaku-grid" to the resolution state previously obtained.
Of course, this remains possible (and it remains the most versatile way of doing this).

However, all this can be automated and even improved (if you don't want to specify improbable sets of rules), because you can specify a whole sequence of sets of rules in order to obtain what you want with a single function call. Load SudoRules with whatever set of rules you want to finally allow and use function "solve-w-preferences" to specify your own hierarchy of resolution theories to be tried.

In particular, if you don’t know in advance what will be enough to solve a puzzle, you may want to restrict the increase in rules complexity before allowing all the loaded rules to apply, you can write e.g.:

Code: Select all

(solve-w-preferences
   "......1....12....3.4..5..2..5..6..4...73....6.....73..2..........87....1.6..4..5."
   S4Fin BIVALUE-CHAINS REVERSIBLE-CHAINS REVERSIBLE-PATTERNS
)

This function will apply all the Subsets and Finned Fishes before any other rule (and in the present case, it will find a big Jellyfish that function "solve" couldn't find if bivalue-chains were loaded). If the puzzle is not solved, it will the try BIVALUE-CHAINS and then REVERSIBLE-CHAINS ... At the end, if the puzzle is not yet solved, it will try all the rules loaded (defined in the configuration file).
In this example, it will merely stop after BIVALUE-CHAINS.

See the User Manual for the predefined resolution theories allowed as preferences and the exact meaning of each symbol for them.
Note that within each preferred resolution theory, the simplest-first strategy continues to apply.
If you type a symbol not allowed, the function will stop after telling you the allowed list (available in the manual).
If the list of preferences is empty, the function works as "solve".
There are similar functions for dealing with the other puzzle formats and for sukakus.

.

a user of CSP-Rules wrote:On GitHub, you write that CSP-Rules is a general solver of finite Constraint Satisfaction Problems.
SudoRules being the application of CSP-Rules to Sudoku, does that imply that SudoRules is a general solver of Sudokus?

The word "general" can be understood in many ways.

1) First, what I wrote on GitHub is more precisely: CSP-Rules is a general pattern-based solver of finite Constraint Satisfaction Problems.
To be still more precise, I should have written what I wrote in many other places: CSP-Rules is a general pattern-based solver of finite binary Constraint Satisfaction Problems.
Each word is important.

"Finite" implies in particular that CSP-Rules cannot deal with CSPs with continuous CSP-Variables; they require very different techniques.

"Binary" means that all the constrains of the CSP are binary and can therefore be interpreted as binary contradictions between candidates. That is essential to the definition of chain rules. I have however shown in [PBCS] that many CSPs that don't appear to be binary in their original formulation (such as Kakuro, Futoshiki, Slitherlink...) can be efficiently turned into binary ones by adding application-specific CSP-Variables.

Of course, the above two conditions are satisfied in Sudoku.

"Pattern-based" is probably the most important qualification. There are lots of general CSP solvers with a main/only goal of producing a solution as fast as possible. This is very useful in many CSPs and this is also essential when the solver has to be used as part of a generator.
Contrary to such solvers, CSP-Rules main goal is to produce an understandable solution, with a justification of each step by a predefined resolution rule, i.e. to produce a readable resolution path in addition to a solution. This is a radically different (and computational much harder) problem.
[CSP-Rules is also "pattern-based" in a second sense: it is coded in a pattern-based way (and, AFAIK, it is the only such solver).]

"General" means that, apart from the above restrictions, CSP-Rules can be applied to any CSP.
Obviously, this must be tempered by practical considerations about memory and computation times, depending on CSP size - as in any other CSP solver.


2) Now, about SudoRules being general: choose your meaning of "general" to get your answer.
It is a general Sudoku solver in the above sense.
It is also general in the sense that it can solve any puzzle solvable by a human (and very much harder ones).

It is not "general" in the sense of including all the popular patterns. Although it has rules for patterns specific to Sudoku, both general ones (Subsets, Finned-Fish) and "exotic" ones (sk-loops, J-Exocets, UR, BUGS...), only the basic versions of these rules are included (and not their myriad possible variants).


Notice that there are many other "general" Sudoku solvers that produce full resolution paths. However, AFAIK, SudoRules is the only one that is "pattern-based" all the way down to its code: the resolution rules are the code.
One consequence is, it makes it very difficult to include behaviours that are not pattern-based (generally requiring some form of T&E, be it for a human solver or a machine), e.g.:
- finding resolution paths with few steps;
- writing variants of rules that require additional, situation-dependent checks (e.g. checking some additional contradictions in non-J exocets).
.

same user of CSP-Rules wrote:

denis_berthier wrote:.b]2)[/b] Now, about SudoRules being general: choose your meaning of "general" to get your answer.
It is a general Sudoku solver in the above sense.
It is also general in the sense that it can solve any puzzle solvable by a human (and very much harder ones).
It is not "general" in the sense of including all the popular patterns. Although it has rules for patterns specific to Sudoku, both general ones (Subsets, Finned-Fish) and "exotic" ones (sk-loops, J-Exocets, UR, BUGS...), only the basic versions of these rules are included (and not their myriad possible variants).

You coded many specific rules for Slitherlink. But Sudoku is much more popular than Slitherlink. Why don't you do the same for Sudoku?

Good point.
In my first (unpublished) version of Slitherlink, there were only:
- generic rules (bivalue-chains, z-chains, whips, braids) inherited from CSP-Rules with no additional coding,
- Quasi-loops, taking into account the global only-one-loop constraint.
This was enough to solve almost all of the puzzles I could find/generate on the web.
In the config file, you can still choose to use only these rules.
However, when I found the slinkier list of rules (first, via its plagiarised form in Wikipedia), I was curious to see how they related to the generic ones. I started to code a few of them and I noticed most of them were definable in terms of sequences of whips[1]. The more I continued, the more my observations were confirmed. From the POV of resolution power, it was quite frustrating (no RoI for the time invested), but it finally proved to be very positive as it led me to introduce the notion of macro-rules and I could use SlitherRules as a (specialised) assistant theorem prover to prove the corresponding subsumption theorems.


As for Sudoku, I have formally proven many subsumption theorems in [PBCS] and I don't feel like coding e.g. all the WXYZLGBTQRSTUV... special cases of them.
For exotic patterns (sk-loops, J-Exocets, exotic fish) that are very rarely useful, I don't see the point of coding variants of variants of them. But anyone interested can easily do it.

Subsets have a special place: they have a generic definition in [PBCS], but no generic implementation in CSP-Rules. For efficiency reasons, they have specific implementations (not very different from one application to another) in each application that has Subsets.


The question is interesting because it is related to the main purpose of CSP-Rules: it is a generic solver of finite CSPs that relies on a small set of rules sufficiently simple to be remembered by anyone and powerful enough to solve all the puzzles a human solver would want to solve.
This is why I've included for illustration purposes applications to various logic puzzles with extremely different types of constraints.
A relatively recent addition to the generic rules can also illustrate this approach: oddagons. This exotic chain pattern seemed to be Sudoku-specific, but it turned out to have a generic formulation.

.
I added the 3rd edition of my book "Pattern-Based Constraint Satisfaction and Logic Puzzles".
You can find it in the "Publications" folder.
It is also available on Researchgate: https://www.researchgate.net/publication/356313228_Pattern-Based_Constraint_Satisfaction_and_Logic_Puzzles_Third_Edition
.

.
Today's update on GitHub consists of the addition of the Tridagon elimination rule (also "trivalue-oddagon or Thor's Hammer", names I don't like). See http://forum.enjoysudoku.com/the-tridagon-rule-t39859.htmlfor my definition of it.
It includes the rule itself, the necessary additions of a global variable ?*Tridagon* for selecting this rule in the configuration file and examples (of the Loki family).

An update to the User Manual will come later.
For those who already know the pattern, the only thing you need to know for using this rule is: set ?*Tridagon* to True in the "Exotic" part of the configuration file.
Tridagons are a very rare pattern, so don't expect to find it in your daily puzzles.

.
Today's update on GitHub is not what some of you may have been expecting from my last posts: anything related to Tridagons. For these additions, I still need more time for testing my implementation.

The update is related to a stupid typo-bug I've found recently in my code for "ordinary" forcing-chains. It also includes an update for the FW ratings of the full cbg-000 collection in the Examples/Sudoku" folder and of the related "comparisons.txt" and "comparisons.rtf" files. The conclusions I reached before his bug are unchanged: forcing-whips are rarely useful.

.
I've just published on GitHub the rules for finding the Tridagon-links introduced here: http://forum.enjoysudoku.com/the-tridagon-rule-t39859-25.html

Notes:
- The Tridagon elimination rule was already published.
- I'll soon publish the Tridagon-Forcing-Whips that allow eliminations based on the above Tridagon-links; but you can already use today's publication to find the Tridagon-links themselves.

.
I've just pushed to GitHub the Tridagon-Forcing-Whips I introduced here: http://forum.enjoysudoku.com/the-tridagon-rule-t39859-31.html

I haven't yet had time to write the corresponding additions to the User Manual, but the general idea is, they are resolution rules like any other resolution rule and they have to be selected in the configuration file, in the part named: Sudoku-specific rules (besides Subsets): uniqueness and "exotic" patterns.
Before trying to use these Tridagon-forcing-whips, it's thus better to read the Tridagon thread: http://forum.enjoysudoku.com/the-tridagon-rule-t39859.html

Beware that if you don't put restrictions on the lengths of whips and Tridagon-Forcing-Whips, computation times can be very long. Whence my recommendation in the config file to increase them progressively.

Note also that, as introduced in a previous post, the TRIDAGONS set of preferences is available for use within function solve-w-preferences, allowing to use all the Tridagons and Tridagon-Forcing-Whips before any normal whip. Depending on puzzles, this works better or worse than normal solve. Which of the two is best in unpredictable.
In the Examples/Sudoku/Tridagons folder, I've added an example (mith-TE3-972#8) where using preferences makes the solution simpler.

Finally, don't forget that Tridagons are an extremely rare exotic pattern and all this is irrelevant to the normal player.

.
Today's update on GitHUb includes:

- an update of the Basic User Manual, adding in particular a section about the already added resolution rules for Tridagons and Tridagon-Forcing-Whips;
- a few examples of applying the above rules (more examples to come later);

- the replacement of the EXAMPLES folder by an independent "CSP-Rules-Examples" repository: https://github.com/denis-berthier/CSP-Rules-Examples. This will allow me to add examples without requiring an update to CSP-Rule itself;
- the addition to CSP-Rules of a global variable ?*CSP-Rules-Examples-Dir* referring to this directory when the "CSP-Rules-Examples" repository is installed as required in a CSP-Rules directory above the CSP-Rules-V2.1 directory; this variable may be useful in particular when dealing with files of puzzles and using the various "solve-file" functions.

.
Big update today on GitHub, related to the recently discussed topics of tridagons and eleven replacement technique.

- addition of two separate sets of preferences: TRIDAGONS and TRIDAGON-FW; they allow a fine control of what one wants to do with tridagon-related rules

- addition of functions for solving with preferences whole files of puzzles

- addition of functions for applying manually the eleven replacement technique

- in the Sudoku configuration file, addition of global variables related to the above additions

- addition of rules for automatically applying eleven replacement in cases "not too far" from to the trivalue oddagon impossible pattern

- update of the Basic User Manual in order to include all the above changes (with all the details not provides here).

.
I've added functions for solving files of sukakus, with self-explaining names.

For Sukaku puzzles given in the 729-character string format (one string per line, with no quotes), with syntax:
- (solve-n-sukakus-after-first-p-from-string-file ?file-name ?p ?n)
- (solve-n-sukakus-after-first-p-from-string-file-excluding ?file-name ?p ?n ?l-out)
?l-out is the list of puzzle numbers (i.e. their line number in the file) that are excluded from the computations

For Sukaku puzzles given in the much more readable list format (one list per line), with syntax:
- (solve-n-sukakus-after-first-p-from-list-file ?file-name ?p ?n)
- (solve-n-sukakus-after-first-p-from-list-file-excluding ?file-name ?p ?n ?l-out)
?l-out is the list of puzzle numbers (i.e. their line number in the file) that are excluded from the computations

In all the cases, the sukaku is pretty-printed (in the visually more appealing grid format) after initialisation of each puzzle.

The [BUM] will be updated later.

.
I've updated the Basic User Manual [BUM] with all the functionalities mentioned in my previous post - and for all the new ones described below.

- All the generic T&E procedures (at depths 1, 2 or 3) have been made sensitive to restrictions on the candidates they may try (at each level). They are totally unchanged in the default case. In and of itself, this only allows new possibilities, but doesn't offer them readily.

- I have added to SudoRules functions related to k-digit patterns:
(solve-k-digit-pattern-string ?k ?string)
(solve-n-grids-after-first-p-from-k-digit-pattern-string-file ?k ?file-name ?p ?n)
(solve-n-grids-after-first-p-from-k-digit-pattern-string-fileexcluding ?k ?file-name ?p ?n $?l-out)
Given a k-digit pattern (in string format) or a file containing a sequence of such patterns, they allow to solve them (e.g. to prove they are contradictory).

When T&E is involved, they restrict the candidates that may be tried at each level to those in the pattern, thus taking advantage of the new generic feature of T&E. By avoiding to try unproductive candidates, this makes these procedures thousands to millions of times faster than standard T&E (depending on T&E-depth).

- As these new features were motivated by eleven's list of contradictory 3-digit patterns (http://forum.enjoysudoku.com/chromatic-patterns-t39885-41.html), I've added the full analysis of this list in the SudoRules directory of https://github.com/denis-berthier/CSP-Rules-Examples. (As previously announced, CSP-Rules examples are now in a separate repository).
This is what allowed to find a single such pattern among 380 that required T&E(3) for the proof of contradiction.

- In https://github.com/denis-berthier/CSP-Rules-Examples, I've also added several proofs of contradiction for the 3-digit trivalue oddagon pattern.
.

.
Minor update:
- added functions for 1-steppers or 2-steppers for puzzles given in grid format: find-sukaku-grid-1-steppers-wrt-W1, find-sukaku-grid-2-steppers-wrt-W1, find-sukaku-1-steppers and find-sukaku-2-steppers
- printing the number of g-candidates, csp-g-links and g-links is now controlled by ?*print-actions* instead of ?*printi-init-details* (more in line with how the printing of candidates, csp-links and links is controlled)
- some (not yet documented) classification functions (for solving files of puzzles) have been renamed (classify-xxx instead of stats-xxx. Such functions are the basis for further statistical studies.

.
The April update on GitHub has introduced the tridagon elimination rule and tridagon-forcing-whips.

Today's update is also all about the tridagon pattern:
- addition of Sudoku-specific rules for detecting the general anti-tridagon pattern (defined here: http://forum.enjoysudoku.com/the-tridagon-rule-t39859-95.html and its guardians and for asserting the corresponding ORk relation;
- addition of generic rules for ORk-Forcing-Whips, k=2,3,4,5 (defined here: http://forum.enjoysudoku.com/or-k-forcing-whips-t40189.html
- corresponding update of the Basic User Manual, with many examples of how to use all of the above.

All these rules make a very powerful way to deal with the known T&E(3) puzzles (i.e. those based on some anti-tridagon pattern).

Notice what's written in the User Manual: when dealing with T&E(3) puzzles, the max size of whips and ORk-Forcing-Whips must be increased progressively in order to avoid combinatorial explosion (the more so as k increases).
There are many ways of using all the rules. See the manual.
Priorities between whips, ORk-Forcing-Whips and the detection of the anti-tridagon-pattern that allows to use them are defined in a way that lets much freedom to the user in terms of minimising the number of guardians vs minimising the length of whips before the first use of the anti-tridagon pattern.

Notice that the previously defined tridagon-forcing-whips are somehow over-ridden by the new ORk-Forcing-Whips. But the priorities are defined differently.