Hi
Denis,
I think you raise a good question, but it must be taken the other way round: start from the problem and, only after that, see what kinds of logical relations it involves.
Interesting. I didn't think I was raising a queston. But "good".
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).
First, a clarification: what I meant by an "at most one of" statement, was something like the conjunction of the NAND staetments associated with one of the "constraints" that you list in (2).
Next, it's nice that you included the 81/324 breakdown above, since it a good illustration of something that can leave me confused. The first thing that popped into my head, was "wait, isn't it really 81 of first type, and only 243 of the 2nd type ?" -- thinking that with (1), the 'rc' constraints from (2) are unnecessary. The answer would depend on whether, in (1), you're considering the possiblity that two or more digits could be placed in the same cell. In the 2nd bit that I quoted, where you say that the type 1 items are "exactly one of" formulae, I think that confirms my "isn't it only 243 ?" suspicion.
Finally, I would in no case use the word requirement here. Requirements appear at another level:
(...)
This surprised me.
I didn't intend a grand meaning in the term "requirement" -- just a preference to distinguish between the "must do", and "may not do" types of (low level) constraints.
For a more general audience ...
In any case, the reason I brought some of that up, has a bit to do with Alan Barker's XSudo program, and how what it does, is relates to "base/cover" concepts. It almost seems that his Truth sets equate to "bases" (sets of "base sectors"), and his link sets, to "covers" (sets of "cover sectors"). That isn't quite true though. In base/cover terms, the way his code is working, in that view, each "base sector" is also being treated as a "cover sector".
That's taking these "definitions" (if you like), into account
- a "base set" is a set of propositions/candidates where "at least one, must be true".
- a "cover set" is a set of propositions/candidates where "no more than one, may be true".
- "sector", rather than "set" is used ("base sector" or "base set"), when the set of candidates is the set of "live candidates" from one of the 324 "units"/"2D-cells".
- a "base", is a set of base sets (or base sectors), and a "cover" is a set of cover sets.
[ While it's true that the candidates in a base
sector, satisfy an "exactly one is true" condition in an actual sudoku solution grid, that fact is never used in base/cover arguments. If it happened to be necessary to support an elimination claim (and I'm not saying that it ever is), then the sector would also be added as a cover sector as well. ]
I'm trying to put a plug in for clarity here. It seems that
logel's definitions, after refinement, are going to revolve around either a "base/cover" setup, or a "truth/link" setup. I don't know what he'll have in mind for the "weak link" aspect of things -- that one should list individual "binary weak links", or that hings like "cover sectors"/"links", could be listed instead. It almost wouldn't mattern, but he's including a "minimality" condition, and maybe sometimes not every binary weak link associated with a cover sector, would be necessary to produce the target candidate elimination.
For
logel,
I think you should heed Denis' advice, and include the "lines" (or whatever you'll call them) in the defintion, 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.
I would make one more plea. When you say "valid permutations of the candidates", I do understand what you mean, up to some point. It reminds me of the "Show candidate permutations" menu item in Alan Barker's XSudo. The silly side of me, though, looks at the diagrams above, and says: "what ... how am I going to get anything but a bunch of 1's in the same places they started at, if I 'permute the candidates' ?". I would appreciate it if you were more explicit about what you say in that regard. On the serious side, assuming that you include the "lines" idea in the definition, I'ld like to see an indication of whether a "valid permutation", could include a case where two candidates from the same "line" are true ("base sector" logic), or whether there's an implied assumption that only one may be true (Alan Barker's "truths" logic). I do realise, however, that the difference lies in what "links" are explicitly present, and that up to now, the number and nature of the links, hasn't been expecially relevant.
More about complexity of verifications, in another post ...
Regards,
Blue.