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

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

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

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

我个人的观点是，最好的参考文献是 Kroening 和 Strichman 的决策程序 https://rads.stackoverflow.com/amzn/click/com/3662570653书。 （确保获得第二版，因为它有很好的更新！）它涵盖了几乎所有感兴趣的主题，并且有一定深度，并且后面有许多参考资料供您跟进。这本书还有一个网站http://www.decision-procedures.org http://www.decision-procedures.org包括额外的阅读材料、幻灯片和项目想法。

该领域的另一本有趣的书是 Bradley 和 Manna 的计算微积分 https://rads.stackoverflow.com/amzn/click/com/3642093477。虽然本书并非专门针对 SAT/SMT，但它涵盖了许多类似的主题以及这些想法如何在程序验证领域发挥作用。另请参阅http://theory.stanford.edu/~arbrad/pivc/index.html http://theory.stanford.edu/%7Earbrad/pivc/index.html相关软件/工具。

当然，这两本书都不是专门针对 z3 的，因此您在其中找不到有关 z3 本身如何构建的任何详细信息。对于 z3 编程及其背后的一些理论，“教程”论文 https://theory.stanford.edu/%7Enikolaj/programmingz3.htmlBjørner、de Moura、Nachmanson 和 Wintersteiger 的著作非常值得一读。

一旦您阅读完这些内容，我建议您根据您的兴趣阅读开发人员的个别论文：

• 比约纳：https://www.microsoft.com/en-us/research/people/nbjorner/publications/ 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/leonardo/publications/

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

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

当然，互联网上有大量资源、许多论文、演示文稿、幻灯片等。您可以直接在这个论坛中直接提出具体问题，或者对于真正的 z3 内部具体问题，您可以使用他们的讨论论坛 https://github.com/Z3Prover/z3/discussions.

Note关于克罗宁和斯特里奇曼的书版本之间的差异，作者们是这么说的：

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