谁来验证验证者？Dafny语言中DPLL算法的计算机实现
Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny
摘要：
我们建立了一个SAT求解器实现DPLL算法的验证启用程序设计语言Dafny。所得到的解算器是完全验证（健全性，完整性和终止性是计算机检查）。我们基准我们的Dafny求解器，我们表明，它是一样有效的等效的DPLL求解器在C#中实现，大约两倍的效率比等效的求解器写在C++。我们的结论是，自动主动验证是一种很有前途的方法，以增加在SAT求解器的信任，因为它结合了执行速度和最终产品的可信度之间的良好权衡。
英文摘要：
We build a SAT solver implementing the DPLL algorithm in the verification-enabled programming language Dafny. The resulting solver is fully verified (soundness, completeness and termination are computer checked). We benchmark our Dafny solver and we show that it is just as efficient as an equivalent DPLL solver implemented in C# and roughly two times less efficient than an equivalent solver written in C++. We conclude that auto-active verification is a promising approach to increasing trust in SAT solvers, as it combines a good trade-off between execution speed and degree of trustworthiness of the final product.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
