/z3-study

z3 solver 学习

Primary LanguagePython

z3-study

z3学习（推荐使用Python进行学习。）

z3是由微软公司开发的一个优秀的SMT求解器（其实就是一个定理证明器），它能够检查逻辑表达式的可满足性。

from z3 import *

if __name__ == '__main__':
    solver = Solver()  # 第1步：创建求解器
    x = Int('x')
    y = Int('y')
    solver.add(x > 2)
    solver.add(y < 10)
    solver.add(x + 2 * y == 7)  # 第2步：添加约束
    if solver.check() == sat:  # 第3步：判断解是否存在
        print(solver.model())  # 第4步：输出结果
    else:
        print("no sat")

学习资源

其它求解器

相关关键概念/Keyword

  • SAT（Satisfiability）：指命题逻辑公式的可满足性问题。

  • SMT（Satisfiability Modulo Theories）：被翻译为“可满足性模理论”、“多理论下的可满足性问题”或者“特定（背景）理论下的可满足性问题”，其判定算法被称为SMT求解器。

    SMT算法分为2种：积极（eager）类算法/惰性（lazy）类算法（主流）。

  • CNF（conjunctive normal form）：命题公式的合取范式形式。也就是形如A1^A2^...^An的公式，其中每一个Ai是一个子句。

  • UF（uninterpreted function）：未解释函数。

  • LRA（linear real arithmetic）：线性实数演算。

  • LIA（linear integer arithmetic）：线性整数演算。

  • NRA（non-linear real arithmetic）：非线性实数演算。

  • NIA（non-linear integer arithmetic）：非线性整数演算。

  • RDL（difference logic over the reals）：实数差分逻辑。

  • IDL（difference logic over the integers）：整数差分逻辑。

  • arrays：数组。

  • BV（bit vector）：位向量。

  • DPLL算法 （Davis-Putnam-Logemann-Loveland algorithm）。

  • CDCL算法（conflict-driven clause learning SAT solver)：基于冲突检测的子句学习求解算法。

  • DAG（directed acyclic graph）：有向无环图。

教程-视频

教程/文章/安装参考

经典应用

Paper