About the T&E TheoremsQuestion from a French friend (my translation) wrote:Isn't there a contradiction between the two theorems you proved in relation with T&E:
Taken from the "concept of a resolution rule" thread, second post
http://forum.enjoysudoku.com/viewtopic.php?t=5600:
denis_berthier wrote:Definition: T&E is the following procedure: recursively make ad hoc hypotheses on something that you do not know to be true at the time you make them, explore their consequences, with the possibility of retracting each of these hypotheses and their consequences if they lead to a dead end.
Theorem: Trial and Error is a resolution technique that cannot be the implementation of any resolution rule.
Taken from the "abominable T&E and lovely braids" thread, second post
http://forum.enjoysudoku.com/viewtopic.php?t=6390:
denis_berthier wrote:T&E theorem: ANY ELIMINATION DONE BY T&E CAN BE DONE BY AN NRCZT-BRAID.
...
Corollary: ANY PUZZLE SOLVABLE BY T&E IS SOLVABLE BY NRCZT-BRAIDS.
Thanks for asking. I wans't aware that this wasn't obvious. The two procedures are different.
There may seem to be a contradiction, due to the very bad name I chose in the first case for the procedure I was defining.
But, the two theorems are true and non contradictory. We must just be careful about names.
The two definitions and associated theorems are recalled here (only the name of the first procedure is changed, the definitions and proofs given in the two aforementioned threads remain unchanged):
1) "Concept of a resolution rule" thread:
What I've called T&E and then rT&E in the first thread, and which should be called something like RTEG "recursive T&E with guessing" is any structured search procedure (DFS or BFS) with no a priori depth limit, and accepting positive results (if it finds a solution, it accepts it - which is a form of guessing).
RTEG theorem: RTEG is a resolution technique that cannot be the implementation of any resolution rule.RTEG theorem (strong form): RTEG is a resolution technique that cannot be the implementation of any set of resolution rules.This can be extended to any RTEG(T), for any resolution theory T, where RTEG(T) means the search is pruned by the rules in T.
2) "Abominable T&E and lovely braids" thread:
Definition: Given a resolution theory T (i.e. a set of resolution rules) and a candidate z, T&E(T, z) is the following resolution technique:
- start an auxiliary grid by copying the current PM; in this auxiliary grid, delete z as a candidate and add it as a decided value; apply to this auxiliary PM all the rules in T until quiescence;
- if a contradiction is thus obtained in this auxiliary PM, then eliminate 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 should 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 of them, say z; apply T&E(T, 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.
Said otherwise, repeat T&E(T, z) for all the candidates z, as long as any one remains, until quiescence.
T&E theorem: Any elimination done by T&E can be done by an nrczt-braid.T&E theorem: Any elimination done by T&E(T) can be done by an nrczt-braid(T).3) Differences between the two procedures:
In the second case:
- there's no recursion (although we can also define a depth 2 T&E, but it won't be unlimited recursion).
- no "guessing" is allowed: if a solution is found in the auxiliary PM, it is merely forgotten.