SAT Solving for Variants of First-Order Subsumption

TL;DR

This work tackles the efficiency bottleneck of first-order subsumption by embedding a tailored SAT-solving engine into saturation-based theorem proving. It introduces generic and optimized SAT encodings for subsumption and subsumption resolution, along with a lightweight SAT solver integrated into Vampire, to accelerate redundancy elimination during saturation. A learning component uses decision trees to dynamically select the most effective encoding, and pruning plus cutoff strategies reduce overhead, resulting in substantial speedups on standard benchmarks (e.g., improved forward simplification by a factor of 1.36 and notable reductions in subsumption times). The approach demonstrates that SAT-based reasoning can effectively handle variants of subsumption in large-scale first-order proving, with practical impact on verification, synthesis, and security-oriented prove/disprove tasks. Future work includes extending to equality with theory reasoning and exploring SMT-style solvers for richer subsumption reasoning.

Abstract

Automated reasoners, such as SAT/SMT solvers and first-order provers, are becoming the backbones of rigorous systems engineering, being used for example in applications of system verification, program synthesis, and cybersecurity. Automation in these domains crucially depends on the efficiency of the underlying reasoners towards finding proofs and/or counterexamples of the task to be enforced. In order to gain efficiency, automated reasoners use dedicated proof rules to keep proof search tractable. To this end, (variants of) subsumption is one of the most important proof rules used by automated reasoners, ranging from SAT solvers to first-order theorem provers and beyond. It is common that millions of subsumption checks are performed during proof search, necessitating efficient implementations. However, in contrast to propositional subsumption as used by SAT solvers and implemented using sophisticated polynomial algorithms, first-order subsumption in first-order theorem provers involves NP-complete search queries, turning the efficient use of first-order subsumption into a huge practical burden. In this paper we argue that the integration of a dedicated SAT solver opens up new venues for efficient implementations of first-order subsumption and related rules. We show that, by using a flexible learning approach to choose between various SAT encodings of subsumption variants, we greatly improve the scalability of first-order theorem proving. Our experimental results demonstrate that, by using a tailored SAT solver within first-order reasoning, we gain a large speedup in solving state-of-the-art benchmarks.

Figures (8)

• Figure 1: Success rates of the SAT solver depending on the number of ticks (ticks are displayed on the horizontal axes). The problems taking the longest time are less likely to succeed.
• Figure 2: Trade-off between positive instances lost when cutting off, and the number of ticks saved.
• Figure 3: Advantage of the model over the perfect model for different depths. The green dashed line shows the baseline advantage of the indirect SAT encoding over the perfect model.
• Figure 4: Decision trees of different depths. The orange nodes choose the indirect encoding, and the blue nodes choose the direct encoding.
• Figure 5: Decision tree from Figure \ref{['fig:tree-depth-3']} in pseudo-code.

Theorems & Definitions (48)

• Definition 1: Subsumption
• Example 1
• Definition 2: Subsumption Resolution
• Example 2
• Theorem 1: Subsumption Constraints
• proof
• Theorem 2: Subsumption Resolution Constraints
• proof
• Definition 3: Match set
• Definition 4: Substitution Compatibility