Yuan's blog

刘沛源的博客

0%

SAT solver与SMT solver

发表于 更新于 Disqus：
本文字数： 749 阅读时长 ≈ 1 分钟

SAT solver

SAT

布尔可满足性问题（Boolean satisfiability problem），指是否存在一组解可以使一个布尔公式结果为True，此问题是NPC问题。现有算法可以有效解决涉及数万个变量和数百万子句的问题的能力。

算法

  1. 完备算法：DPLL, CDCL, LA
  2. 不完备算法：SLS, MP, EA
  3. 混合求解
  4. 并行求解

    SAT Solver

    是可用布尔公式（合取范式）描述的的一类问题的求解器。

    求解方法

    将问题转换为合取范式，代入求解器即可。

    应用方向

  5. 电路可满足问题：验证是否存在一组input，使得output为true
  6. 电路形式等效检查：验证两个电路等效

    示例

    比如若要求解使析取范式 $(\neg A \vee B) \wedge (C \vee D)$ 为 True的所有结果
    1
    2
    3
    4
    5
    6
    import pycosat

    # 用数字标识一个变量
    # (not a or b) and (c or d)
    for solution in list(pycosat.itersolve([(-1, 2), (3, 4)])):
      print(solution)
    输出如下
    1
    2
    3
    4
    5
    6
    7
    8
    9
    [-1, 2, 3, 4]
    [-1, 2, 3, -4]
    [-1, 2, -3, 4]
    [-1, -2, -3, 4]
    [-1, -2, 3, 4]
    [-1, -2, 3, -4]
    [1, 2, 3, 4]
    [1, 2, 3, -4]
    [1, 2, -3, 4]

SMT solver

SMT solver

是SAT的扩展，使用一阶逻辑描述问题, 变量类型不再限于布尔变量，还可以是常量、函数、谓词等

应用方向

  1. 软件包依赖检查
  2. 数独问题
  3. 八皇后
  4. 算术表达式满足性检查

    应用方向示例

    可以进行变量约束问题求解
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    20
    21
    22
    23
    24
    from z3 import Int, Solver
    x = Int('x')
    y = Int('y')

    s = Solver()
    print(s)

    s.add(x > 10, y == x + 2)
    print(s)
    print("Solving constraints in the solver s ...")
    print(s.check())

    print("Create a new scope...")
    s.push()
    s.add(y < 11)
    print(s)
    print("Solving updated set of constraints...")
    print(s.check())

    print("Restoring state...")
    s.pop()
    print(s)
    print("Solving restored set of constraints...")
    print(s.check())
    结果如下
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    []
    [x > 10, y == x + 2]
    Solving constraints in the solver s ...
    sat
    Create a new scope...
    [x > 10, y == x + 2, y < 11]
    Solving updated set of constraints...
    unsat
    Restoring state...
    [x > 10, y == x + 2]
    Solving restored set of constraints...
    sat

    参考资料

    [1] https://rhettinger.github.io/overview.html
    [2] https://resources.mpi-inf.mpg.de/departments/rg1/conferences/vtsa08/slides/barret2_smt.pdf
    [3] http://www.jsjkx.com/CN/article/openArticlePDF.jsp?id=16156
    [4] https://pysathq.github.io/docs/pysat.pdf
    [5] https://ericpony.github.io/z3py-tutorial/guide-examples.htm