A VARIATIONAL METHOD FOR ANALYZING UNIT CLAUSE SEARCH

We expose a variational method for analysing algorithms, as applied to analyse the algorithm UC, which is the Davis-Putnam procedure for a s et of clauses of three literals. The variable from a unit clause or, i f there is none, the first remaining variable from a fixed list is cho sen. The algorithm UC finds all the solutions as a set of cylinders. F ollowing the nomenclature of Purdom [J. Inform. Process., 13 (1990), p p. 449-455], we call this algorithm ''unit clause backtracking with cy linders of solutions.'' First we give an expression for the number of nodes of the calculation trees of all the inputs. Then we use a variat ional method to calculate the base beta of the principal exponential p art of the average time of calculation T. This ''exponential base'' is the maximum of three elementary functions f(i) of four real variables . These functions are defined on the product of the half positive real line by the 3-dimensional unit real cube. We finally obtain the follo wing short statement. Let upsilon be the number of the variables. Let c be the number of the clauses. Let gamma = c/upsilon > 1. Let gamma b e constant when upsilon grows to infinity. The principal exponential p art of the average time of UC is BU where [GRAPHICS] We mean that lim( upsilon-->infinity) T-1/upsilon = beta. As a first consequence of our method we match UC, with the algorithm B without rearrangement (i.e., with a fixed order for introducing the variables). This gives a proof to a conjecture of P.W. Purdom [Artif. Intell., 21 (1983). pp. 117-133 ].