The New Sudoku Players' Forum

[denis_berthier]

Thanks for your advice. Strictly speaking, I am not a programmer, my profession is not a programmer, and I have never profited from writing programs. I am just a programming amateur. I started programming with vba provided by microsoft excel. I now use Freebasic programming language.

OK, but it seems you're quite good in these languages. Tell me if you have any problem reading a partial-whip file.

[yzfwsf]

a) If, in RS3, the left-linking or any t- or z- candidate of CSP-Variable Vp has been asserted, then Z and/or the previous Rk(’s) to which Lp is linked must have been eliminated by ECP in the passage from RS2 to RS3 (if it was not yet eliminated in RS2); if Z is among these eliminations, there remains nothing to prove; otherwise, the procedure has already been successfully terminated by case f of the first such k.
b) If, in RS3, left-linking candidate Lp has been eliminated (but not asserted) (it can therefore no longer be used as a left-linking candidate in a braid) and if CSPVariable Vp still has a z- or a t- candidate Cp, then replace Lp by Cp; now, up to Cp, B’ is a partial braid in RS3 with target Z. Notice that, even if Lp was linked to Rp-1 (as it would if B was a whip), this may not be the case for Cp; therefore trying to prove a similar theorem for whips would fail here (see section 5.10.3 for an example of non-confluence of the Wn theories). [As it missed this point, the proof given for zt-chains in HLS1 was not correct.]
c) If, in RS3, any t- or z- candidate of Vp has been eliminated (but not asserted), this has not changed the basic structure of B (at stage p). Continue with the same B’.
d) If, in RS3, right-linking candidate Rp has been asserted (p can therefore not be the last index of B’), it can no longer be used as an element of a braid, because it is no longer a candidate. Notice that all the left-linking and t- candidates for CSPVariables of B after p that were incompatible in B with Rp, i.e. linked to it, if still present in RS2, must have been eliminated by ECP somewhere between RS2 and RS3. But, considering the braid structure of B upwards from p, more eliminations and assertions must have been done by rules from BRT between RS2 and RS3. Let q be the smallest number strictly greater than p such that, in RS3, CSPVariable Vq still has a (left-linking, t- or z-) candidate Cq that is not linked to any of the Ri for p ≤ i < q (by definition of a braid, Cq is therefore linked to Z or to some Ri with i < p). Between RS2 and RS3, the following rules from BRT must have been applied for each of the CSP-Variables Vu of B with index u increasing from p+1 to q-1 included: eliminate its left-linking candidate (Lu) by ECP, assert its right-linking candidate (Ru) by S, eliminate by ECP all the left-linking and t-candidates for CSPVariables after u that were incompatible in B with the newly asserted candidate (Ru). In RS3, excise from B’ the part related to CSP-Variables p to q-1 (included) and (if Lq has been eliminated in the passage from RS1 to RS3) replace Lq by Cq; for each integer s ≥ p, decrease by q-p the index of CSP-Variable Vs and of its candidates in B’; in RS3, B’ is now, up to p (the ex q), a partial braid in Bn with target Z.
e) If, in RS3, left-linking candidate Lp has been eliminated (but not asserted) and if CSP-Variable Vp has no t- or z- candidate in RS3 (complementary to case b), then Vp has only one possible value in RS3, namely Rp; Rp must therefore have been asserted by S somewhere between RS1 and RS3; this case has therefore been dealt with by case d (because the assertion of Rp also entails the elimination of Lp).
f) If, in RS3, right-linking candidate Rp of B has been eliminated (but not asserted), in which case p cannot be the last index of B’, then replace B’ by its initial part: {L1 R1} – {L2 R2} – …. – {Lp .}. At this stage, B’ is in RS3 a shorter braid with target Z. Return B’ and stop.
Notice that the above proof works only because the notion of being linked does not depend on the resolution state.
Notice also that what we have proven is indeed the following: given RS1, B and RS2 as above, if RS3 is the resolution state obtained from RS2 by the repeated application of rules from BRT until quiescence, then: – either a contradiction has been detected by CD somewhere between RS2 and RS3 (and, due to consistency preservation between RS1 and RS2, it can only be because a contradiction inherent in the givens of P has been made manifest by CD); – or Z has been eliminated by ECP somewhere between RS2 and RS3; – or Z can be eliminated in RS3 by a braid B’ possibly shorter than B, with target Z, with CSP-Variables a sub-sequence W’ of those of B, with right-linking candidates those of B belonging to the sub-sequence W’, with left-linking candidates those of B belonging to the sub-sequence W’, each of them possibly replaced by a z- or t- candidate of B for the same CSP-Variable.

Does this mean that the B found in RS1 is the shortest? Also, is the search process of B all terminated by case f?

[denis_berthier]

Hi yzfwsf
I don't know why you put that part in red. It's the most trivial case.

Does this mean that the B found in RS1 is the shortest?

No. Not even the original braid is supposed to be the shortest one that allowed to eliminate Z.
Obviously, the construction produces a braid that can't be longer than the original one. But, it gives no other guarantee about its length. And that is not the purpose of the proof anyway.

Also, is the search process of B all terminated by case f?

Yes.

[yzfwsf]

There are three kinds of contradictions in Vp:
1) No Rp compatible with Z
2) Lp (z or t candidates) has been assert
3) Rp has been eliminated
Can RS1 be determined by either of the above?

[denis_berthier]

.
You should have also cited the start of the proof:

We must show that, if an elimination of a candidate Z could have been done in a resolution state RS1 by a braid B of length m ≤ n and with target Z, it will always still be possible, starting from any further state RS2 obtained from RS1 by consistency preserving assertions and eliminations, if we use a sequence of rules from Bn.
Let B be: {L1 R1} – {L2 R2} – …. – {Lp Rp} – {Lp+1 Rp+1} – … – { m .}, with target Z.
Consider first the state RS3 obtained from RS2 by applying repeatedly the rules in BRT until quiescence. As BRT has the confluence property (theorem 4.1), this state is uniquely defined, independently of the way we apply the BRT rules.

The confluence property is very strong. What's proven here (invariance for confluence) is still stronger.
RS1 is some resolution state, where B is supposed to exist. RS1 doesn't have to be determined by anything.
RS2 is some state after RS1, reached after some arbitrary (but consistency preserving) assertions and deletions have happened. RS2 also is totally arbitrary (apart from being "after" RS1).
RS3 is the closure of RS2 under BRT.

What the proof does is review all that can have happened to B between RS1 and RS3 and show that Z can still be eliminated in RS3 by some shorter braid (built from B).

[yzfwsf]

Hi:denis
I was originally poor in English, and your book is academic, so I can't understand it even more. Can you annotate every sentence of this code in natural language? Thanks.

Code: Select all

(defrule braid[10]
   (declare (salience ?*braid[10]-salience*))
   (chain
      (type partial-braid)
      (context ?cont)
      (length 9)
      (target ?zzz)
      (llcs $?llcs)
      (rlcs $?rlcs)
      (csp-vars $?csp-vars)
      (last-rlc ?last-rlc)
   )
   (candidate (context ?cont) (status cand) (label ?new-llc&~?zzz&:(not (member$ ?new-llc $?rlcs))&:(linked-or ?new-llc ?zzz $?rlcs)))   
   (is-csp-variable-for-label (csp-var ?new-csp&:(not (member$ ?new-csp $?csp-vars))) (label ?new-llc))
     (forall (csp-linked ?cont ?new-llc ?xxx ?new-csp)
      (exists (exists-link ?cont ?xxx ?vvv&:(or (eq ?vvv ?zzz) (member$ ?vvv $?rlcs))))
   )
   
   ?cand <- (candidate (context ?cont) (status cand) (label ?zzz))
=>
   (retract ?cand)
   (if (eq ?cont 0) then (bind ?*nb-candidates* (- ?*nb-candidates* 1)))
   (if (or ?*print-actions* ?*print-L10* ?*print-braid* ?*print-braid-10*) then
      (print-braid 10 ?zzz $?llcs $?rlcs $?csp-vars ?new-llc . ?new-csp)
   )
)

[denis_berthier]

Hi:denis
I was originally poor in English, and your book is academic, so I can't understand it even more. Can you annotate every sentence of this code in natural language? Thanks.

OK. Comments preceded by ";;;"

Code: Select all

;;; This defines rule braid[10]:
(defrule braid[10]
   ;;; this defines the priority of rule braid[10]:
   (declare (salience ?*braid[10]-salience*))

   ;;; 1st condition: there is a chain of type partial-braid, of length 9, with target ?zzz,
   ;;; with its sequences of llcs, rlcs and csps defined by variables $?llcs, $?rlcs, $?csps
   ;;; and with its last rlc defined by variable ?last-rlc (this is redundant but useful)
   (chain
      (type partial-braid)
      (context ?cont)
      (length 9)
      (target ?zzz)
      (llcs $?llcs)
      (rlcs $?rlcs)
      (csp-vars $?csp-vars)
      (last-rlc ?last-rlc)
   )
   
   ;;; Starting from this partial-braid[9], the other conditions extend it to a braid[10].

   ;;; 2nd condition: there is a candidate ?new-llc
   ;;; which is not equal to ?zzz and which is not a member of $?rlcs (i.e. not equal to any previous right-linkng candidate),
   ;;; but which is linked to ?zzz or to one of the candidates in  $?rlcs (i.e. to some previous right-linkng candidate)
   (candidate (context ?cont) (status cand) (label ?new-llc&~?zzz&:(not (member$ ?new-llc $?rlcs))&:(linked-or ?new-llc ?zzz $?rlcs)))   

   ;;; 3rd condition: there is a csp-variable ?new-csp which is different from all the previous ones and which is a csp-variable for this candidate ?new-llc
   (is-csp-variable-for-label (csp-var ?new-csp&:(not (member$ ?new-csp $?csp-vars))) (label ?new-llc))

   ;;; 4th condition: moreover, this csp-variable is such that for any candidate ?xxx for it other than ?new-llc
   (forall (csp-linked ?cont ?new-llc ?xxx ?new-csp)
         ;;; there exists a link between ?xxx and ?zzz or some of the previous right-linking candidates
         (exists (exists-link ?cont ?xxx ?vvv&:(or (eq ?vvv ?zzz) (member$ ?vvv $?rlcs))))
   )

   ;;; identify the target for elimination (that's not really a condition, just a CLIPS technical condition for allowing the forthcoming elimination)
   ?cand <- (candidate (context ?cont) (status cand) (label ?zzz))
=>
   ;;; if all the above conditions are satisfied, then eliminate the target:
   (retract ?cand)
   ::: update the number of candidates:
   (if (eq ?cont 0) then (bind ?*nb-candidates* (- ?*nb-candidates* 1)))
   ;;; print the braid elimination:
   (if (or ?*print-actions* ?*print-L10* ?*print-braid* ?*print-braid-10*) then
      (print-braid 10 ?zzz $?llcs $?rlcs $?csp-vars ?new-llc . ?new-csp)
   )
)