.
Someone told by PM that I should recall the definition of T&E(n).
The classical pseudo-definition of T&E was "suppose candidate Z is true; if this leads to a contradiction, delete Z".
This is totally meaningless if you don't say HOW it may lead to a contradiction: in particular, any candidate that is not in the solution does lead to a contradiction in First Order Logic [FOL] - not a very useful definition.
I'll recall my formal definition, first introduced here
http://forum.enjoysudoku.com/fully-supersymmetric-chains-t5591-151.html and here
http://forum.enjoysudoku.com/abominable-trial-and-error-and-lovely-braids-t6390.html. These were the first formalisations of what was intended in the previously vague definition.
I'll take the form present in [PBCS], including all the details necessary for writing a non-ambiguous program.
©PBCS, section 5.6 wrote:Definition: given a resolution theory T with the confluence property, a resolution state RS and a candidate Z in RS, T&E(T, Z, RS) or Trial-and-Error based on T for Z in RS, is the following procedure (notice: a procedure, not a resolution rule):
- make a copy RS’ of RS; in RS’, delete Z as a candidate and assert it as a value;
- in RS’, apply repeatedly all the rules in T until quiescence;
- if RS’ has become a contradictory state, then delete Z from RS (sic: RS, not RS’); else do nothing (in particular if a solution is obtained in RS’, merely forget it);
- (discard RS’ and) return the (possibly) modified RS state.
Notice that this definition is meaningful only if T has the confluence property: otherwise, the result of “applying repeatedly in RS’ all the rules in T until quiescence” may not be uniquely defined.
Definition: given a resolution theory T with the confluence property and a resolution state RS, we define the T&E(T, RS) procedure as follows:
a) in RS, apply the rules in T until quiescence; if the resulting RS is a solution or a contradictory state, then return it and stop;
b) mark all the candidates remaining in RS as “not-tried”;
c) choose some “not-tried” candidate Z, un-mark it and apply T&E(T, Z, RS);
d) if Z has been eliminated from RS by step c, then goto a else if there remains at least one “not-tried” candidate in RS then goto c else return RS and stop.
Definition: given a resolution theory T with the confluence property and an instance P with initial resolution state RSP , we define T&E(T, P) as T&E(T, RSP ).
Notice that this procedure always stays at depth 1 (i.e. only one candidate is tested at a time) but that a candidate Z may be tried several times for T&E(T, Z, RSi ) in different resolution states RSi. This is normal, because the result may be different if other candidates have been eliminated in the meanwhile. This also guarantees that the result of this procedure does not depend on the order in which remaining candidates are “tried”.
We say that P can be solved by T&E(T), or that P is in T&E(T), if T&E(T, P) produces a solution for P.
When T is the Basic Resolution Theory (BRT) of a CSP (which is known to always have the confluence property), we simply write T&E instead of T&E(BRT(CSP))).
©PBCS, section 11.3.2 wrote:Definition: given a resolution theory T with the confluence property, a resolution state RS and an integer n, the two procedures Trial-and-Error based on T at depth n for Z in RS and Trial-and-Error based on T at depth n in RS [respectively T&E(T, Z, RS, n) and T&E(T, RS, n)] are defined by mutual recursion as follows:
T&E(T, Z, RS, 1) = T&E(T, Z, RS) and T&E(T, RS, 1) = T&E(T, RS), where the right-hand sides have been defined in section 5.6.1.
For n>1, T&E(T, Z, RS, n) is defined as follows:
- make a copy RS1 of RS; in RS1 , delete Z as a candidate and assert it as a value;
- apply T&E(T, RS1, n-1);
- if RS1 has become a contradictory state (detected by CD), then delete Z from RS (sic: RS, not RS1 ); otherwise, do nothing (in particular if a solution is obtained in RS1, merely forget it);
- return the (possibly) modified RS state.
For n>1, T&E(T, RS, n) is defined as follows:
a) in RS, apply the rules in T until quiescence; if the resulting RS is a solution or a contradictory state, then return it and stop;
b) mark all the candidates remaining in RS as “not-tried”;
c) choose some “not-tried” candidate Z, un-mark it and apply T&E(T, Z, RS, n);
d) if Z has been eliminated from RS by this procedure,
then goto a
else if there remains at least one “not-tried” candidate in RS then goto c else return RS and stop.
Notice that every time a candidate is eliminated by step d of T&E(T, RS, n), all the other candidates (remaining after step a) are re-marked as “not-tried” by step b. Thus, the same candidate can be tried several times in different resolution states. Even with T having the confluence property, this is necessary to guarantee that the result does not depend on the order used to try the candidates (in step c).
Definition: given a resolution theory T with the confluence property and an instance P with initial resolution state RSP , we define T&E(T, P, n) as T&E(T, RSP , n).
Definition: for an instance P, the T&E-depth of P, d(P), is the smallest n≥0 such that P can be solved by T&E(n), with the convention that T&E(0) = BRT(CSP).
[Edit]: T&E(T, n) is coded in CSP-Rules for n≤3. T can be selected in the config file