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.

翻译：自动推理器，如SAT/SMT求解器和一阶证明器，正逐渐成为严格系统工程的核心支柱，被应用于系统验证、程序综合和网络安全等领域。这些领域的自动化关键依赖于底层推理器在寻找待执行任务的证明和/或反例方面的效率。为提高效率，自动推理器使用专用的证明规则以保持证明搜索的可处理性。为此，（变体形式的）归结是自动推理器（从SAT求解器到一阶定理证明器乃至更广泛的系统）所使用的最重要的证明规则之一。在证明搜索过程中执行数百万次归结检查是常见情况，这需要高效的实现。然而，与SAT求解器所使用的、通过复杂多项式算法实现的命题归结不同，一阶定理证明器中的一阶归结涉及NP完全搜索查询，这使得一阶归结的高效使用成为巨大的实际负担。本文认为，集成专用的SAT求解器为一阶归结及相关规则的高效实现开辟了新途径。我们证明，通过采用灵活的学习方法在各种归结变体的SAT编码之间进行选择，我们极大地提升了一阶定理证明的可扩展性。我们的实验结果表明，通过在一阶推理中使用定制的SAT求解器，我们在求解前沿基准测试时获得了显著的加速。