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/firstout, 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 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 given-clause utilization, but even a fairly small improvement leads to better outcomes. There seems to be a huge potential for further progress.
展开▼
