Backtracking (BT) and Conflict-directed Back Jumping (CBJ)

To demonstrate bt and cbj, we have a number of claire3 programs written

Coded versions of bt

bt.cl. Our first and most primitive implementation of chronological backtracking. It is so primitive it doesn't really work. The purpose of this is to show what a forward move looks like, and a backward move. However, we can use this in the interpreter and show how it goes. NOTE: the problems that can be solved are exclusively 3 colouring problems.
bt0.cl. Our first working version of bt. This uses mutual recursion, and is not really practical, but is okay for demonstrations purposes. It is called as bt(V,D,C)
bt1.cl. We now incorporate performance measures, in particular NODES (instantiations) and CHECKS (actual checks). Again we call bt(V,D,C). We also include a second set of constraints, C2, such that the problem is insoluble, call as bt(V,D,C2) for this demo. We get our end of run statistics by looking at NODES and CHECKS explicitly. We can look at the global variables using the look() function. NOTE: we now have a trace facility, enabled by system.verbose := 3 prior to calling bt(V,D,C).
bt2.cl. We remove mutual recursion, and implement bt iteratively
bt3.cl. We modify the iterative implementation of bt2.cl to allow more general binary constraints. But we are still stuck with uniform 3-colouring domains. Call bt(V,D,C).
bt4.cl. Non-uniform domains and arbirary binary constraints. Must now call bt(V,CD,C) where CD is the current domain. Can now use csp4.cl and csp5.cl

Coded versions of cbj

In cbj.cl we introduce a new global array, CS. CS[i] is the conflict set for variable V[i], i.e. the set of past variables that V[i] failed consistency checks. When reaching a dead end we jump back from V[i] to V[h], where h is the deepest past variable in conflict with V[i]. We also update CS[h] to become the set of variables in conflict with V[i] or V[h]. cbj is derived from bt4.cl as follows

functions label and unlabel deliver an integer result, the index of the next current variable
We have new global variables, boolean CONSISTENT and array of sets CS.
label(v,d,c,i) delivers i+1 if it successfully instantiates v[i], otherwise CONSISTENT is false, and i is delivered as a result (and we jump back from v[i])
unlabel(v,d,c,i) jumps back to v[h], the deepest variable in conflict with v[i], sets CONSISTENT to true if v[h] has values remaining to be tried. Otherwise CONSISTENT is set to false and another round of jumping might occur from v[h]. Regardless, the function delivers h as a result, the new current variable.
cbj replaces bt and has the following structure
- if CONSISTENT is true and i < N we label variable v[i], and get the new current variable, i.e i := label(v,d,c,i)
- if CONSISTENT is false and i > 0 we unlabel variable vi[i] and get the new current variable, i.e. i := unlabel(v,d,c,i)
- if i > N we terminate with a solution
- if i = 0 we terminate with evidence of insolubility

Coded versions of fc

Forward checking fc.cldiffers from cbj and bt in one obvious way: when we instantate the current variable we filter the domains of future variables, weeding out values that are incompatible. Consequently, we never check back, just forwards.

We are now faced with a number of engineering problems. First, we must be able to recover domains on backtracking, i.e. undo the effect of forward checking. We introduce 2 new data structures

RED: if v[i] checks against v[j] and removes a value y from CD[j] then the tuple (i,y) will be in RED[j]. That is RED[j] is the set of reductions on variable j
FCR: if v[i] checks against v[j] and removes any value from CD[j] then j will be in FCR[i]. That is, via forward checking, variable v[i] removes values from the variables with indices in FCR[i], the forward checking reductions of v[i]

FCR and RED allows us to maintain domains during search. Furthermore, we can exploit FCR and RED to incorporate cbj into fc, giving us the hybrid fc-cbj, and algorithm that checks forward and jumps back.

References

For FC see Haralick & Eliott's 1980 paper in AIJ. For BM and BJ, see papers by the late (great) John Gashnig. For cbj and its hybrids see Computational Intelligence 9(3), 1993.