z3 - Z3 SMT求解器的名称是什么意思？

Question

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

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

Answer 1

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

1. 扎帕托
2. Zap2
3. Z3

由 Nikolaj Bjørner 在 Z3 and SMT in Industrial R&D 中解释:

Microsoft Research was also an incubator to the SLAM symbolic model checker, which had instigated the previous generations of SMT solvers at Microsoft: Zapatho solved integer difference logic and uninterpreted functions, Zap2 (dropping “atho”) extended the scope to full linear arithmetic, uninterpreted functions, arrays and quantifiers,and Leonardo de Moura and I created a v. 3 from scratch, Z3, dropping “ap”.

(原文:N Bjørner，“工业研发中的 Z3 和 SMT”，载于:K Havelund、J Peleska、B Roscoe、E de Vink:“形式化方法:第 22 届国际研讨会，FM 2018，作为联合逻辑的一部分举行 session ，FloC 2018，英国牛津，2018 年 7 月 15 日至 17 日， session 记录”，施普林格，第 676 页。)