A THEORETICAL EVALUATION OF SELECTED BACKTRACKING ALGORITHMS

In recent years, many new backtracking algorithms for solving constrai nt satisfaction problems have been proposed. The algorithms are usuall y evaluated by empirical testing. This method, however, has its limita tions. Our paper adopts a different, purely theoretical approach, whic h is based on characterizations of the sets of search tree nodes visit ed by the backtracking algorithms. A notion of inconsistency between i nstantiations and variables is introduced, and is shown to be a useful tool for characterizing such well-known concepts as backtrack, backju mp, and domain annihilation. The characterizations enable us to: (a) p rove the correctness of the algorithms, and (b) partially order the al gorithms according to two standard performance measures: the number of nodes visited, and the number of consistency checks performed. Among other results, we prove the correctness of Backjumping and Conflict-Di rected Backjumping, and show that Forward Checking never visits more n odes than Backjumping. Our approach leads us also to propose a modific ation to two hybrid backtracking algorithms, Backmarking with Backjump ing (BMJ) and Backmarking with Conflict-Directed Backjumping (BM-CBJ), so that they always perform fewer consistency checks than the origina l algorithms.