denis_berthier wrote:
SOLVABLE BY NRCZT-BRAIDS <=> SOLVABLE BY T&E(ECP+NS+HS)This post gives a precise answer to the question: what is the solving potential of nrczt-braids?
Given any resolution theory, such a question is generally very hard to answer. E.g., if I considered only whips instead of braids, I'd have no answer.
First, I need non ambiguous definitions. And for this, you must remember my distinction between a resolution rule and a resolution technique (see here:
http://forum.enjoysudoku.com/viewtopic.php?t=5600&start=0).
Definition: Given a resolution theory T and a candidate z, T&E(T, z) is the following resolution technique:
- start a new grid by copying the current PM; add z to this new grid as a decided value; apply to this new PM all the rules in T;
- if a contradiction is obtained in this new PM, then delete z from the original one; if no contradiction is obtained, then merely go back to the original PM.
I think this is what everyone means by "using T&E(T) to eliminate candidate z".
Definition: Given a resolution theory T, T&E(T) is the following resolution technique (this is only conceptual, any implementation would optimise this):
- a) define phase = 1;
- b) apply all the rules in T;
- c) set changed-PM = false; mark all the remaining candidates as "not tried";
- d) if there is at least one "not-tried" candidate, then choose any one of them, say z; apply T&E(z); if it eliminates z, then set changed-PM = true and apply all the rules in T, otherwise un-mark z; in both cases, goto d;
- e) if there is no not-tried candidate:
----------- if changed-PM = true, then set phase = phase +1 and goto c);
----------- if changed-PM = false, then stop.
Notice that the procedure allows considering the same candidate z several times. This is reasonable, because any elimination on another candidate z' by T&E(z') may entail a new possibility of a contradiction appearing in a new application of T&E(z).
Definition: a puzzle P is solvable by T&E(T) if the above procedure leads to a solution.
We'll be interested only in T= ECP+NS+HS (with ECP = the rules for the elementary constraints propagation).
Notation: T&E designates T&E(ECP+NS+HS)
THEOREM: ANY ELIMINATION THAT CAN BE DONE BY AN NRCZT-BRAID WITH TARGET Z CAN BE DONE BY T&E(ECP+NS+HS, z)
COROLLARY: ANY PUZZLE THAT CAN BE SOLVED WITH ONLY NRCZT-BRAIDS (+ of course ECP, NS and HS) CAN BE SOLVED BY T&E(ECP+NS+HS).Proof: obvious.
What is interesting is that the converse is true:
THEOREM: ANY ELIMINATION THAT CAN BE DONE BY T&E(ECP+NS+HS, z) CAN BE DONE BY AN NRCZT-BRAID WITH TARGET z.
COROLLARY: ANY PUZZLE THAT CAN BE SOLVED BY T&E(ECP+NS+HS) CAN BE SOLVED BY NRCZT-BRAIDS.Notice that puzzles that can't be solved by T&E(ECP+NS+HS) are extremely rare.
We shall show that any elimination done by T&E, at any step in the resolution process, could have been done by an nrczt-braid.
Consider the PM generated by the T&E hypothesis z=n0r0c0 and take n0r0c0 as the target of the nrczt-braid we're going to build.
In the auxiliary PM generated by the T&E hypothesis, the T&E procedure is a well defined sequence of deletions of candidates based on ECP and of assertions of values based on NS or HS, until a contradiction is reached (if one is reached).
1) Consider the first step of T&E that is not an elimination by ECP.
Suppose first that the assertion made by this step relies on NS: say r'c'=n'
If this assertion can be made, it can only be because:
- n'r'c' is not nrc-linked to n0r0c0 (otherwise it would have been eliminated by ECP);
- all the other candidates for cell r'c' have been eliminated by the assertion of n0r0c0, which supposes that they are nrc-linked to n0r0c0, because only ECP can produce eliminations.
Take any of the candidates in cell r'c', different from n'r'c', say n1r'c'.
Then {n1r'c' n'r'c'} is the first cell of our nrczt-braid (and all the other candidates in cell r'c' are z-candidates).
The same reasoning applies if this step is an assertion by HS(row): instead of considering the rc-cell r'c', we consider the rn-cell r'n'.
The same reasoning applies if this step is an assertion by HS(col): instead of considering the rc-cell r'c', we consider the cn-cell c'n'.
The same reasoning applies if this step is an assertion by HS(blk): instead of considering the rc-cell r'c', we consider the bn-cell b'n'.
2) The sequel is done by recursion. If we have been able to replace the T&E procedure upto the nth assertion step, then we can replace it by a longer nrczt-braid upto the (n+1)th assertion step. Name n'r'c' the nth candidate asserted.
Suppose first that the (n+1)th assertion made by T&E relies on NS: say r'c'=n'
If this assertion can be made, it can only be because:
- n'r'c' is not nrc-linked to n0r0c0 or to any of the previous candidates asserted in any of the previous steps, i.e. to any of the right-linking candidates of the partial nrczt-braid we've already built (otherwise it would have been eliminated by ECP);
- all the other candidates for cell r'c' have been eliminated by the assertions of n0r0c0 and of all the previously asserted candidates, which supposes that each of them is individually nrc-linked to the target or to some of the previous right-linking candidates;
- there is a candidate n1r'c' in cell r'c' which is nrc-linked to n0r0c0 OR to a previous right-linking candidate n2r2c2. Take {n1r'c' n'r'c'} as the next cell of our braid. NOTICE THAT IT WOULD BLOCK HERE IF WE CONSIDERED WHIPS INSTEAD OF BRAIDS.
The new cell of our nrczt-braid, {n1r'c' n'r'c'}, is appended to the right of n2r2c2 (all the other candidates in cell r'c' are z- or t- candidates wrt to already existing branches of the net).
The same reasoning applies if this step is an assertion by HS(row): instead of considering the rc-cell r'c', we consider the rn-cell r'n'.
The same reasoning applies if this step is an assertion by HS(col): instead of considering the rc-cell r'c', we consider the cn-cell c'n'.
The same reasoning applies if this step is an assertion by HS(blk): instead of considering the rc-cell r'c', we consider the bn-cell b'n'.
3) End: a contradiction is detected by T&E when a cell (rc-, rn-, cn- or bn-) has no candidate left. Suppose it is an rc-cell.
How can that happen? Only via an ECP step. But it means then that the last asserted value is nrc-linked to a previous right-linking candidate or to the target, i.e. we have an nrczt-braid.
q.e.d.
Remark: for the first time,
we thus have a set of resolution rules (the set of nrczt-braid[n] rules, for any length n, together with ECP, NS and HS) which is equivalent to T&E. 
