SAT in Saturation: A Satisfied Match

Abstract

aturation is the leading concept behind the proof-search algorithms of state-of-the-art first-order theorem provers [3, 11, 10]. The key idea behind saturation-based proof search is to reduce the problem of proving validity of a first-order formula to the problem of establishing unsatisfiability of the respective formula, by using a sound inference system, such as resolution and superposition [2, 7]. Central to efficient saturation-based proof search is the implementation of redundancy in the form of simplification rules [9, 6]: such rules do not add new formulas to search space, but instead simplify/delete redundant formulas from the search space, while not loosing refutational completeness of superposition. Redundancy in first-order theorem proving is controlled via term/clause ordering and literal selection functions in extension of standard superposition: redundant clauses are logical consequences of smaller clauses with respect to the considered ordering. While redundancy is essential for efficient proof search, establishing whether an arbitrary first- order formula is redundant is as hard as proving whether it is valid. First-order provers therefore implement sufficient conditions towards proving redundancy, so that these conditions can be efficiently checked, ideally using only syntactic arguments over formulas. One such condition comes with the notion of subsumption, yielding one of the most important simplification rules in automated reasoners [1]. It is common that millions of subsumption checks are performed during a single solver run [8]. However, in contrast to propositional subsumption as used by SAT solvers and implemented using sophisticated polynomial algorithms, first-order subsumption in first-order theorem proving involves NP-complete search queries, turning the efficient use of first-order subsumption into a huge practical burden. This talks presents a tailored integration of SAT solving for detecting variants of subsumption in superposition. Key to our approach is retrieving clauses from the search space and checking whether subsumption with retrieved clauses can be applied, using multi-literal matching. A solution to our SAT-based encoding gives a concrete application of (variants of) subsumption, allowing the first-order prover to apply that instance of subsumption as a simplification rule during saturation [5, 8, 4]. Our SAT encoding captures subset relations among literals/clauses and formalizes matching of literals between inference premises/conclusions. We show that SAT encodings improve literal matching, and thus subsumption, in first-order theorem proving. In particular, our experimental results using the Vampire prover demonstrate the practical benefits of using SAT solving for variants of first-order subsumption.