Performance of Clause Selection Heuristics for Saturation-Based
  Theorem Proving

             Stephan Schulz, Martin Moehrmann

We analyze the performance of various clause selection heuristics
for saturating first-order theorem provers. These heuristics include
elementary first-in/first-out and symbol counting, but also
interleaved heuristics and a complex heuristic with goal-directed
components.

We can both confirm and dispel some parts of developer folklore. Key
results include: (1) Simple symbol counting heuristics beat
first-in/first-out, but by a surprisingly narrow margin. (2) Proofs
are typically small, not only compared to all generated clauses, but
also compared to the number of selected and processed clauses. In
particular, only a small number of \emph{given clauses} (clauses
selected for processing) contribute to any given proof. However, the
results are extremely diverse and there are extreme outliers. (3)
Interleaving selection of the given clause according to different
clause evaluation heuristics not only beats the individual
elementary heuristics, but also their union - i.e. it shows a
synergy not achieved by simple strategy scheduling. (4) Heuristics
showing better performance typically achieve a higher ratio of
\emph{given-clause} utilization, but even a fairly small improvement
leads to better outcomes. There seems to be a huge potential for
further progress.