eleven wrote:logel,
please give us a better example.
E.g. can you show your first step to solve "Champagne dry" and explain pattern, lines etc. there ?
- Code: Select all
98.7.....7.....6....6.5.....4...5.3...79..5......2...1..85..9......1...4.....3.2.
eleven wrote:[Added:] "No problem" might be misleading. As you know, i "love" those XSudo pictures with 40 marked cells, 25 base and 21 cover sets, and the "conclusion": xy<>z without any further explanation. But as i see it, the goal here is to find well defined "minimal" solutions rather than reader friendly ones.
denis_berthier wrote:About vocabulary: any of your patterns is a very specific structure. So, the real topic of the thread is not "Universal Elimination Pattern" but "Universal Definition of an Elimination Pattern".
denis_berthier wrote:One can now wonder why you don't include from the start the core (the base set) in the definition instead of using such a convoluted path to reach the same effect (hopefully - because I'm not convinced that your statement, even in its modified form, is true).
In any case, I think your current definition makes it too difficult to check if something is an elimination pattern.
blue wrote:Statements of the first type, are related to "base sets", or "strongly linked (candidate) sets", or "strong links" (for short).
Statements of the second type, are related to "cover sets", or "pairwise weakly linked (candidate) sets", or "weak links" (for short). In Alan Barker's vocabulary, they are just "links", or "link sets".
Statements of the third type, are related to either "CSP variables" (e.g. Denis Berthier's vocabulary), or "Truths" (Alan Barker's vocabulary).
denis_berthier wrote:The problem is naturally formulated in terms of:
1) 81 rc-cells and of values (digits) that must be assigned to them;
2) 324 constraints the values of these cells must satisfy; these can be classified into 4 constraint types (rc, rn, cn, bn).
Now, translated into logic formulae:
- type 1 is expressed in terms of EOO (exactly one of);
- type 2 is expressed in terms of NAND (not and).
The other type of logical relation you consider ("at most one of") never appears (neither in Sudoku nor in the general CSP).
One important aspect of these predicates:
- type 1 appears as non-binary (most of the time);
- type 2 always appears as binary.
denis_berthier wrote:I haven't forgotten the topic of this thread.
The fact that type 1 is (generally) not binary has concrete implications on complexity:
- Sudoku is not a 2-SAT problem and can't therefore be solved by the very efficient 2-SAT solvers.
- for the same reasons, logel means of checking validity of an "elimination pattern" is also not a 2-SAT problem (even if the target is fixed to True). The complexity of checking can't easily be computed in the general case, whereas it can for patterns such as Subsets, g-Subsets, whips and all the oriented chains fauna - which I express by saying that these special (but very general) patterns carry their own proof with them. In my view, a "pattern" that requires a non-obvious checking procedure (testing all the permutations - or all the remaining ones after the target has been fixed to True) does not really qualify as a pattern in any "pure logic" view of solving.
eleven wrote:The daily definition
eleven wrote:logel wrote:But because I see absolutely no reason to modify the problem statement, I reject using uniqueness methods in the solving sequence.
If you like.I know that other people have a different view, but I never heard a sound reasoning.
Here is my point of view:
Sudoku in first line is a game, which is played with the goal to solve it. The play is unfair, when the puzzle is not unique, because no solution can be found without guessing. When you had spent 5 hours trying to solve a multisolution puzzle, you know, why players insist on the uniqueness of puzzles as part of the "problem statement".
(On the other hand i had fun to solve some puzzles, which were declared to be multisolution puzzles, but this i a different game. )
Since your universal method seems to be non guessing, it is useless for non unique puzzles too, isn't it ?
For a player the goal is neither to analyze the puzzle nor to proof a solution (though both is required), but to find a solution, and in best case an elegant one. For this goal uniqueness methods can be the salt in the soup.
blue wrote:1) There are statements like: "there must be at least one X in Y" (e.g. at least one 3 in box 4)
2) There are statements like: "there can be no more than one X in Y" (e.g. no more than one 3 in box 4)
3) There are statements like: "there must be exactly one X in Y" (e.g. exactly one 3 in box 4)
Statements of the first type, are related to "base sets", or "strongly linked (candidate) sets", or "strong links" (for short).
Statements of the second type, are related to "cover sets", or "pairwise weakly linked (candidate) sets", or "weak links" (for short). In Alan Barker's vocabulary, they are just "links", or "link sets".
Statements of the third type, are related to either "CSP variables" (e.g. Denis Berthier's vocabulary), or "Truths" (Alan Barker's vocabulary).
logel wrote:If I try an interpretation: first and third type are identical.
logel wrote:A see the 324 basic constraints rather as equations of boolean variables called candidates carrying a value true or false.
What I call line is an equation L1 XOR L2 XOR ... XOR L9 = TRUE, where Lx are the candidates from a constraint. Btw XOR is a binary and associative operation.
The XOR expression of each line trivially get shorter with every elimination.
The type2 NAND is not needed at this point, but Lx NAND Ly = TRUE (x<>y) is a consequence from the line equation.
logel wrote:When constructing a sudoku problem its important to check that the problem has a unique solution (!) AND is minimal. Here minimal means that there are no redundant givens.
Why is that important? Redundant givens that you can calculate from the other make the minimal problem simpler to solve. This is obvious because some of the complexity is removed.
Although the uniqueness statement is a bit special, because it cannot expressed by variables, it works like any other redundant clue. It is redundant because it can be calculated form the rest.
So you end up with the statement: I found a simpler solution of a sudoku problem because I made it simpler.
Besides the simplification effect there are more disadvantages. In case that the puzzle is unsolvable anyway, using uniqueness and finding a contradiction makes it impossible to distinguish between "really unsolvable" and "not unique". Not so important, also not desirable.
One of my long term goals is defining a function that gives "elegant" or "simple" a well defined value based on definite principles. Such function would allow to compare solutions by a "quality". Ideas are welcome.
Comparison of solutions sequences using redundant clues (or uniqueness) with normal solution sequences are obviously useless. Not desirable.
denis_berthier wrote:Now, let me state an objection I have to logel's claim of universality.
It is very basic and it is the same objection I had to Allan's similar erroneous claim, years ago.
Most of the known patterns fall into two broad families:
- Subsets (Naked, Hidden or Super-Hidden), g-Subsets
- chains (reversible or oriented)
For both families, the proof that a target can be eliminated is obvious.
I've shown that oriented chains subsume most (but not all) cases of Subsets, in the sense that these Subsets can also be seen as oriented chains with the same targets. I've also shown that chains are much more powerful than Subsets of same size. However, I've never claimed that chains are a universal pattern - which would clearly be false, considering the (rare but real) cases of non-subsumption.
What I want to recall in the context of this thread is that any claim that the first family above is universal is clearly false. A chain cannot be considered as a mere set of CSP-variables (base set) and constraints. In such a view, something would be lost: the order of the chain. As a result, the proof of validity the chain carries with it would also be lost (and the complexity of proving validity increased).
The elementary mathematical basis for this is (symbolically) "sequence = set + order relation on this set".
tarek wrote:The idea of universal solving technique / pattern is an attractive one and is something that I would encourage forum members to work on even if there seems to no light at the end of the tunnel or if there is a déjà vu situation.
Most of the hard work in the Ultimate Fish Guide came from collective ideas/work by forum members. Because it was constructed on solid foundations, it allowed the extension of its concepts to what has been described before by Alan, Dennis and others. There is no harm in exploring ideas or methods that have been discussed before if the result would lead to a Fresh result. I guess that until we get the Fresh result, the process will look far from it.
The oversimplifying sarcastic thread can be found here at the The Ultimate Lizard Guide
blue wrote:For logel,
I think you should heed Denis' advice, and include the "lines" (or whatever you'll call them) in the definition, from the start (along with the "links"). When you use the term "valid permutation of the candidates", it has little meaning without them. Your original definition, and 1st modification -- both in terms of candidates only, had this flaw:
- Code: Select all
1 . . | 1 . . | . . . 1 . . | 1 . . | . . .
/ . . | / . . | . . . / . . | / . . | . . .
/ . . | / . . | . . . / . . | / . . | . . .
------+--------+------ ------+--------+------
1 . . | 1 . 1* | . . . 1 . . | 1 . 1* | . . .
/ . . | / . . | . . . / . . | / . . | . . .
/ . . | / . . | . . . / . . | / . . | . . .
------+--------+------ ------+--------+------
/ . . | / . . | . . . / . . | / . . | . . .
/ . . | / . . | . . . / . . | / . . | . . .
/ . . | / . . | . . . 1 . . | / . . | . . .
The '/'s mark cells where there is no '1' candidate.
The '*' marks a (possible) target candidate.
The diagram on the left, shows a situation where an X-Wing elimination is possible.
The diagram on the right, shows the same thing with an extra '1' candidate in r9c1 -- where there is no X-Wing elimination.
For the 2nd diagram, I didn't see anything in your definition, that would block me from simply ignoring the 1r9c1 candidate, and focusing on the '1' candidates in the diagram on the left.
It's (slightly) possible that the bit about "valid permutations of the candidates", was meant to block that, but if that's the case, it wasn't made clear.
F . . | T . . | . . .
/ . . | / . . | . . .
/ . . | / . . | . . .
------+--------+------
F . . | F . T* | . . .
/ . . | / . . | . . .
/ . . | / . . | . . .
------+--------+------
/ . . | / . . | . . .
/ . . | / . . | . . .
+ . . | / . . | . . .
logel wrote:denis_berthier wrote:Now, let me state an objection I have to logel's claim of universality.
It is very basic and it is the same objection I had to Allan's similar erroneous claim, years ago.
[...]
The elementary mathematical basis for this is (symbolically) "sequence = set + order relation on this set".
You seem to see a contradiction where is absolutely none.
[...]
the conclusion that chains cannot comply to the universal defininition, because they can only be verified by a chain procedure, is incomprehensible.
logel wrote:I rather see an advantage to have a definition covering all. Now its possible to define size for the most general class. This is especially important for pattern derived from level-one contradiction pathes, their size is calculated from the steps.
logel wrote:If you use e.g. braid eliminations on level-one you mostly construct a non-braid elimation for the global level. So the size of such construction is "undefined" using your braid-size.
denis_berthier wrote:...the same old flawed arguments.
eleven wrote:And don't you know, that - when uniqueness methods are allowed - a puzzle also can become harder, when you add a clue, because with this clue you can't apply the technique anymore ?leren wrote:...
eleven wrote:Can't you stop it ?denis_berthier wrote:...the same old flawed arguments.
eleven wrote:Your bombastic rules set cannot even solve a 77 clue puzzle with 2 solutions
eleven wrote:but you refuse to accept uniqueness as part of the definition ?