Hi Denis,
I just noticed your latest comments. Thanks for them. I'm replying here to your earlier ones first.
denis_berthier wrote:What do you call advanced whips? There are g-whips already, but they don't shorten the resolution paths. If you mean S-whips (i.e. with Subsets allowed as rlcs), their additional resolution power is not worth the effort to code them, considering their increased computational complexity - and they are not necessary for puzzles in T&E(1), i.e. all but 1/30,000,000 puzzles.
Ok. I didn't realize that S-whips weren't implemented in SudoRules. In that case I would just ask for a couple of notational examples of those (preferably with all naked, hidden, and super-hidden subsets as rlcs). Even if SudoRules doesn't use them and you don't think they're important, many human solvers use them. I'd like to know how such logic maps to your notation. For example, how would you write my pseudo-braid above as a real one? It has both naked and hidden subsets as rlcs, though obviously not super-hidden ones (since Robert doesn't use even live fishes, much less almost-ones). And yes, it also has a set of UR guardians as a CSP-variable as you noticed. I have no idea how you'd notate that.
Variety in SudoRules can better be seen in Subset rules, Oddagons, special cases of whips (bivalue-chains, z-chains, t-whips, typed versions of all the chains, ...)
Yes, I can find examples of all of those.
forcing-whips (that I never use because they are inefficient and inelegant)
Why do you think they're inelegant? Those of us who like verity patterns would probably disagree. If I've understood forcing whips/braids correctly, they're much closer to methods that many advanced human solvers like to use. It's a common method in TDP (conjugate tracks), and it's also somewhat similar to what I do with coloring. With that style one doesn't have to assume anything. Mostly you look for agreements (verities) between the two parities, but it can also reveal a contradiction for one of them, so it can be fruitful in two ways. If you look for contradictions only, then you can find contradictions only -- and if you happen to try a true candidate, you'll never get one, which may take a while to realize.
Also, when you look for agreements for the two branches, you don't have to stop when you find the first result. You can keep going and find many more without losing any of the previous work. I think that's what Robert has been saying recently. Of course if you do that long enough, you'll eventually run into a contradiction for one of the parities (assuming no OR-branching is needed), and that solves the whole pattern, including the previously found agreements. The biggest benefit of the two-pronged approach is that the contradiction can happen for either parity, and even if you don't find one, you may still get useful results.
exotic (and very rare) patterns (sk-loops, J-Exocets), uniqueness rules (for those who like that),
Good to know SudoRules has those too, although I'm the most interested in the patterns that are unique to it. For example:
W*-whips for some extreme puzzles...
I guess those involve some kind of nesting. That would make them interesting, though possibly incomprehensible for me at this time. At some point I'd like to see an example. I think you used them for some hard puzzle recently, but chose not to display the full notation.
AND anyone can extend it to code his own rules; you should give that a try.
Not likely in the near future, but I'll keep that in mind. I've been avoiding any sort of sudoku coding so far, except for a basic solver I once did. But, I think I will at least try and run SudoRules in the not so distant future. I expect it to work well on a Mac, since you use that too.
SpAce wrote:For me a second miracle is that they have very different computational complexities, and to the whip's advantage. Why exactly is that?
No second miracle here, but something perfectly clear to me.
Before you get a whip/braid, you have to build partial-whips/braids, which have a pending rlc. Complexity arises at the time you extend them from length n to n+1.
And what counts here is the
branching factor from the last rlc (i.e. the mean number of possible next llcs):
- in whips, it is constant (in the mean), i.e. independent of the partial-whip length
- in braids, it increases linearly (still in the mean) with the length of the partial braid.
As a result, the mean relative complexity of partial-braids wrt partial-whips (or, in simpler terms, their relative numbers) is exponential with length.
Ok. I think I can understand that, at least from a software point of view. Not sure how well it applies to human solving, but I guess it could. I have to do more testing. The couple of times I recently did, it did indeed seem simpler (but slower) to stick to a continuous path, and the contradictions were easier to spot with less coloring clutter. However, they were targets for which I knew a whip existed, and I got lucky with my routing choices.
I'm still wondering what you do when your partial whip runs into a dead-end. Do you backtrack to a previous choosing point (and erase all the chain elements from the dead-end part) and try a different route? With my coloring system that would be kind of tedious. It's easier to just leave it all there and continue from a different place, but that quickly loses any notion of continuity.
SpAce wrote:For me it would seem logical that you'd get many more dead-ends if you only looked for whips, because it's the more specific type.
It sounds sensible and it may play
some role, but the fact is, it doesn't turn out to be as important as the branching factor.
Ok. I have to trust you on that.
I had (and still have) no convincing way of explaining in advance why it turns out to be that way. That's why I sometimes call it a (laïc) "miracle". It's also related (but not in a systematic way) to the fact that non-confluence is very rare for whips. Without such a gain, I would probably have given up developing SudoRules long ago.
And all this is true not only of Sudoku, but of all the other logic puzzles I've tried - in spite of their very different types of constraints. Which leads me to think there may be some general explanation, it keeps lurking in my mind, but it still eludes me.
Well, this is interesting indeed.