Seulkee Baek ; Mario Carneiro ; Marijn J. H. Heule - A Flexible Proof Format for SAT Solver-Elaborator Communication

lmcs:8509 - Logical Methods in Computer Science, April 18, 2022, Volume 18, Issue 2 - https://doi.org/10.46298/lmcs-18(2:3)2022
A Flexible Proof Format for SAT Solver-Elaborator CommunicationArticle

Authors: Seulkee Baek ; Mario Carneiro ; Marijn J. H. Heule

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.


Volume: Volume 18, Issue 2
Secondary volumes: Selected Papers of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021)
Published on: April 18, 2022
Accepted on: January 15, 2022
Submitted on: September 21, 2021
Keywords: Computer Science - Logic in Computer Science
Funding:
    Source : OpenAIRE Graph
  • SHF: Small: Mechanical Verification of QBF Results; Funder: National Science Foundation; Code: 2010951

8 Documents citing this article

Consultation statistics

This page has been seen 2819 times.
This article's PDF has been downloaded 2126 times.