Z3 的参考资料 - 它是如何工作的[内部理论]？

Question

我有兴趣阅读 Z3 背后的内部理论。具体来说，我想阅读 Z3 SMT 求解器的工作原理，以及它如何为不正确的模型找到反例。我希望能够为一些非常简单的示例手动计算出跟踪。

不过，Z3 的所有引用似乎都是如何在其中编码的；或对其算法的非常高级的描述。我找不到所用算法的描述。微软没有公开这些信息吗？

谁能引用任何可以全面了解 Z3 的理论 + 工作的参考资料（论文/书籍）？

Answer 1

我个人认为，最好的参考是 Kroening 和 Strichman 的 Decision Procedures 书。 （确保获得第 2 版，因为它有很好的更新！）它几乎涵盖了一定深度感兴趣的所有主题，并且在后面有许多参考资料供您跟进。这本书还有一个网站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/

• 德莫拉：https://www.microsoft.com/en-us/research/people/leonardo/publications/

• 温特斯泰格：https://www.microsoft.com/en-us/research/people/cwinter/publications/

• 纳赫曼森：https://www.microsoft.com/en-us/research/people/levnach/publications/

当然，互联网上有大量资源、许多论文、演示文稿、幻灯片等。请随时直接在此论坛中提出具体问题，或者对于真正的 z3 内部具体问题，您可以使用他们的@987654330 @。

注意关于 Kroening 和 Strichman 的书的版本之间的差异，作者是这样说的：

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