高效认证的RAT验证
计算机科学中的逻辑
2017-08-09 v2
摘要
子句证明已成为验证SAT求解器结果的流行方法。然而，即使在高度优化的实现中，验证最广泛支持格式（DRAT）的子句证明也是昂贵的。我们提出一种新格式，称为LRAT，它通过附加提示扩展了DRAT格式，从而便于实现简单快速的验证算法。检查LRAT证明的有效性可以使用可信系统（如定理证明器支持的语言）来实现。我们通过实现两个认证的LRAT检查器（一个在Coq中，一个在ACL2中）来证明这一点。
引用
@article{arxiv.1612.02353,
title = {Efficient Certified RAT Verification},
author = {Luís Cruz-Filipe and Marijn Heule and Warren Hunt and Matt Kaufmann and Peter Schneider-Kamp},
journal= {arXiv preprint arXiv:1612.02353},
year = {2017}
}