我对阅读Z3背后的内在理论很感兴趣。具体地说,我想阅读Z3 SMT求解器是如何工作的,以及它如何能够为不正确的模型找到反例。我希望能够手动计算出一些非常简单的例子的轨迹。
然而,所有的Z3参考似乎都是如何在其中编码;或者是对他们的算法的非常高级的描述。我找不到对所用算法的描述。此信息是否未由Microsoft公开?
有人能引用一些参考文献(论文/书籍)来全面了解Z3的理论和实践吗?
推荐答案我个人的意见是,最好的参考资料是克罗宁和斯特里奇曼Decision Procedures的书。(一定要买第二版,因为它有很好的更新!)它几乎涵盖了所有感兴趣的主题,达到了一定的深度,并在后面有许多参考文献供您跟进。这本书还有一个网站www.decision-procedures,里面有额外的阅读资料、幻灯片和项目想法。
该领域的另一本有趣的书是Bradley和Manna的The Calculus of Computation。虽然这本书不是专门针对SAT/SMT的,但它涵盖了许多类似的主题,以及这些想法如何在程序验证领域发挥作用。另请参阅theory.stanford.edu/~arbrad/pivc/index.html以了解相关软件/工具。
当然,这两本书都不是特定于Z3的,所以您不会找到任何关于Z3本身是如何在其中构造的详细内容。对于Z3编程和它背后的一些理论,Bjórner、De Moura、Nachmanson和Wintersteiger的"tutorial" paper是一本很好的读物。一旦你看过这些,我建议你根据你的兴趣阅读开发人员的个别论文:
比约尔纳:www.microsoft/en-us/research/people/nbjorner/publications/
de Moura:www.microsoft/en-us/research/people/leonardo/publications/
Wintersteiger:www.microsoft/en-us/research/people/cwinter/publications/
Nachmanson:www.microsoft/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的参考文献
发布评论