Great variation in execution time
nVery short and very long runs for different randomized runs on same instances
nHeavy-tailed distribution (Pareto)
Very short
Very long
 Control of Computation:
 Restarts in Satistifiabilty Solvers
Eric Horvitz, April 5, 2003
In 1960, Davis-Putnam procedure was introduced as a theorem-proving technique suitable for automation. It deals with classical propositional and first-order logic.
Davis-Putnam procedure deals with a disjunction of clause sets, called a block.
This procedure involves repeated rewriting of a block into an equivalent block using simple rewriting rules. Each of these rewriting rules takes some clause set in a block and replace it by one or more of others. The aim is to produce a block that can easily be seen as satisfactory or not.