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
].