1) Forcing whips and forcing braids
In section "5.9. Forcing whips and braids, a bad idea?" of my book "Pattern-Based Constraint Satisfaction and Logic Puzzles" (PBCS1, 2012, https://denis-berthier.pagesperso-orange.fr/PBCS/index.html, freely available here: https://arxiv.org/abs/1304.1628), I wrote:
PBCS1 wrote:Consider a bivalue variable (in any resolution state), with its two possible values x1 and x2 corresponding to candidates Z1 and Z2 . Suppose there are two partial whips/braids, say W 1 and W2 , one with target Z1 , the other with target Z2 . In case W1 and W2 share a left-linking candidate L [respectively a right-linking candidate R], L can be deleted [resp. R can be asserted]: this is reasoning by cases, which is perfectly valid in intuitionistic logic. Do we get interesting new patterns this way (to be called forcing whips / forcing braids because they force a conclusion that could not be obtained by a single whip/braid pattern)? Obviously, the answer would be negative for reversible chains: it would suffice to reverse one of the chains and to link the two by the bivalue variable in order to obtain a single chain of same type as the two given ones. Notice that in this process the chain thus obtained should be assigned length n1 + n2 +1, where the ni are the lengths of the two chains.
But as whips and braids are not reversible, it seems one could get new patterns, more general than whips and braids. What is the resolution power of such patterns? We have no general answer. But, in the Sudoku case, if these patterns are assigned length n1 + n2 +1 and given smaller priority than whips/braids of same length, we have found no occurrence in a random sample of 1,300 puzzles. As the memory requirements for such combinations are very high, we did not try on larger samples.
There is still the possibility of starting from trivalue variables and considering three whips/braids instead of two, but complexity increases accordingly."
Remember that, in my approach, bivalue means rc-, rn-, cn- or bn- bivalue, i.e. bivalue or bilocal.
2) TDP theory
As far as I understand it, TDP theory consists of taking two candidates as above, separately applying the T&E procedure to each of them, eliminating the candidates that are eliminated by the two procedures and asserting the candidates that are asserted by the two procedures.
3) The T&E vs braids theorem
In section "5.6. The “T&E vs braids” theorem" of PBCS1, I proved the fundamental theorem for braids:
PBCS1 wrote:Theorem 5.7: for any instance of any CSP, any elimination that can be done by T&E can be done by a braid. Any instance of a CSP that can be solved by T&E can be solved by braids.
4) TDP vs forcing braids
It is an immediate consequence of the above that any elimination/assertion done by TDP can be done by forcing braids (and most of the time by forcing whips)
5) Extension
One can consider T&E(T,1) for any resolution theory T with the confluence property - for instance a theory including subsets. In PBCS1, I have proven corresponding generalisations of the T&E vs braids" theorem.
6) Rating
Whereas TDP, like any procedure based on T&E, doesn't come with any notion of rating, this is inherent in the forcing braids approach. The longest forcing whip [resp. braid] necessary to solve a puzzle defines its FW [resp. FB] rating.
7) Open question
The open question I mentioned in the first point above (Are there puzzles that can be solved by forcing braids but not braids?) remains open. In terms of TDP, it becomes: are there puzzles that can be solved by TDP (based only on singles and elementary contradiction propagation) but not by braids - or: are there puzzles that can be solved by TDP but not by (repeated) T&E? A good place to look for would be in the SER 9.4 to 9.5 zone (puzzles with SER ≤ 9.3 are generally solvable by braids).
I tried a few of the puzzles proposed by Robert in the "puzzles" section, but they are very easy (solvable in W5 or W6) and don't allow any conclusion.
