一句话：提出 FRAT 证明格式与工具链，显著降低 UNSAT SAT 证明精化为 LRAT 的时间与内存开销。
针对不可满足 SAT 问题，求解器通常输出 DRAT 证明，再精化为 LRAT 以供独立检查，但这一精化过程计算开销大。本文提出 FRAT：一种灵活的证明格式及配套工具链。与 DRAT 相比，FRAT 允许求解器在证明中包含更多信息，并支持可选证明步骤，使开发者能在实现成本与精化时间之间权衡；该格式易向前/向后解析，且可扩展到未来证明方法。作者将 FRAT 工具链与同类 DRAT 工具链进行基准测试，结果显示精化时间中位数降低超过 84%，峰值内存使用中位数下降超过 94%，而求解器时间几乎没有额外开销。
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.
@article{paperbot1708,
title = {A Flexible Proof Format for SAT Solver-Elaborator Communication},
author = {Seulkee Baek and Mario Carneiro and Marijn J. H. Heule},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:3)2022}
}