.
TRIDAGON-FORCING-WHIPS
1) OR-forcing-chains in general
Whenever an OR relation OR(C1, C2) between two candidates C1 and C2 has been proven, assertions and eliminations can easily be obtained by resorting to reasoning by cases. This is not very elegant as it relies on two different streams of reasoning, but it can be useful.
More precisely, consider two different chains, one based on C1 and one based on C2. It can be concluded that:
- any candidate X that is linked to some candidate with positive valence in each chain can be eliminated,
- and any candidate that has positive valence in both chains can be asserted as a decided value.
As a special case of X having negative valence, one or two of the chains can have length 0 (which means that the corresponding Ci is linked to X).
Now, a point on the complexity assigned to such OR-forcing-chains in my approach: the OR(C1, C2) relation isn't supposed to have been proven with the use of a crystal ball. It has involved some particular pattern with its own length (e.g. a biwhip[k]). Similarly, each of the partial-chains has its own length, resp. p1 and p2.
The length of the OR-forcing-chain is thus naturally assigned value n= k + p1 + p2. Indeed, I have no choice: no other possible value would be consistent with my other ratings.
One might object that if the same OR relation is used several times in the resolution path, this is "unfair". But this would rely on a misunderstanding of the fundamental nature of all my ratings: they are ratings of the hardest elimination/assertion step and how many times this highest rating is reached in the resolution path is totally irrelevant.
One might prefer a rating of a full resolution path and I understand this, but as of now, any such proposed rating is totally inconsistent.
In my approach, the typical OR-forcing-chain[n] is a forcing-whip[n], the OR relation being a mere bivalue relation (length 1) and the length of this forcing-whip has already been defined long ago as n = 1 + p1 + p2.
2) Tridagon-Forcing-Whips
Definition:
A Tridagon-Forcing-Whip[n] is a particular type of OR forcing-chain where:
- the partial-chains involved are partial-whips, of respective lengths p1 and p2
- the OR relation involved is a Tridagon-link[12]
- n = 12 + p1 + p2
Remarks:
In order to avoid considering special cases when p1 and/or p2 is 0, the direct link can be considered as a whip[0].
Having a well-defined length, these forcing chains have a natural place in the CSP-Rules hierarchy. However, as for any other rules, various strategies allow to change this default hierarchy. More on this later.
Examples: see my previous posts.
Notation: see my previous posts. The "-" symbol at the end of the lines for the partial-whips means as usual a direct contradiction link.
Implementation:
- the mere Tridagon elimination rule (first post of this thread) is fully implemented in SudoRules and has already been published on GitHub;
- the Tridagon-links are fully implemented in SudoRules, based on my previous analysis of all the possible cases;
- the Tridagon-Forcing-Whip[n] rules are fully implemented in SudoRules. I've applied them to the above-mentioned complete list of 246 puzzles. `
All this will be published soon on GitHub, after I've done more testing.