A Theoretical Evaluation of Selected Backtracking Algorithms

In recent years, numerous new backtracking algorithms have been proposed. The algorithms are usually evaluated by empirical testing. This method, however, has its limitations. Our thesis adopts a different, purely theoretical approach, which is based on characterizations of the sets of search tree nodes visited by the backtracking algorithms. A new notion of inconsistency between instantiations and variables is introduced, a useful tool for describing such well-known concepts as backtrack, backjump, and domain annihilation. The characterizations enable us to: (a) prove the correctness of the algorithms, and (b) partially order the algorithms according to two standard performance measures: the number of visited nodes, and the number of performed consistency checks. Among other results, we prove, for the first time, the correctness of Backjumping and Conflict-Directed Backjumping, and show that Forward Checking never visits more nodes than Backjumping. Our approach leads us also to propo..