Z3 SMT解算器的名称是什么意思？

Question

微软研究公司( Microsoft )的Z3 SMT解决方案被广泛视为其领域的领导者。

"Z3“这个名字背后有什么含义吗?还是它纯粹是一个随机的项目名称？我看过几篇介绍这个项目的论文和幻灯片，但似乎没有一个能解释这个项目的名称。

Answer 1

名为Z3 (SMT = 可满足模理论)的“Z3 SMT解算器”是基于以前的微软解决程序Zapatho。基本上，更高版本的功能更多，但名称更短。它从

1. 萨帕索
2. Zap2
3. Z3

由Nikolaj Bj rner在Z3与SMT在工业研发中的应用中解释

微软研究公司也是SLAM符号模型检查器的孵化器。SLAM符号模型检查器是微软前几代SMT求解器的前身: Zapatho解决整数差分逻辑和未解释函数，Zap2 (删除“at”)将范围扩展到全线性算术、未解释函数、数组和量词，Leonardo de Moura和我从零开始创建了V3，Z3，删除ap。

(原名:n Bj rner，"Z3和SMT in Industrial R&D“，载于:K Havelund，J Peleska，B Roscoe，E de Vink：”正式方法:第22次国际研讨会，FM 2018，作为联邦逻辑会议的一部分，FloC 2018年，英国牛津，2018年7月15-17日，议事录“，斯普林格，第676页)。