{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T22:29:57Z","timestamp":1783549797874,"version":"3.55.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T00:00:00Z","timestamp":1654041600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,24]],"date-time":"2023-04-24T00:00:00Z","timestamp":1682294400000},"content-version":"vor","delay-in-days":327,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NFN","award":["S11408-23 (RiSE)"],"award-info":[{"award-number":["S11408-23 (RiSE)"]}]},{"name":"State of Upper Austria","award":["LIT AI Lab"],"award-info":[{"award-number":["LIT AI Lab"]}]},{"name":"Albert-Ludwigs-Universit\u00e4t Freiburg im Breisgau"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Bounded variable elimination is one of the most important preprocessing techniques in SAT solving. It benefits from discovering functional dependencies in the form of definitions encoded in the CNF. While the common approach pioneered in <jats:sc>SatELite<\/jats:sc> relies on syntactic pattern matching, our new approach uses cores produced by an embedded SAT solver, <jats:sc>Kitten<\/jats:sc>. In contrast to a similar semantic technique implemented in <jats:sc>Lingeling<\/jats:sc> based on BDD algorithms to generate irredundant CNFs, our new approach is able to generate DRAT proofs. We further discuss design choices for our embedded SAT solver Kitten. Experiments with Kissat show the effectiveness of this approach.\n<\/jats:p>","DOI":"10.1007\/s10703-023-00421-2","type":"journal-article","created":{"date-parts":[[2023,4,24]],"date-time":"2023-04-24T16:02:47Z","timestamp":1682352167000},"page":"381-404","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Mining definitions in Kissat with Kittens"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1705-3083","authenticated-orcid":false,"given":"Mathias","family":"Fleury","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,24]]},"reference":[{"key":"421_CR1","doi-asserted-by":"publisher","unstructured":"Balyo T, Fr\u00f6hlich A, Heule M, Biere A (2014) Everything you always wanted to know about blocked sets (but were afraid to ask). In: Sinz C, Egly U (eds.) Theory and applications of satisfiability testing - SAT 2014 - 17th international conference, held as part of the vienna summer of logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Lecture notes in computer science, vol.\u00a08561, pp. 317\u2013332. Springer. https:\/\/doi.org\/10.1007\/978-3-319-09284-3_24","DOI":"10.1007\/978-3-319-09284-3_24"},{"key":"421_CR2","unstructured":"Biere A (2003) About the SAT solvers Limmat, Compsat, Funex and the QBF solver Quantor , presentation for the SAT\u201903 SAT Solver Competition"},{"key":"421_CR3","doi-asserted-by":"publisher","unstructured":"Biere A (2004) Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) Theory and applications of satisfiability testing, 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10-13, Revised selected papers. Lecture notes in computer science, vol.\u00a03542, pp. 59\u201370. Springer. https:\/\/doi.org\/10.1007\/11527695_5","DOI":"10.1007\/11527695_5"},{"key":"421_CR4","unstructured":"Biere A (2010) Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Tech. Rep.\u00a010\/1, Johannes kepler university Linz, FMV reports series, institute for formal models and verification, Johannes Kepler University, Altenbergerstr.\u00a069, 4040 Linz, Austria. https:\/\/doi.org\/10.350\/fmvtr.2010-1"},{"key":"421_CR5","doi-asserted-by":"publisher","unstructured":"Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: Irwin, M.J. (ed.) Proceedings of the 36th conference on design automation, new orleans, LA, USA, June 21-25, pp. 317\u2013320. ACM Press (1999). https:\/\/doi.org\/10.1145\/309847.309942","DOI":"10.1145\/309847.309942"},{"key":"421_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:117\u2013148. https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Adv Comput"},{"key":"421_CR7","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:117\u2013148. https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Adv Comput"},{"key":"421_CR8","doi-asserted-by":"publisher","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Tools and algorithms for construction and analysis of systems, 5th international conference, TACAS \u201999, held as part of the european joint conferences on the theory and practice of software, ETAPS\u201999, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings. Lecture notes in computer science, vol.\u00a01579, pp. 193\u2013207. Springer. https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"421_CR9","doi-asserted-by":"publisher","unstructured":"Biere A, Clarke EM, Raimi R, Zhu Y (1999) Verifiying safety properties of a Power PC microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D.A. (eds.) Computer aided verification, 11th international conference, CAV \u201999, Trento, Italy, July 6-10, 1999, Proceedings. Lecture notes in computer science, vol.\u00a01633, pp. 60\u201371. Springer . https:\/\/doi.org\/10.1007\/3-540-48683-6_8","DOI":"10.1007\/3-540-48683-6_8"},{"key":"421_CR10","unstructured":"Biere A, Fazekas K, Fleury M, Heisinger M (2020) CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Heule M, J\u00e4rvisalo M, Suda M, Iser M, Balyo T (eds.) Proc.\u00a0of SAT competition 2020\u2013Solver and Benchmark Descriptions , to appear"},{"key":"421_CR11","unstructured":"Biere A, Fleury M (2021) Mining definitions in kissat with kittens. In: Workshop on the Pragmatics of SAT 2021 , http:\/\/www.pragmaticsofsat.org\/2021\/"},{"key":"421_CR12","unstructured":"Biere A, Fleury M, Heisinger M (2021) CaDiCaL, Kissat, Paracooba entering the SAT Competition 2021. In: Heule, M., J\u00e4rvisalo, M., Suda, M. (eds.) SAT Competition 2021, submitted"},{"key":"421_CR13","doi-asserted-by":"crossref","unstructured":"Biere A, J\u00e4rvisalo M, Kiesl B (2021) Preprocessing in SAT solving. In: Biere A, Heule M, van Maaren H, Walsh T (eds.) Handbook of satisfiability, Frontiers in artificial intelligence and applications, vol.\u00a0336, pp. 391 \u2013 435. IOS Press, 2nd edition edn","DOI":"10.3233\/FAIA336"},{"key":"421_CR14","doi-asserted-by":"publisher","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: Jhala R, Schmidt DA (eds.) Verification, model checking, and abstract interpretation-12th international conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings. Lecture notes in computer science, vol.\u00a06538, pp. 70\u201387. Springer . https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"421_CR15","doi-asserted-by":"publisher","unstructured":"Brummayer R, Lonsing F, Biere A (2010) Automated testing and debugging of SAT and QBF solvers. In: Strichman O, Szeider S (eds.) Theory and applications of satisfiability testing-SAT 2010, 13th international conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture notes in computer science, vol.\u00a06175, pp. 44\u201357. Springer . https:\/\/doi.org\/10.1007\/978-3-642-14186-7_6","DOI":"10.1007\/978-3-642-14186-7_6"},{"issue":"1","key":"421_CR16","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke EM, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1):7\u201334. https:\/\/doi.org\/10.1023\/A:1011276507260","journal-title":"Formal Methods Syst Des"},{"issue":"3","key":"421_CR17","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7(3):201\u2013215. https:\/\/doi.org\/10.1145\/321033.321034","journal-title":"J ACM"},{"key":"421_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: Bacchus F, Walsh T (eds.) Theory and applications of satisfiability testing, 8th international conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings. Lecture notes in computer science, vol.\u00a03569, pp. 61\u201375. Springer","DOI":"10.1007\/11499107_5"},{"key":"421_CR19","doi-asserted-by":"publisher","unstructured":"E\u00e9n N, Mishchenko A, S\u00f6rensson N (2007) Applying logic synthesis for speeding up SAT. In: Marques-Silva J, Sakallah KA (eds.) Theory and applications of satisfiability testing-SAT 2007, 10th international conference, Lisbon, Portugal, May 28-31, 2007, Proceedings. Lecture notes in computer science, vol.\u00a04501, pp. 272\u2013286. Springer. https:\/\/doi.org\/10.1007\/978-3-540-72788-0_26","DOI":"10.1007\/978-3-540-72788-0_26"},{"key":"421_CR20","doi-asserted-by":"publisher","unstructured":"van Eijk CAJ, Jess JAG (1996) Exploiting functional dependencies in finite state machine verification. In: 1996 European design and test conference, ED &TC 1996, Paris, France, March 11-14, 1996. pp. 9\u201314. IEEE computer society. https:\/\/doi.org\/10.1109\/EDTC.1996.494119","DOI":"10.1109\/EDTC.1996.494119"},{"key":"421_CR21","doi-asserted-by":"publisher","unstructured":"Fazekas K, Biere A, Scholl C (2019) Incremental inprocessing in SAT solving. In: Janota M, Lynce I (eds.) Theory and applications of satisfiability testing-SAT 2019-22nd international conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings. Lecture notes in computer science, vol. 11628, pp. 136\u2013154. Springer . https:\/\/doi.org\/10.1007\/978-3-030-24258-9_9","DOI":"10.1007\/978-3-030-24258-9_9"},{"key":"421_CR22","doi-asserted-by":"publisher","unstructured":"Heule M, Biere A (2013) Blocked clause decomposition. In: McMillan KL, Middeldorp A, Voronkov A (eds.) Logic for programming, artificial intelligence, and reasoning - 19th International conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. Lecture notes in computer science, vol.\u00a08312, pp. 423\u2013438. Springer . https:\/\/doi.org\/10.1007\/978-3-642-45221-5_29","DOI":"10.1007\/978-3-642-45221-5_29"},{"key":"421_CR23","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule M, J\u00e4rvisalo M, Lonsing F, Seidl M, Biere A (2015) Clause elimination for SAT and QSAT. J Artif Intell Res 53:127\u2013168. https:\/\/doi.org\/10.1613\/jair.4694","journal-title":"J Artif Intell Res"},{"key":"421_CR24","unstructured":"Iser M (2020) Recognition and exploitation of gate structure in SAT solving. Ph.D. thesis, Karlsruhe institute of technology, Germany , https:\/\/nbn-resolving.org\/urn:nbn:de:101:1-2020042904595660732648"},{"key":"421_CR25","doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo M, Biere A, Heule M (2010) Blocked clause elimination. In: Esparza J, Majumdar R, (eds.) Tools and algorithms for the construction and analysis of systems, 16th international conference, TACAS 2010, Held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Lecture Notes in computer science, vol.\u00a06015, pp. 129\u2013144. Springer . https:\/\/doi.org\/10.1007\/978-3-642-12002-2_10","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"421_CR26","doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo M, Heule M, Biere A (2012) Inprocessing rules. In: Gramlich B, Miller D, Sattler U (eds.) Automated reasoning-6th international joint conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings. Lecture notes in computer science, vol.\u00a07364, pp. 355\u2013370. Springer . https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"421_CR27","doi-asserted-by":"publisher","unstructured":"Jiang JR, Lin H, Hung W (2009) Interpolating functions from large Boolean relations. In: Roychowdhury JS (ed.) 2009 International conference on computer-aided design, ICCAD 2009, San Jose, CA, USA, November 2-5, 2009. pp. 779\u2013784. ACM . https:\/\/doi.org\/10.1145\/1687399.1687544","DOI":"10.1145\/1687399.1687544"},{"key":"421_CR28","doi-asserted-by":"publisher","first-page":"103229","DOI":"10.1016\/j.artint.2019.103229","volume":"281","author":"J Lagniez","year":"2020","unstructured":"Lagniez J, Lonca E, Marquis P (2020) Definability for model counting. Artif Intell 281:103229. https:\/\/doi.org\/10.1016\/j.artint.2019.103229","journal-title":"Artif Intell"},{"key":"421_CR29","doi-asserted-by":"publisher","unstructured":"Lynce I, Silva JPM (2003) Probing-based preprocessing techniques for propositional satisfiability. In: 15th IEEE International conference on tools with artificial intelligence (ICTAI 2003), 3-5 November 2003, Sacramento, California, USA. p.\u00a0105. IEEE computer society . https:\/\/doi.org\/10.1109\/TAI.2003.1250177","DOI":"10.1109\/TAI.2003.1250177"},{"key":"421_CR30","doi-asserted-by":"publisher","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Hunt Jr, WA, Somenzi F (eds.) Computer aided verification, 15th International conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. Lecture notes in computer science, vol.\u00a02725, pp. 1\u201313. Springer . https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"421_CR31","unstructured":"Minato S (1992) Fast generation of irredundant sum-of-products forms from binary decision diagrams. In: Proceedings of the synthesis and simulation meeting and international interchange (SASIMI\u201992). pp. 64\u201373"},{"key":"421_CR32","doi-asserted-by":"publisher","unstructured":"Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th design automation conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001. pp. 530\u2013535. ACM. https:\/\/doi.org\/10.1145\/378239.379017","DOI":"10.1145\/378239.379017"},{"key":"421_CR33","unstructured":"Nabeshima H, Iwanuma K, Inoue K (2015) GlueMiniSat 2.2.10 & 2.2.10-5 (2015), SAT-Race"},{"key":"421_CR34","first-page":"309","volume":"3","author":"A Padoa","year":"1901","unstructured":"Padoa A (1901) Essai d\u2019une th\u00e9orie alg\u00e9brique des nombres entiers, pr\u00e9c\u00e9d\u00e9 d\u2019une introduction logique \u00e0 une theorie d\u00e9ductive quelconque. Biblioth\u00e8que du Congr\u00e8s international de philosophie. 3:309\u2013365","journal-title":"Biblioth\u00e8que du Congr\u00e8s international de philosophie."},{"key":"421_CR35","doi-asserted-by":"publisher","unstructured":"Reichl F, Slivovsky F, Szeider S (2021) Certified DQBF solving by definition extraction. In: Li C, Many\u00e0 F (eds.) Theory and applications of satisfiability testing-SAT 2021-24th international conference, Barcelona, Spain, July 5-9, 2021, Proceedings. Lecture notes in computer science, vol. 12831, pp. 499\u2013517. Springer . https:\/\/doi.org\/10.1007\/978-3-030-80223-3_34","DOI":"10.1007\/978-3-030-80223-3_34"},{"key":"421_CR36","doi-asserted-by":"publisher","unstructured":"Silva JPM, Sakallah KA (1996) GRASP - a new search algorithm for satisfiability. In: Rutenbar RA, Otten RHJM (eds.) Proceedings of the 1996 IEEE\/ACM international conference on computer-aided design, ICCAD 1996, San Jose, CA, USA, November 10-14, 1996. pp. 220\u2013227. IEEE Computer Society \/ ACM. https:\/\/doi.org\/10.1109\/ICCAD.1996.569607","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"421_CR37","doi-asserted-by":"publisher","unstructured":"Slivovsky F (2020) Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In: Lahiri SK, Wang C (eds.) Computer aided verification - 32nd international conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. lecture notes in computer science, vol. 12224, pp. 508\u2013528. Springer.https:\/\/doi.org\/10.1007\/978-3-030-53288-8_24","DOI":"10.1007\/978-3-030-53288-8_24"},{"key":"421_CR38","doi-asserted-by":"publisher","unstructured":"Soos M, Meel KS (2019) BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In: The thirty-third AAAI conference on artificial intelligence, AAAI 2019, the thirty-first innovative applications of artificial intelligence conference, IAAI 2019, the ninth AAAI symposium on educational advances in artificial intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019. pp. 1592\u20131599. AAAI Press . https:\/\/doi.org\/10.1609\/aaai.v33i01.33011592","DOI":"10.1609\/aaai.v33i01.33011592"},{"key":"421_CR39","doi-asserted-by":"publisher","unstructured":"Soos M, Nohl K, Castelluccia C (2009) Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) Theory and applications of satisfiability testing-SAT 2009, 12th international conference, SAT 2009, Swansea, UK, June 30-July 3, 2009. Proceedings. Lecture notes in computer science, vol.\u00a05584, pp. 244\u2013257. Springer . https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"421_CR40","unstructured":"Subbarayan S, Pradhan DK (2004) NiVER: Non increasing variable elimination resolution for preprocessing SAT instances. In: SAT 2004 - The seventh international conference on theory and applications of satisfiability testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings , http:\/\/www.satisfiability.org\/SAT04\/programme\/118.pdf"},{"key":"421_CR41","doi-asserted-by":"publisher","unstructured":"Yang B, Simmons RG, Bryant RE, O\u2019Hallaron DR (1999) Optimizing symbolic model checking for constraint-rich models. In: Halbwachs N, Peled DA (eds.) Computer aided verification, 11th international conference, CAV \u201999, Trento, Italy, July 6-10, 1999, Proceedings. Lecture notes in computer science, vol.\u00a01633, pp. 328\u2013340. Springer. https:\/\/doi.org\/10.1007\/3-540-48683-6_29","DOI":"10.1007\/3-540-48683-6_29"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00421-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00421-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00421-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,10]],"date-time":"2023-10-10T10:31:23Z","timestamp":1696933883000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00421-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["421"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00421-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6]]},"assertion":[{"value":"6 May 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 March 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 April 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}