{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:09:24Z","timestamp":1750219764951,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T00:00:00Z","timestamp":1674000000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council (ERC) under the European Union\u2019s Horizon 2020 research and innovation program","award":["713999"],"award-info":[{"award-number":["713999"]}]},{"name":"Netherlands Organization for Scientific Research (NWO) under the Vidi program","award":["016.Vidi.189.037"],"award-info":[{"award-number":["016.Vidi.189.037"]}]},{"name":"National Science Foundation","award":["CCF-2015445"],"award-info":[{"award-number":["CCF-2015445"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,1,31]]},"abstract":"<jats:p>Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order logic with equality. In this article, we port inprocessing techniques to work with superposition, a leading first-order proof calculus, and we strengthen known preprocessing techniques. Specifically, we look into elimination of hidden literals, variables (predicates), and blocked clauses. Our evaluation using the Zipperposition prover confirms that the new techniques usefully supplement the existing superposition machinery.<\/jats:p>","DOI":"10.1145\/3565366","type":"journal-article","created":{"date-parts":[[2022,9,30]],"date-time":"2022-09-30T12:25:28Z","timestamp":1664540728000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["SAT-Inspired Eliminations for\u00a0Superposition"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7049-6847","authenticated-orcid":false,"given":"Petar","family":"Vukmirovi\u0107","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, HV Amsterdam, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8367-0936","authenticated-orcid":false,"given":"Jasmin","family":"Blanchette","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, HV Amsterdam, The Netherlands and Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, Vanduvre-l\u00e8s-Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,18]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59200-8_72"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/280474"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.217"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_13"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09595-y"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_16"},{"key":"e_1_3_2_9_2","first-page":"59","volume-title":"International Conference on Theory and Applications of Satisfiability Testing SAT 2004 (LNCS)","volume":"3542","author":"Biere Armin","year":"2004","unstructured":"Armin Biere. 2004. Resolve and expand. In International Conference on Theory and Applications of Satisfiability Testing SAT 2004 (LNCS). Holger H. Hoos and David G. Mitchell (Eds.), Vol. 3542. Springer, 59\u201370."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_10"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_4"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_3"},{"key":"e_1_3_2_13_2","first-page":"25","volume-title":"PAAR-2014 (EPiC Series in Computing)","author":"Bonacina Maria Paola","year":"2014","unstructured":"Maria Paola Bonacina and David A. Plaisted. 2014. SGGS theorem proving: An exposition. In PAAR-2014 (EPiC Series in Computing), Stephan Schulz, Leonardo de Moura, and Boris Konev (Eds.), Vol. 31. EasyChair, 25\u201338."},{"key":"e_1_3_2_14_2","first-page":"1","volume-title":"Handbook of Philosophical Logic (Handbook of Philosophical Logic)","author":"Carnielli Walter","year":"2007","unstructured":"Walter Carnielli, Marcelo E. Coniglio, and Jo\u00e3o Marcos. 2007. Logics of formal inconsistency. In Handbook of Philosophical Logic (Handbook of Philosophical Logic). Dov M. Gabbay and Franz Guenthner (Eds.), Vol. 14. Springer, 1\u201393."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_35"},{"key":"e_1_3_2_16_2","first-page":"172","volume-title":"International Symposium on Frontiers of Combining Systems FroCoS 2017 (LNCS)","author":"Cruanes Simon","year":"2017","unstructured":"Simon Cruanes. 2017. Superposition with structural induction. In International Symposium on Frontiers of Combining Systems FroCoS 2017 (LNCS). Clare Dixon and Marcelo Finger (Eds.), Vol. 10483. Springer, 172\u2013188."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_18_2","first-page":"1","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation VMCAI 2013 (LNCS)","author":"Moura Leonardo de","year":"2013","unstructured":"Leonardo de Moura and Dejan Jovanovi\u0107. 2013. A model-constructing satisfiability calculus. In International Workshop on Verification, Model Checking, and Abstract Interpretation VMCAI 2013 (LNCS). Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.), Vol. 7737. Springer, 1\u201312."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_20_2","first-page":"61","volume-title":"International Conference on Theory and Applications of Satisfiability Testing SAT 2005 (LNCS)","volume":"3569","author":"E\u00e9n Niklas","year":"2005","unstructured":"Niklas E\u00e9n and Armin Biere. 2005. Effective preprocessing in SAT through variable and clause elimination. In International Conference on Theory and Applications of Satisfiability Testing SAT 2005 (LNCS). Fahiem Bacchus and Toby Walsh (Eds.), Vol. 3569. Springer, 61\u201375."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9150-9"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_14"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.5555\/230183"},{"key":"e_1_3_2_24_2","unstructured":"Jon William Freeman. 1995. Improvements to Propositional Satisfiability Search Algorithms . Ph.D. Dissertation. University of Pennsylvania."},{"key":"e_1_3_2_25_2","first-page":"425","volume-title":"International Conference on Principles of Knowledge Representation and Reasoning (KR\u201992)","author":"Gabbay Dov M.","year":"1992","unstructured":"Dov M. Gabbay and Hans J\u00fcrgen Ohlbach. 1992. Quantifier elimination in second-order predicate logic. In International Conference on Principles of Knowledge Representation and Reasoning (KR\u201992), Bernhard Nebel, Charles Rich, and William R. Swartout (Eds.). Morgan Kaufmann, 425\u2013435."},{"key":"e_1_3_2_26_2","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"Gallier Jean H.","year":"1987","unstructured":"Jean H. Gallier. 1987. Logic for Computer Science: Foundations of Automatic Theorem Proving. Wiley."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_7"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_26"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21581-0_17"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_22"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_17"},{"key":"e_1_3_2_33_2","first-page":"31","volume-title":"LPAR-21 (EPiC Series in Computing)","author":"Kiesl Benjamin","year":"2017","unstructured":"Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, and Armin Biere. 2017. Blocked clauses in first-order logic. In LPAR-21 (EPiC Series in Computing). Thomas Eiter and David Sands (Eds.), Vol. 46. EasyChair, 31\u201348."},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(99)00037-2"},{"key":"e_1_3_2_35_2","first-page":"102","volume-title":"Haifa Verification Conference HVC 2012 (LNCS)","volume":"7857","author":"Manthey Norbert","year":"2012","unstructured":"Norbert Manthey, Marijn Heule, and Armin Biere. 2012. Automated reencoding of Boolean formulas. In Haifa Verification Conference HVC 2012 (LNCS). Armin Biere, Amir Nahir, and Tanja E. J. Vos (Eds.), Vol. 7857. Springer, 102\u2013117."},{"key":"e_1_3_2_36_2","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"131","volume-title":"Handbook of Satisfiability","author":"Marques-Silva Joao P.","year":"2009","unstructured":"Joao P. Marques-Silva, Ines Lynce, and Sharad Malik. 2009. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability. Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press, 131\u2013153."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005843632307"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61511-3_77"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/778522.778535"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"e_1_3_2_42_2","first-page":"611","volume-title":"International Joint Conference on Artificial Intelligence 2001","author":"Riazanov Alexandre","year":"2001","unstructured":"Alexandre Riazanov and Andrei Voronkov. 2001. Splitting without backtracking. In International Joint Conference on Artificial Intelligence 2001. Bernhard Nebel (Ed.). Morgan Kaufmann, 611\u2013617."},{"issue":"2","key":"e_1_3_2_43_2","first-page":"111","article-title":"E\u2014A brainiac theorem prover","volume":"15","author":"Schulz Stephan","year":"2002","unstructured":"Stephan Schulz. 2002. E\u2014A brainiac theorem prover. AI Communications 15, 2\u20133 (2002), 111\u2013126.","journal-title":"AI Communications"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"e_1_3_2_46_2","first-page":"276","volume-title":"International Conference on Theory and Applications of Satisfiability Testing SAT 2004 (LNCS)","volume":"3542","author":"Subbarayan Sathiamoorthy","year":"2004","unstructured":"Sathiamoorthy Subbarayan and Dhiraj K. Pradhan. 2004. NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In International Conference on Theory and Applications of Satisfiability Testing SAT 2004 (LNCS). Holger H. Hoos and David G. Mitchell (Eds.), Vol. 3542. Springer, 276\u2013291."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9407-7"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-190627"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"e_1_3_2_50_2","first-page":"231","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design FMCAD 2021","author":"Vukmirovi\u0107 Petar","year":"2021","unstructured":"Petar Vukmirovi\u0107, Jasmin Blanchette, and Marijn J. H. Heule. 2021. SAT-inspired eliminations for superposition. In Proceedings of the Formal Methods in Computer-Aided Design FMCAD 2021. IEEE, 231\u2013240."},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_18"},{"key":"e_1_3_2_52_2","article-title":"A comprehensive framework for saturation theorem proving","author":"Waldmann Uwe","unstructured":"Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. A comprehensive framework for saturation theorem proving. Journal of Automated Reasoning (accepted). Retrieved from https:\/\/matryoshka-project.github.io\/pubs\/saturate_article.pdf.","journal-title":"Journal of Automated Reasoning"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3565366","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3565366","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:12Z","timestamp":1750178232000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3565366"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,18]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3565366"],"URL":"https:\/\/doi.org\/10.1145\/3565366","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2023,1,18]]},"assertion":[{"value":"2022-03-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-22","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}