From DRUP to PAC and Back
From DRUP to PAC and Back
复制标题
从 DRUP 到 PAC 并返回
DOI：
10.23919/date48585.2020.9116276
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Manuel Kauers
中科院分区：
文献类型：
--
作者：
Daniela Kaufmann;Armin Biere;Manuel Kauers
目前，最有效的自动方法来验证门级乘法器结合SAT解决和计算机代数。为了提高核查的可信度，生成了证明证书。然而，由于解决技术的不同，这些证书需要两种不同的证明格式，即DRUP和PAC。到目前为止，一个综合的证据还没有出现。因此，这种方法的正确性只能信任组合推理的正确性。在本文中，我们将展示如何在一个证明格式中生成一个证明，然后使用一个简单的证明检查器来证明正确性。我们进一步实证研究证明生成和检查时间以及证明大小的影响。事实证明，PAC证明更紧凑，检查速度更快。
Currently the most efficient automatic approach to verify gate-level multipliers combines SAT solving and computer algebra. In order to increase confidence in the verification, proof certificates are generated. However, due to different solving techniques, these certificates require two different proof formats, namely DRUP and PAC. A combined proof has so far been missing. Correctness of this approach can thus only be trusted up to the correctness of compositional reasoning. In this paper we show how to generate a single proof in one proof format, which then allows to certify correctness using one simple proof checker. We further investigate empirically the effect on proof generation and checking time as well as on proof size. It turns out that PAC proofs are much more compact and faster to check.