First-Order Subsumption via SAT Solving

被引:2
作者
Rath, Jakob [1 ]
Biere, Armin [2 ]
Kovacs, Laura [1 ]
机构
[1] TU Wien, Vienna, Austria
[2] Univ Freiburg, Freiburg, Germany
来源
2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD | 2022年 / 3卷
基金
欧洲研究理事会;
关键词
rst-order subsumption; multi-literal matching; automated theorem proving; satisfiability checking; VERIFICATION;
D O I
10.34727/2022/isbn.978-3-85448-053-2_22
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Automated reasoners, such as SAT/SMT solvers and first-order provers, are becoming the backbones of applications of formal methods, for example in automating deductive verification, program synthesis, and security analysis. Automation in these formal methods 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, 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 integration of a dedicated SAT solver provides a remedy towards efficient implementation of first-order subsumption and related rules, and thus further increasing scalability of first-order theorem proving towards applications of formal methods. Our experimental results demonstrate that, by using a tailored SAT solver within first-order reasoning, we gain a large speed-up in state-of-the-art benchmarks.
引用
收藏
页码:160 / 169
页数:10
相关论文
共 41 条
[1]  
Asadi Sepideh, 2020, 2020 Formal Methods in Computer Aided Design (FMCAD), P77, DOI 10.34727/2020/isbn.978-3-85448-042-6_14
[2]  
Bachmair L., 1994, Journal of Logic and Computation, V4, P217, DOI 10.1093/logcom/4.3.217
[3]   cvc5: A Versatile and Industrial-Strength SMT Solver [J].
Barbosa, Haniel ;
Barrett, Clark ;
Brain, Martin ;
Kremer, Gereon ;
Lachnitt, Hanna ;
Mann, Makai ;
Mohamed, Abdalrhman ;
Mohamed, Mudathir ;
Niemetz, Aina ;
Notzli, Andres ;
Ozdemir, Alex ;
Preiner, Mathias ;
Reynolds, Andrew ;
Sheng, Ying ;
Tinelli, Cesare ;
Zohar, Yoni .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 :415-442
[4]  
Barthe G, 2019, 2019 FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), P170, DOI 10.23919/FMCAD.2019.8894277
[5]   Reliable benchmarking: requirements and solutions [J].
Beyer, Dirk ;
Loewe, Stefan ;
Wendler, Philipp .
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (01) :1-29
[6]  
Biere A., 2019, DEP COMPUTER SCI S B, P8
[7]  
Biere A., 2008, Journal on Satisfiability, Boolean Modeling and Computation, V4, P75, DOI 10.3233/sat190039
[8]   Evaluating CDCL Variable Scoring Schemes [J].
Biere, Armin ;
Froehlich, Andreas .
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015, 2015, 9340 :405-422
[10]  
Clochard Martin, 2020, P POPL