Layered Clause Selection for Saturation-based Theorem Proving

Clause selection is one of the main heuristic decision points in navigating proof search of saturation-based theorem provers. A recently developed layered clause selection framework allows one to boost a basic clause selection heuristic by organising clauses into groups of more or less promising ones according to a specified numerical feature. In this work, we investigate this framework in depth and introduce, in addition to a previously presented feature (based on the amount of theory reasoning in the derivation of a clause), three new features for clause selection (tracking relatedness to the goal, the number of split dependencies in the AVATAR architecture, and closeness to the Horn fragment, respectively). We implemented the resulting clause selection heuristics in the state-of-the-art saturation-based theorem prover Vampire and present an evaluation of these new clause-selection strategies and their combinations over the TPTP and SMTLIB libraries