Z3的参考文献--它是如何工作的[内部理论]？ [英] References for Z3 - how does it work[internal theory]?

问题描述

我对阅读Z3背后的内在理论很感兴趣。具体地说，我想阅读Z3 SMT求解器是如何工作的，以及它如何能够为不正确的模型找到反例。我希望能够手动计算出一些非常简单的例子的轨迹。

然而，所有的Z3参考似乎都是如何在其中编码；或者是对他们的算法的非常高级的描述。我找不到对所用算法的描述。此信息是否未由Microsoft公开？

有人能引用一些参考文献(论文/书籍)来全面了解Z3的理论和实践吗？

推荐答案

我个人的意见是，最好的参考资料是克罗宁和斯特里奇曼Decision Procedures的书。(一定要买第二版，因为它有很好的更新！)它几乎涵盖了所有感兴趣的主题，达到了一定的深度，并在后面有许多参考文献供您跟进。这本书还有一个网站http://www.decision-procedures.org，里面有额外的阅读资料、幻灯片和项目想法。

该领域的另一本有趣的书是Bradley和Manna的The Calculus of Computation。虽然这本书不是专门针对SAT/SMT的，但它涵盖了许多类似的主题，以及这些想法如何在程序验证领域发挥作用。另请参阅http://theory.stanford.edu/~arbrad/pivc/index.html以了解相关软件/工具。

当然，这两本书都不是特定于Z3的，所以您不会找到任何关于Z3本身是如何在其中构造的详细内容。对于Z3编程和它背后的一些理论，Bjórner、De Moura、Nachmanson和Wintersteiger的"tutorial" paper是一本很好的读物。

一旦你看过这些，我建议你根据你的兴趣阅读开发人员的个别论文：

• 比约尔纳：https://www.microsoft.com/en-us/research/people/nbjorner/publications/

• de Moura：https://www.microsoft.com/en-us/research/people/leonardo/publications/

• Wintersteiger：https://www.microsoft.com/en-us/research/people/cwinter/publications/

• Nachmanson：https://www.microsoft.com/en-us/research/people/levnach/publications/

当然，互联网上有太多的资源，有很多论文、演示文稿、幻灯片等。您可以直接在这个论坛中提出具体问题，或者对于真正的Z3内部具体问题，可以使用他们的discussions forum。

注意：关于克罗宁和斯特里奇曼的书版本之间的差异，以下是两位作者必须说的话：

这本书的第一版被世界各地的课程采用为教科书。它是在2008年出版的，现在被称为SMT的领域当时还处于初级阶段，没有现在的标准术语和规范算法；第二版反映了这些变化。提出了DPLL(T)框架。它还用现代SAT启发式算法扩展了SAT一章，并包括关于增量可满足性和相关约束满足问题(CSP)的新部分。关于量词的章节增加了一个新的关于使用E-匹配进行一般量化的章节和一个关于有效命题推理(EPR)的章节。该书还包括关于SMT在工业软件工程和计算生物学中的应用的新章节，分别由Nikolaj Bjórner和Leonardo de Moura以及Hillel Kugler合著。

这篇关于Z3的参考文献--它是如何工作的[内部理论]？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！