{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:06:49Z","timestamp":1750309609843,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["10.55776\/COE12"],"award-info":[{"award-number":["10.55776\/COE12"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"name":"State of Upper Austria (LIT AI Lab)"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,31]]},"DOI":"10.1145\/3672608.3707863","type":"proceedings-article","created":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:26:21Z","timestamp":1747247181000},"page":"1043-1050","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["FERAT: A New Expansion-Based Certification Framework for Quantified Boolean Formulas"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-5751-7820","authenticated-orcid":false,"given":"Marcel","family":"Simader","sequence":"first","affiliation":[{"name":"Johannes Kepler Universit\u00e4t, Linz, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9234-4377","authenticated-orcid":false,"given":"Adrian","family":"Rebola-Pardo","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Vienna, Austria"},{"name":"Johannes Kepler Universit\u00e4t, Linz, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-4494","authenticated-orcid":false,"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[{"name":"Johannes Kepler Universit\u00e4t, Linz, Austria"}]}],"member":"320","published-online":{"date-parts":[[2025,5,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Johannes Altmanninger and Adrian Rebola-Pardo. 2020. Frying the egg roasting the chicken: unit deletions in DRAT proofs. In CPP. ACM 61\u201370.","DOI":"10.1145\/3372885.3373821"},{"volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","author":"Beyersdorff Olaf","key":"e_1_3_2_1_2_1","unstructured":"Olaf Beyersdorff, Mikol\u00e1s Janota, Florian Lonsing, and Martina Seidl. 2021. Quantified Boolean Formulas. In Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, Vol. 336. IOS Press, 1177\u20131221."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_5"},{"volume-title":"CAV (1) (Lecture Notes in Computer Science","author":"Biere Armin","key":"e_1_3_2_1_4_1","unstructured":"Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. 2024. CaDiCaL 2.0. In CAV (1) (Lecture Notes in Computer Science, Vol. 14681). Springer, 133\u2013152."},{"key":"e_1_3_2_1_5_1","volume-title":"Heule","author":"Biere Armin","year":"2023","unstructured":"Armin Biere, Mathias Fleury, Nils Froleyks, and Marijn J. H. Heule. 2023. The SAT Museum. In POS@SAT (CEUR Workshop Proceedings, Vol. 3545). CEUR-WS.org, 72\u201387."},{"key":"e_1_3_2_1_6_1","volume-title":"Frontiers in Artificial Intelligence and Applications","volume":"336","author":"Biere Armin","year":"2021","unstructured":"Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). 2021. Handbook of Satisfiability - Second Edition. Frontiers in Artificial Intelligence and Applications, Vol. 336. IOS Press."},{"volume-title":"Expansion-Based QBF Solving Without Recursion","author":"Bloem Roderick","key":"e_1_3_2_1_7_1","unstructured":"Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, and Martina Seidl. 2018. Expansion-Based QBF Solving Without Recursion. In FMCAD. IEEE, 1\u201310."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_5"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"e_1_3_2_1_11_1","volume-title":"LPAR (EPiC Series in Computing","volume":"229","author":"Fleury Mathias","year":"2020","unstructured":"Mathias Fleury and Christoph Weidenbach. 2020. A Verified SAT Solver Framework including Optimization and Partial Valuations. In LPAR (EPiC Series in Computing, Vol. 73). EasyChair, 212\u2013229."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-012-9322-x"},{"key":"e_1_3_2_1_13_1","volume-title":"Goldberg and Yakov Novikov","author":"Evguenii","year":"2003","unstructured":"Evguenii I. Goldberg and Yakov Novikov. 2003. Verification of Proofs of Unsatisfiability for CNF Formulas. In DATE. IEEE Computer Society, 10886\u201310891."},{"volume-title":"FERPModels: A Certification Framework for Expansion-Based QBF Solving","author":"Hadzic Vedad","key":"e_1_3_2_1_14_1","unstructured":"Vedad Hadzic, Roderick Bloem, Ankit Shukla, and Martina Seidl. 2022. FERPModels: A Certification Framework for Expansion-Based QBF Solving. In SYNASC. IEEE, 80\u201383."},{"volume-title":"Trimming while checking clausal proofs","author":"Heule Marijn","key":"e_1_3_2_1_15_1","unstructured":"Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. 2013. Trimming while checking clausal proofs. In FMCAD. IEEE, 181\u2013188."},{"volume-title":"ARCADE@CADE (EPiC Series in Computing","author":"Heule Marijn","key":"e_1_3_2_1_16_1","unstructured":"Marijn Heule and Benjamin Kiesl. 2017. The Potential of Interference-Based Proof Systems. In ARCADE@CADE (EPiC Series in Computing, Vol. 51). EasyChair, 51\u201354."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.01.004"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ARTINT.2016.01.004"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.048"},{"key":"e_1_3_2_1_20_1","volume-title":"Heule","author":"Kiesl Benjamin","year":"2018","unstructured":"Benjamin Kiesl, Adri\u00e1n Rebola-Pardo, and Marijn J. H. Heule. 2018. Extended Resolution Simulates DRAT. In IJCAR (Lecture Notes in Computer Science, Vol. 10900). Springer, 516\u2013531."},{"key":"e_1_3_2_1_21_1","volume-title":"LPAR (EPiC Series in Computing","volume":"603","author":"Rebola-Pardo Adri\u00e1n","year":"2018","unstructured":"Adri\u00e1n Rebola-Pardo and Martin Suda. 2018. A Theory of Satisfiability-Preserving Proofs in SAT Solving. In LPAR (EPiC Series in Computing, Vol. 57). EasyChair, 583\u2013603."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"volume-title":"Using Rust and Creusot to create the world's fastest deductively verified SAT solver. Master's thesis","author":"Skot\u00e5m Sarek H\u00f8verstad","key":"e_1_3_2_1_24_1","unstructured":"Sarek H\u00f8verstad Skot\u00e5m. 2022. CreuSAT, Using Rust and Creusot to create the world's fastest deductively verified SAT solver. Master's thesis. University of Oslo. https:\/\/www.duo.uio.no\/handle\/10852\/96757"},{"key":"e_1_3_2_1_25_1","volume-title":"Hunt Jr","author":"Wetzler Nathan","year":"2014","unstructured":"Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr. 2014. DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. In SAT (Lecture Notes in Computer Science, Vol. 8561). Springer, 422\u2013429."}],"event":{"name":"SAC '25: 40th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Catania International Airport Catania Italy","acronym":"SAC '25"},"container-title":["Proceedings of the 40th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672608.3707863","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3672608.3707863","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:33Z","timestamp":1750298253000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672608.3707863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":25,"alternative-id":["10.1145\/3672608.3707863","10.1145\/3672608"],"URL":"https:\/\/doi.org\/10.1145\/3672608.3707863","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]},"assertion":[{"value":"2025-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}