Z3 SMT求解器名称的含义是什么？

Question

Microsoft Research 的 Z3 SMT 求解器被广泛视为该领域的领导者。

“Z3”这个名字背后有什么含义还是纯粹是一个随机的项目名称？我浏览了几篇介绍该项目的论文和幻灯片，但似乎都没有解释这个名称。

Answer 1

名称为Z3 SMT 求解器的“Z3” （SMT = Satisfiability modulo theories）是基于以前称为 Zapatho 的 Microsoft 求解器。基本上，更高版本的功能更多，但名称更短。它来自

1. 扎帕托
2. Zap2
3. Z3

Nikolaj Bjørner 在Z3 和 SMT 在工业研发中的解释：

微软研究院也是 SLAM 符号模型检查器的孵化器，它在微软鼓动了前几代 SMT 求解器：Zapatho 解决了整数差分逻辑和未解释的函数，Zap2（去掉“atho”）将范围扩展到完整的线性算术，未解释函数、数组和量词，以及 Leonardo de Moura 和我从头开始创建了一个 v.3，Z3，去掉了“ap”。

（原文：N Bjørner，“工业研发中的 Z3 和 SMT”，见：K Havelund、J Peleska、B Roscoe、E de Vink：“形式方法：第 22 届国际研讨会，FM 2018，作为联邦逻辑会议的一部分举行，FloC 2018 年，英国牛津，2018 年 7 月 15 日至 17 日，会议录”，Springer，第 676 页。）