A Flexible Proof Format for SAT Solver-Elaborator Communication

We introduce FRAT, a new proof format for unsatisfiable SAT problems, and its associated toolchain. Compared to DRAT, the FRAT format allows solvers to include more information in proofs to reduce the computational cost of subsequent elaboration to LRAT. The format is easy to parse forward and backw...

Descripción completa

Detalles Bibliográficos
Autores principales: Baek, Seulkee, Carneiro, Mario, Heule, Marijn J. H.
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2021
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979213/
http://dx.doi.org/10.1007/978-3-030-72016-2_4
_version_ 1783667242276225024
author Baek, Seulkee
Carneiro, Mario
Heule, Marijn J. H.
author_facet Baek, Seulkee
Carneiro, Mario
Heule, Marijn J. H.
author_sort Baek, Seulkee
collection PubMed
description We introduce FRAT, a new proof format for unsatisfiable SAT problems, and its associated toolchain. Compared to DRAT, the FRAT format allows solvers to include more information in proofs to reduce the computational cost of subsequent elaboration to LRAT. The format is easy to parse forward and backward, and it is extensible to future proof methods. The provision of optional proof steps allows SAT solver developers to balance implementation effort against elaboration time, with little to no overhead on solver time. We benchmark our FRAT toolchain against a comparable DRAT toolchain and confirm >84% median reduction in elaboration time and >94% median decrease in peak memory usage.
format Online
Article
Text
id pubmed-7979213
institution National Center for Biotechnology Information
language English
publishDate 2021
record_format MEDLINE/PubMed
spelling pubmed-79792132021-03-23 A Flexible Proof Format for SAT Solver-Elaborator Communication Baek, Seulkee Carneiro, Mario Heule, Marijn J. H. Tools and Algorithms for the Construction and Analysis of Systems Article We introduce FRAT, a new proof format for unsatisfiable SAT problems, and its associated toolchain. Compared to DRAT, the FRAT format allows solvers to include more information in proofs to reduce the computational cost of subsequent elaboration to LRAT. The format is easy to parse forward and backward, and it is extensible to future proof methods. The provision of optional proof steps allows SAT solver developers to balance implementation effort against elaboration time, with little to no overhead on solver time. We benchmark our FRAT toolchain against a comparable DRAT toolchain and confirm >84% median reduction in elaboration time and >94% median decrease in peak memory usage. 2021-03-01 /pmc/articles/PMC7979213/ http://dx.doi.org/10.1007/978-3-030-72016-2_4 Text en © The Author(s) 2021 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Baek, Seulkee
Carneiro, Mario
Heule, Marijn J. H.
A Flexible Proof Format for SAT Solver-Elaborator Communication
title A Flexible Proof Format for SAT Solver-Elaborator Communication
title_full A Flexible Proof Format for SAT Solver-Elaborator Communication
title_fullStr A Flexible Proof Format for SAT Solver-Elaborator Communication
title_full_unstemmed A Flexible Proof Format for SAT Solver-Elaborator Communication
title_short A Flexible Proof Format for SAT Solver-Elaborator Communication
title_sort flexible proof format for sat solver-elaborator communication
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979213/
http://dx.doi.org/10.1007/978-3-030-72016-2_4
work_keys_str_mv AT baekseulkee aflexibleproofformatforsatsolverelaboratorcommunication
AT carneiromario aflexibleproofformatforsatsolverelaboratorcommunication
AT heulemarijnjh aflexibleproofformatforsatsolverelaboratorcommunication
AT baekseulkee flexibleproofformatforsatsolverelaboratorcommunication
AT carneiromario flexibleproofformatforsatsolverelaboratorcommunication
AT heulemarijnjh flexibleproofformatforsatsolverelaboratorcommunication

Ejemplares similares