{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:17:13Z","timestamp":1760660233707,"version":"build-2065373602"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,11,11]],"date-time":"2024-11-11T00:00:00Z","timestamp":1731283200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,11,11]],"date-time":"2024-11-11T00:00:00Z","timestamp":1731283200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TU Wien"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/s10703-024-00454-1","type":"journal-article","created":{"date-parts":[[2024,11,11]],"date-time":"2024-11-11T11:35:43Z","timestamp":1731324943000},"page":"27-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SAT solving for variants of first-order subsumption"],"prefix":"10.1007","volume":"67","author":[{"given":"Robin","family":"Coutelier","sequence":"first","affiliation":[]},{"given":"Jakob","family":"Rath","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Rawson","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,11]]},"reference":[{"issue":"6","key":"454_CR1","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1109\/MS.2017.4121212","volume":"34","author":"KRM Leino","year":"2017","unstructured":"Leino KRM (2017) Accessible software verification with Dafny. IEEE Softw 34(6):94\u201397","journal-title":"IEEE Softw"},{"doi-asserted-by":"crossref","unstructured":"Clochard M, March\u00e9 C, Paskevich A (2020) Deductive verification with ghost monitors. In: Proceedings of POPL, pp 2\u20131226","key":"454_CR2","DOI":"10.1145\/3371070"},{"unstructured":"Georgiou P, Gleiss B, Kov\u00e1cs L (2020) Trace logic for inductive loop reasoning. In: Proceedings of FMCAD, pp 255\u2013263","key":"454_CR3"},{"issue":"3","key":"454_CR4","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli A, Gurfinkel A, Chaki S (2016) SMT-based model checking for recursive programs. Form Methods Syst Des 48(3):175\u2013205","journal-title":"Form Methods Syst Des"},{"doi-asserted-by":"crossref","unstructured":"Padon O, McMillan KL, Panda A, Sagiv M, Shoham S (2016) Ivy: safety verification by interactive generalization. In: Proceedings of PLDI, pp 614\u2013630","key":"454_CR5","DOI":"10.1145\/2908080.2908118"},{"unstructured":"Asadi S, Blicha M, Hyv\u00e4rinen AEJ, Fedyukovich G, Sharygina N (2020)Incremental verification by SMT-based summary repair. In: Proceedings of FMCAD, pp 77\u201382","key":"454_CR6"},{"doi-asserted-by":"publisher","unstructured":"Garcia-Contreras I, K, HGV, Shoham S, Gurfinkel A (2023) Fast approximations of quantifier elimination. In: Proceedings of CAV, pp 64\u201386 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_4","key":"454_CR7","DOI":"10.1007\/978-3-031-37703-7_4"},{"unstructured":"Pick L, Fedyukovich G, Gupta A (2020) Automating modular verification of secure information flow. In: Proceedings of FMCAD, pp 158\u2013168","key":"454_CR8"},{"doi-asserted-by":"crossref","unstructured":"Mart\u00ednez G, Ahman D, Dumitrescu V, Giannarakis N, Hawblitzel C, Hritcu C, Narasimhamurthy M, Paraskevopoulou Z, Pit-Claudel C, Protzenko J, Ramananandro T, Rastogi A, Swamy N (2019) Meta-F$$^\\star$$: proof automation with SMT, tactics, and metaprograms. In: Proceedings of ESOP, pp 30\u201359","key":"454_CR9","DOI":"10.1007\/978-3-030-17184-1_2"},{"doi-asserted-by":"publisher","unstructured":"Veronese L, Farinier B, Bernardo P, Tempesta M, Squarcina M, Maffei M (2023) WebSpec: towards machine-checked analysis of browser security mechanisms. In: SP, pp 2761\u20132779 . https:\/\/doi.org\/10.1109\/SP46215.2023.10179465","key":"454_CR10","DOI":"10.1109\/SP46215.2023.10179465"},{"doi-asserted-by":"publisher","unstructured":"Brugger LS, Kov\u00e1cs L, Komel AP, Rain S, Rawson M (2023) CheckMate: automated game-theoretic security reasoning. In: CCS, pp 1407\u20131421. https:\/\/doi.org\/10.1145\/3576915.3623183","key":"454_CR11","DOI":"10.1145\/3576915.3623183"},{"issue":"2\u20134","key":"454_CR12","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere A (2008) PicoSAT essentials. J Satisf Boolean Model Comput 4(2\u20134):75\u201397","journal-title":"J Satisf Boolean Model Comput"},{"doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Proceedings of TACAS, pp 337\u2013340","key":"454_CR13","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"crossref","unstructured":"Barbosa H, Barrett CW, Brain M, Kremer G, Lachnitt H, Mann M, Mohamed A, Mohamed M, Niemetz A, N\u00f6tzli A, Ozdemir A, Preiner M, Reynolds A, Sheng Y, Tinelli C, Zohar Y (2022) CVC5: a versatile and industrial-strength SMT solver. In: Proceedings of TACAS, pp 415\u2013442","key":"454_CR14","DOI":"10.1007\/978-3-030-99524-9_24"},{"doi-asserted-by":"crossref","unstructured":"Weidenbach C, Dimova D, Fietzke A, Kumar R, Suda M, Wischnewski P (2009) SPASS version 3.5. In: Proceedings of CADE, pp 140\u2013145","key":"454_CR15","DOI":"10.1007\/978-3-642-02959-2_10"},{"doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs L, Voronkov A (2013) First-order theorem proving and vampire. In: CAV, pp 1\u201335","key":"454_CR16","DOI":"10.1007\/978-3-642-39799-8_1"},{"doi-asserted-by":"crossref","unstructured":"Schulz S, Cruanes S, Vukmirovic P (2019) Faster, higher, stronger: E 2.3. In: Proceedings of CADE, pp 495\u2013507","key":"454_CR17","DOI":"10.1007\/978-3-030-29436-6_29"},{"doi-asserted-by":"crossref","unstructured":"Cruanes S (2017) Superposition with structural induction. In: Proceedings of FroCoS, pp 172\u2013188","key":"454_CR18","DOI":"10.1007\/978-3-319-66167-4_10"},{"issue":"3\u20134","key":"454_CR19","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1016\/j.jsc.2005.09.007","volume":"41","author":"B Buchberger","year":"2006","unstructured":"Buchberger B (2006) Bruno Buchberger\u2019s PhD thesis 1965: an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. J Symb Comput 41(3\u20134):475\u2013511. https:\/\/doi.org\/10.1016\/j.jsc.2005.09.007","journal-title":"J Symb Comput"},{"doi-asserted-by":"publisher","unstructured":"Nieuwenhuis R, Rubio A (2001) Paramodulation-based theorem proving. In: Handbook of automated reasoning, pp 371\u2013443. https:\/\/doi.org\/10.1016\/b978-044450813-3\/50009-6","key":"454_CR20","DOI":"10.1016\/b978-044450813-3\/50009-6"},{"issue":"1","key":"454_CR21","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson JA (1965) A machine-oriented logic based on the resolution principle. J ACM 12(1):23\u201341. https:\/\/doi.org\/10.1145\/321250.321253","journal-title":"J ACM"},{"issue":"3","key":"454_CR22","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair L, Ganzinger H (1994) Rewrite-based equational theorem proving with selection and simplification. J Log Comput 4(3):217\u2013247","journal-title":"J Log Comput"},{"doi-asserted-by":"publisher","unstructured":"Biere A (2004) Resolve and expand. In: Proceedings of SAT. https:\/\/doi.org\/10.1007\/11527695_5","key":"454_CR23","DOI":"10.1007\/11527695_5"},{"doi-asserted-by":"crossref","unstructured":"Sekar R, Ramakrishnan IV, Voronkov A (2001) Term indexing. In: Handbook of automated reasoning, pp 1853\u20131964","key":"454_CR24","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"doi-asserted-by":"crossref","unstructured":"Nieuwenhuis R, Hillenbrand T, Riazanov A, Voronkov A (2001) On the evaluation of indexing techniques for theorem proving. In: Proceedings of IJCAR, pp 257\u2013271","key":"454_CR25","DOI":"10.1007\/3-540-45744-5_19"},{"doi-asserted-by":"crossref","unstructured":"Schulz S (2013) Simple and efficient clause subsumption with feature vector indexing. In: Automated reasoning and mathematics\u2014essays in memory of William W. McCune, pp 45\u201367","key":"454_CR26","DOI":"10.1007\/978-3-642-36675-8_3"},{"doi-asserted-by":"crossref","unstructured":"Kapur D, Narendran P (1986) NP-completeness of the set unification and matching problems. In: Proceedings of IJCAR, pp 489\u2013495","key":"454_CR27","DOI":"10.1007\/3-540-16780-3_113"},{"unstructured":"Rath J, Biere A, Kov\u00e1cs L (2022) First-order subsumption via SAT solving. In: FMCAD, p 160","key":"454_CR28"},{"doi-asserted-by":"publisher","unstructured":"Coutelier R, Kov\u00e1cs L, Rawson M, Rath J (2023) SAT-based subsumption resolution. In: Proceedings of CADE, pp 190\u2013206. https:\/\/doi.org\/10.1007\/978-3-031-38499-8_11","key":"454_CR29","DOI":"10.1007\/978-3-031-38499-8_11"},{"doi-asserted-by":"crossref","unstructured":"Gleiss B, Kov\u00e1cs L, Rath J (2020) Subsumption demodulation in first-order theorem proving. In: Proceedings of the of IJCAR, pp 297\u2013315","key":"454_CR30","DOI":"10.1007\/978-3-030-51074-9_17"},{"doi-asserted-by":"publisher","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) An extensible SAT-solver. In: Proceedings of SAT, pp 502\u2013518. https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","key":"454_CR31","DOI":"10.1007\/978-3-540-24605-3_37"},{"doi-asserted-by":"publisher","unstructured":"Biere A, Froleyks N, Wang W (2023) CadiBack: extracting backbones with CaDiCaL. In: Proceedings of SAT, pp 3\u20131312. https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.3","key":"454_CR32","DOI":"10.4230\/LIPICS.SAT.2023.3"},{"issue":"3","key":"454_CR33","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/S10703-023-00421-2","volume":"60","author":"M Fleury","year":"2022","unstructured":"Fleury M, Biere A (2022) Mining definitions in Kissat with Kittens. Formal Methods Syst Des 60(3):381\u2013404. https:\/\/doi.org\/10.1007\/S10703-023-00421-2","journal-title":"Formal Methods Syst Des"},{"doi-asserted-by":"crossref","unstructured":"Marques-Silva J, Lynce I, Malik S (2021) Conflict-driven clause learning SAT solvers. In: Handbook of satisfiability. frontiers in artificial intelligence and applications, vol 336, pp 133\u2013182. Chapter 4","key":"454_CR34","DOI":"10.3233\/FAIA200987"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of DAC, pp 530\u2013535","key":"454_CR35","DOI":"10.1145\/378239.379017"},{"unstructured":"Frisch AM, Giannaros PA (2010) SAT encodings of the at-most-k constraint. some old, some new, some fast, some slow. In: Proceedings of WS on constraint modelling and reformulation","key":"454_CR36"},{"key":"454_CR37","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W McCune","year":"1997","unstructured":"McCune W, Wos L (1997) Otter\u2014the CADE-13 competition incarnations. J Autom Reason 18:211\u2013220","journal-title":"J Autom Reason"},{"doi-asserted-by":"publisher","unstructured":"Voronkov A (2014) AVATAR: the architecture for first-order theorem provers. In: Proceedings of CAV, pp 696\u2013710. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46","key":"454_CR38","DOI":"10.1007\/978-3-319-08867-9_46"},{"unstructured":"Biere A, Fazekas K, Fleury M, Heisinger M (2020) CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Proceedings of SAT competition 2020: solver and benchmark descriptions, pp 50\u201353. http:\/\/hdl.handle.net\/10138\/318450","key":"454_CR39"},{"issue":"4","key":"454_CR40","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe G (2017) The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J Autom Reason 59(4):483\u2013502","journal-title":"J Autom Reason"},{"key":"454_CR41","first-page":"2825","volume":"12","author":"F Pedregosa","year":"2011","unstructured":"Pedregosa F, Varoquaux G, Gramfort A, Michel V, Thirion B, Grisel O, Blondel M, Prettenhofer P, Weiss R, Dubourg V, Vanderplas J, Passos A, Cournapeau D, Brucher M, Perrot M, Duchesnay E (2011) Scikit-learn: machine learning in python. J Mach Learn Res 12:2825\u20132830","journal-title":"J Mach Learn Res"},{"unstructured":"Goodfellow IJ, Bengio Y, Courville AC (2016) Deep learning. Adaptive computation and machine learning. http:\/\/www.deeplearningbook.org\/","key":"454_CR42"},{"issue":"1","key":"454_CR43","first-page":"1","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer D, L\u00f6we S, Wendler P (2017) Reliable benchmarking: requirements and solutions. J. Softw Tools Technol Transf 21(1):1\u201329","journal-title":"J. Softw Tools Technol Transf"},{"unstructured":"Tange O (2018) GNU parallel 2018","key":"454_CR44"},{"doi-asserted-by":"crossref","unstructured":"Tammet T (1998) Towards efficient subsumption. In: Proceedings of CADE, pp 427\u2013441","key":"454_CR45","DOI":"10.1007\/BFb0054276"},{"issue":"2","key":"454_CR46","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G Gottlob","year":"1985","unstructured":"Gottlob G, Leitsch A (1985) On the efficiency of subsumption algorithms. J ACM 32(2):280\u2013295","journal-title":"J ACM"},{"doi-asserted-by":"crossref","unstructured":"Gottlob G, Leitsch A (1985) Fast subsumption algorithms. In: Proceedings of EUROCAL \u201985, pp 64\u201377","key":"454_CR47","DOI":"10.1007\/3-540-15984-3_239"},{"doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs L, Voronkov A (2013) First-order theorem proving and vampire. In: CAV, pp 1\u201335. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","key":"454_CR48","DOI":"10.1007\/978-3-642-39799-8_1"},{"doi-asserted-by":"crossref","unstructured":"Liffiton MH, Maglalang JC (2012) A cardinality solver: more expressive constraints for free. In: Proceedings of SAT, pp 485\u2013486","key":"454_CR49","DOI":"10.1007\/978-3-642-31612-8_47"},{"doi-asserted-by":"crossref","unstructured":"Gebser M, Kaminski R, Kaufmann B, Schaub T (2009) On the implementation of weight constraint rules in conflict-driven ASP solvers. In: Proceedings of ICLP, pp 250\u2013264","key":"454_CR50","DOI":"10.1007\/978-3-642-02846-5_23"},{"doi-asserted-by":"crossref","unstructured":"Walsh T (2000) SAT v CSP. In: Proceedings of CP, pp 441\u2013456","key":"454_CR51","DOI":"10.1007\/3-540-45349-0_32"},{"unstructured":"Ryan L (2004) Efficient algorithms for clause-learning SAT solvers. Master\u2019s thesis, Simon Fraser University","key":"454_CR52"},{"issue":"3","key":"454_CR53","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/S10817-019-09516-0","volume":"64","author":"MJH Heule","year":"2020","unstructured":"Heule MJH, Kiesl B, Biere A (2020) Strong extension-free proof systems. J Autom Reason 64(3):533\u2013554. https:\/\/doi.org\/10.1007\/S10817-019-09516-0","journal-title":"J Autom Reason"},{"doi-asserted-by":"publisher","unstructured":"E\u00e9n N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: Proceedings of SAT, vol 3569, pp 61\u201375. https:\/\/doi.org\/10.1007\/11499107_5","key":"454_CR54","DOI":"10.1007\/11499107_5"},{"doi-asserted-by":"publisher","unstructured":"Biere A, J\u00e4rvisalo M, Kiesl B (2021) Preprocessing in SAT solving. In: Handbook of satisfiability\u2014second edition. Frontiers in artificial intelligence and applications, vol 336, pp 391\u2013435. https:\/\/doi.org\/10.3233\/FAIA200992","key":"454_CR55","DOI":"10.3233\/FAIA200992"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00454-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00454-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00454-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T10:33:31Z","timestamp":1760610811000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00454-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,11]]},"references-count":55,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["454"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00454-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2024,11,11]]},"assertion":[{"value":"20 January 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 May 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 November 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}