Average Time Analysis of Clause Order Backtracking
Khaled M. Bugrara, Paul Walton Purdom · SIAM Journal on Computing · 1993
Backtracking aigorithms solve problems by selecting a variable and assigning each possible value to the variable. The resulting subproblems are simplified and solved recursively. Simple backtracking selects variables in a fixed order. Clause order backtracking selects variables from the first nontrivial clause that has not yet been satisfied. Formulas are given for the average time used by clause order backtracking when solving random CNF satisfiability problems, where the problem sets have v variables, t clauses, and a probability p of a literal being in a clause. The average time for clause order backtracking is always less than that for simple backtracking. It leads to polynomial time under many conditions where simple backtracking uses exponential average time. Cases where clause order backtracking uses average time less than $v^n $ (in the limit of v going to infinity) include $p \sqrt {[\ln t + {{{{(\ln v)} / 2}]} / v}} $. (The second result needs a slight increase in the coefficient of $\ln t$ when t increases faster than $v^{\ln v} $.)