Z3

释义 Definition

Z3 通常指 Z3 定理证明器/SMT 求解器：由微软研究院开发的自动推理工具，用来判断逻辑公式在给定理论（如整数、数组、位向量等）下是否可满足，并可用于程序验证、约束求解与自动化推理。
（另有较少见含义：Z3 也可指康拉德·楚泽（Konrad Zuse）在 1941 年完成的早期计算机 Z3。）

发音 Pronunciation

/ziː θriː/

例句 Examples

I used Z3 to solve a set of constraints.
我用 Z3 解了一组约束条件。

By encoding the program’s rules as logic formulas, we can ask Z3 to find a counterexample automatically.
把程序规则编码成逻辑公式后，我们可以让 Z3 自动寻找反例。

词源 Etymology

“Z3” 属于名称/代号而非传统词汇：在计算领域常读作 “Z three”。作为工具名时，它与自动推理与约束求解相关；作为历史计算机名时，源自楚泽对其机器系列（Z1、Z2、Z3）的编号命名。

相关词 Related Words

• Solver
• SMT
• SAT
• Constraint
• Theorem
• Proof
• Verification
• Model
• Satisfiable
• Symbolic

文学与作品 Literary Works

• The Z3 Theorem Prover（TACAS 2008 论文，介绍 Z3 的设计与能力）
• Programming Z3（面向开发者的实践书/文档，讲解如何用 API 调用 Z3）
• Handbook of Satisfiability（综述类著作中涉及 SAT/SMT 及相关工具，常提及 Z3）
• Decision Procedures: An Algorithmic Point of View（决策过程经典教材；讨论 SMT/求解器生态时常引用 Z3 等工具）