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
    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

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1965 times.
    This article's PDF has been downloaded 1433 times.