等式问题与 z3 的使用

基本数据类型

在Python中使用 Z3 模块，我们的所求结果一般有以下几种数据类型：

  • Int

  • Real

  • Bool

  • Array

  • BitVec(‘a’, 8)

其中 BitVec 可以是特定大小的数据类型，不一定是 8 位，例如 C 语言中的 int 型可以用 BitVec(‘a’, 32)

表示。

基本语句

在 Python 中使用该模块，我们通常用到如下几个 API：

  • **Solver()**：创建一个通用求解器，以进行下一步的求解

  • **add()**：添加约束条件，通常在solver()命令之后，添加的约束条件通常是一个逻辑等式

  • **check()**：添加完约束条件后，用来来检测解的情况，有解的时候会返回 sat，无解的时候会返回unsat

  • **model()**：在存在解的时候，该函数会将每个限制条件所对应的解集的交集，进而得出正解

分别对应设未知数，列方程组，判断方程是否有解，解方程组。

简单使用

image-20240302165337491

入门实践

1
2
3
4
5
6
7
8
9
10
11
12
13
14
from z3 import *
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
s = Solver()
s.add(b == a - 2)
s.add(d == c + 2)
s.add(d == a + 5)
s.add(b - 20 + c - 20 == 15)
if s.check() == sat:
	print(s.model())
# _solve = s.model()
# print(_solve)

image-20240302165540789

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
from z3 import *

s = Solver()
code = [Int(str(i)) for i in range(3)]


def GoodValueBadPlace(nums, count):
    exps = []
    for i in range(len(nums)):
        for j in range(len(code)):
            if i == j:
                continue
            else:
                exps.append(If(nums[i] == code[j], 1, 0))
    return Sum(exps) == count


# one number is correct and well-placed
s.add(Or(code[0] == 2, code[1] == 9, code[2] == 1))
# one number is correct but wrong placed
s.add(GoodValueBadPlace([2, 4, 5], 1))
# two numbers are correct but wrong placed
s.add(GoodValueBadPlace([4, 6, 3], 2))
# nothing is correct
s.add(And(code[0] != 5, code[1] != 7, code[2] != 9))
# one number is correct but wrong placed
s.add(GoodValueBadPlace([5, 6, 9], 1))

if s.check() == sat:
    m = s.model()
    for c in code:
        print(m[c], end=' ')