{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:08Z","timestamp":1753894388139,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,4,18]],"date-time":"2022-04-18T00:00:00Z","timestamp":1650240000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We introduce FRAT, a new proof format for unsatisfiable SAT problems, and its\nassociated toolchain. Compared to DRAT, the FRAT format allows solvers to\ninclude more information in proofs to reduce the computational cost of\nsubsequent elaboration to LRAT. The format is easy to parse forward and\nbackward, and it is extensible to future proof methods. The provision of\noptional proof steps allows SAT solver developers to balance implementation\neffort against elaboration time, with little to no overhead on solver time. We\nbenchmark our FRAT toolchain against a comparable DRAT toolchain and confirm\n&gt;84% median reduction in elaboration time and &gt;94% median decrease in peak\nmemory usage.<\/jats:p>","DOI":"10.46298\/lmcs-18(2:3)2022","type":"journal-article","created":{"date-parts":[[2022,4,20]],"date-time":"2022-04-20T14:13:33Z","timestamp":1650464013000},"source":"Crossref","is-referenced-by-count":2,"title":["A Flexible Proof Format for SAT Solver-Elaborator Communication"],"prefix":"10.46298","volume":"Volume 18, Issue 2","author":[{"given":"Seulkee","family":"Baek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Carneiro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2022,4,18]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/9357\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/9357\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:20:22Z","timestamp":1687292422000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/8509"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,18]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(2:3)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2109.09665v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2109.09665","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2109.09665","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2022,4,18]]},"article-number":"8509"}}