在Dafny中实现DPLL算法
Verifying the DPLL Algorithm in Dafny
摘要：
现代高性能SAT求解器可以快速解决实践中出现的大型可满足性实例。如果实例是可满足的，那么SAT求解器可以提供一个见证，该见证可以以令人满意的真值赋值的形式独立地进行检查。但是，如果实例无法满足，则证书可能会呈指数级增长，或者SAT求解器可能无法输出证书。然后，SAT求解器的实现应该被信任不包含错误。然而，由典型的高性能SAT求解器实现的数据结构和算法足够复杂以允许细微的编程错误。为了解决这个问题，我们使用Dafny系统构建了一个经过验证的SAT求解器。我们在本文中讨论它的实现。
英文摘要：
Modern high-performance SAT solvers quickly solve large satisfiability instances that occur in practice. If the instance is satisfiable, then the SAT solver can provide a witness which can be checked independently in the form of a satisfying truth assignment. However, if the instance is unsatisfiable, the certificates could be exponentially large or the SAT solver might not be able to output certificates. The implementation of the SAT solver should then be trusted not to contain bugs. However, the data structures and algorithms implemented by a typical high-performance SAT solver are complex enough to allow for subtle programming errors. To counter this issue, we build a verified SAT solver using the Dafny system. We discuss its implementation in the present article.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
