{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:33:45Z","timestamp":1725471225906},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Contemporary SAT solvers are complex tools and may contain bugs.  In<\/jats:p><jats:p>order to increase the trust in the results of SAT solving, SAT solvers<\/jats:p><jats:p>may produce certificates that can be checked independently.  For<\/jats:p><jats:p>unsatisfiability certificates, DRAT is the de facto standard.  As long<\/jats:p><jats:p>as the checkers are not formalized, extending the certificate format<\/jats:p><jats:p>would decrease the trust in the checker because its code complexity<\/jats:p><jats:p>increases.  With the advent of formally verified checkers for DRAT<\/jats:p><jats:p>proofs, this is no longer the case.  In this note I argue that<\/jats:p><jats:p>symmetry breaking is not adequately supported by DRAT proofs, and<\/jats:p><jats:p>propose to have dedicated certification for symmetry breaking instead.<\/jats:p>","DOI":"10.29007\/2b78","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T23:06:06Z","timestamp":1516748766000},"page":"46-40","source":"Crossref","is-referenced-by-count":0,"title":["Beyond DRAT: Challenges in Certifying UNSAT"],"prefix":"10.29007","volume":"51","author":[{"given":"Bertram","family":"Felgenhauer","sequence":"first","affiliation":[]}],"member":"11545","event":{"name":"ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T23:06:10Z","timestamp":1516748770000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/TFMG"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/2b78","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}