UNSAT证明中的确定性
Determinism in the Certification of UNSAT Proofs
摘要：
对SAT求解器增加可信度的研究非常活跃，并使用各种方法。这些方法中的一些从证明者那里获得证明，然后检查它，通常是根据证明的信息复制搜索。因为认证过程涉及另一个重要的证明搜索，我们可以对它的信任降低了。一些试图修改这一使用证明人已验证了证明助理，如伊莎贝尔/HOL和Coq。我们的方法是不同的，因为它是基于一个非常简单的证明。该认证机构享有非常高的信任度，但效率非常低。在本文中，我们用这种方法进行了实验，并得出结论，通过对格式进行一些限制，可以基本上消除搜索的需要，并且原则上可以证明任意大小的证明。
英文摘要：
The search for increased trustworthiness of SAT solvers is very active and uses various methods. Some of these methods obtain a proof from the provers then check it, normally by replicating the search based on the proof's information. Because the certification process involves another nontrivial proof search, the trust we can place in it is decreased. Some attempts to amend this use certifiers which have been verified by proofs assistants such as Isabelle/HOL and Coq. Our approach is different because it is based on an extremely simplified certifier. This certifier enjoys a very high level of trust but is very inefficient. In this paper, we experiment with this approach and conclude that by placing some restrictions on the formats, one can mostly eliminate the need for search and in principle, can certify proofs of arbitrary size.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
