Z3求解方程组

基本用法

变量表示

  • Int-整数型
1
2
3
from z3 import *
a=Int('a')#声明单个整型变量
a,b=Ints('a b')#声明多个整型变量
  • Real-实数型
1
2
3
from z3 import *
a=Real('a')#声明单个实性变量
a,b=Reals('a b')
  • BitVec-向量
1
2
3
from z3 import *
a=BitVec('a',8)#声明单个8位的变量
a,b=BitVec('a b',8)#声明多个8位的变量

只有向量类型可以进行位运算（异或，左右移位等）

  • 布尔类型
1
p=z3.Bool(name='p')
  • 整型宇实数类型变量之间可以互相进行转换
1
2
3
4
>>> z3.ToReal(x) 
ToReal(x)
>>> z3.ToInt(y) 
ToInt(y)

常量表示

除了python原有的常量数据类型外，我们也可以使用z3自带的常量类型参与运算：

1
2
3
4
5
6
7
8
>>> z3.IntVal(val = 114514) # integer 
114514 
>>> z3.RealVal(val = 1919810) # real number 
1919810 
>>> z3.BitVecVal(val = 1145141919810, bv = 32) # bit vector，自动截断 
2680619074 
>>> z3.BitVecVal(val = 1145141919810, bv = 64) # bit vector 
1145141919810

求解器

在使用z3进行约束求解之前我们首先需要获得一个求解器类实例，本质上其实就是一组约束的集合：

1
s=z3.Solver()

添加约束

我们可以通过求解器的add()方法为指定求解器添加约束条件，约束条件可以直接通过z3变量组成的式子进行表示：

1
2
s.add(x*5==10)
s.add(y*1/2==x)

对于布尔类型的式子而言，我们可以使用z3内置的And()、Or()、Not()、Implies()等方法进行布尔逻辑运算：

1
2
3
s.add(z3.Implies(p,q))
s.add(r==z3.Not(q))
s.add(z3.Or(z3.Not(p),r))

约束求解

当我们向求解器中添加约束条件之后，我们可以使用check()方法检查约束是否是可满足的（satisfiable，即z3是否能够帮我们找到一组解）：

  • z3.sat：约束可以被满足
  • z3.unsat：约束无法被满足
1
s.check()

若约束可以被满足，则我们可以通过model()方法获取到一组解：

1
s.model()

对于约束条件比较少的情况，我们也可以无需创建求解器，直接通过solve()方法进行求解：

1
z3.solve(z3.Implies(p,q),r==z3.Not(q),z3.Or(z3.Not(p),r))

常规使用

  • 解方程
1
2
3
4
from z3 import *
a,b=Ints('a b')
#solve函数
solve(a+b==10,a+3*b==12)
  • 化简表达式
1
2
3
4
5
6
from z3 import *
x=Int('x')
y=Int('y')
print (simplify(x + y + 2*x + 3))
print (simplify(x < y + x + 2))
print (simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))

进阶使用

  • 当需要取出特定变量的时候，可以使用Solver求解器
1
2
3
4
5
6
7
8
9
10
11
12
13
14
from z3 import *
a,b = Ints('a b')

s=Solver()  #创建一个解的对象s
s.add(a + b == 10)#添加约束条件
s.add(a + 3 * b == 12)

if s.check() == sat: #check() 检查解是否存在，存在会return 'sat'
	result = s.model() #输出

print(result)

print(result[a])
print(result[b])

例题

[GDOUCTF 2023]Check_Your_Luck

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
from z3 import *

#创建求解器实例
s=z3.Solver()

#定义变量
v,w,x,y,z=Ints("v w x y z")

#添加约束条件
s.add(v * 23 + w * -32 + x * 98 + y * 55 + z * 90 == 333322)
s.add(v * 123 + w * -322 + x * 68 + y * 67 + z * 32 == 707724)
s.add(v * 266 + w * -34 + x * 43 + y * 8 + z * 32 == 1272529)
s.add(v * 343 + w * -352 + x * 58 + y * 65 + z * 5 == 1672457)
s.add(v * 231 + w * -321 + x * 938 + y * 555 + z * 970 == 3372367)

#检查是否有解
if s.check()==sat:
    model=s.model()
    print("flag{",end="")
    print(f"{model[v]}",end="")
    print("_",end="")
    print(f"{model[w]}",end="")
    print("_",end="")
    print(f"{model[x]}",end="")
    print("_",end="")
    print(f"{model[y]}",end="")
    print("_",end="")
    print(f"{model[z]}",end="")
    print("}")

[MoeCTF 2021]大佬请喝coffee

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 *

#生成一组整数变量，并将它们存储在一个列表中
charArray = [Int("input[%d]"%i) for i in range(9)]

#创建求解器实例
s=z3.Solver()

#添加约束条件
s.add((charArray[0] * 4778) + (charArray[1] * 3659) + (charArray[2] * 9011) + (charArray[3] * 5734) + (charArray[4] * 4076) + (charArray[5] * 6812) + (charArray[6] * 8341) + (charArray[7] * 6765) + (charArray[8] * 7435) == 5711942)
s.add((charArray[0] * 4449) + (charArray[1] * 5454) + (charArray[2] * 4459) + (charArray[3] * 5800) + (charArray[4] * 6685) + (charArray[5] * 6120) + (charArray[6] * 7357) + (charArray[7] * 3561) + (charArray[8] * 5199) == 4885863) 
s.add((charArray[0] * 3188) + (charArray[1] * 6278) + (charArray[2] * 9411) + (charArray[3] * 5760) + (charArray[4] * 9909) + (charArray[5] * 7618) + (charArray[6] * 7184) + (charArray[7] * 4791) + (charArray[8] * 8686) == 6387690)
s.add((charArray[0] * 8827) + (charArray[1] * 7419) + (charArray[2] * 7033) + (charArray[3] * 9306) + (charArray[4] * 7300) + (charArray[5] * 5774) + (charArray[6] * 6588) + (charArray[7] * 5541) + (charArray[8] * 4628) == 6077067)
s.add((charArray[0] * 5707) + (charArray[1] * 5793) + (charArray[2] * 4589) + (charArray[3] * 6679) + (charArray[4] * 3972) + (charArray[5] * 5876) + (charArray[6] * 6668) + (charArray[7] * 5951) + (charArray[8] * 9569) == 5492294)
s.add((charArray[0] * 9685) + (charArray[1] * 7370) + (charArray[2] * 4648) + (charArray[3] * 7230) + (charArray[4] * 9614) + (charArray[5] * 9979) + (charArray[6] * 8309) + (charArray[7] * 9631) + (charArray[8] * 9272) == 7562511)
s.add((charArray[0] * 6955) + (charArray[1] * 8567) + (charArray[2] * 7949) + (charArray[3] * 8699) + (charArray[4] * 3284) + (charArray[5] * 6647) + (charArray[6] * 3175) + (charArray[7] * 8506) + (charArray[8] * 6552) == 5970432)
s.add((charArray[0] * 4323) + (charArray[1] * 4706) + (charArray[2] * 8081) + (charArray[3] * 7900) + (charArray[4] * 4862) + (charArray[5] * 9544) + (charArray[6] * 5211) + (charArray[7] * 7443) + (charArray[8] * 5676) == 5834523)
s.add((charArray[0] * 3022) + (charArray[1] * 8999) + (charArray[2] * 5058) + (charArray[3] * 4529) + (charArray[4] * 3940) + (charArray[5] * 4279) + (charArray[6] * 4606) + (charArray[7] * 3428) + (charArray[8] * 8889) == 4681110) 

#检查是否有解
if s.check()==sat:
    model=s.model()
    for i in range(9):
        print(chr(int(str(model[charArray[i]]))),end = '')

[HNCTF 2022 WEEK2]

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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
from z3 import *

v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15,v16,v17,v18,v19,v20,v21,v22,v23 = Ints("v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23")
s=z3.Solver()

s.add(245 * v6 + 395 * v5 + 3541 * v4 + 2051 * v3 + 3201 * v2 + 1345 * v7 == 855009)
s.add(3270 * v6 + 3759 * v5 + 3900 * v4 + 3963 * v3 + 1546 * v2 + 3082 * v7 == 1515490)
s.add(526 * v6 + 2283 * v5 + 3349 * v4 + 2458 * v3 + 2012 * v2 + 268 * v7 == 854822)
s.add(3208 * v6 + 2021 * v5 + 3146 * v4 + 1571 * v3 + 2569 * v2 + 1395 * v7 == 1094422)
s.add(3136 * v6 + 3553 * v5 + 2997 * v4 + 1824 * v3 + 1575 * v2 + 1599 * v7 == 1136398)
s.add(2300 * v6 + 1349 * v5 + 86 * v4 + 3672 * v3 + 2908 * v2 + 1681 * v7 == 939991)
s.add(212 * v22 + 153 * v21 + 342 * v20 + 490 * v12 + 325 * v11 + 485 * v10 + 56 * v9 + 202 * v8 + 191 * v23 == 245940)
s.add(348 * v22 + 185 * v21 + 134 * v20 + 153 * v12 + 460 * v9 + 207 * v8 + 22 * v10 + 24 * v11 + 22 * v23 == 146392)
s.add(177 * v22 + 231 * v21 + 489 * v20 + 339 * v12 + 433 * v11 + 311 * v10 + 164 * v9 + 154 * v8 + 100 * v23 == 239438)
s.add(68 * v20 + 466 * v12 + 470 * v11 + 22 * v10 + 270 * v9 + 360 * v8 + 337 * v21 + 257 * v22 + 82 * v23 == 233887)
s.add(246 * v22 + 235 * v21 + 468 * v20 + 91 * v12 + 151 * v11 + 197 * v8 + 92 * v9 + 73 * v10 + 54 * v23 == 152663)
s.add(241 * v22 + 377 * v21 + 131 * v20 + 243 * v12 + 233 * v11 + 55 * v10 + 376 * v9 + 242 * v8 + 343 * v23 == 228375)
s.add(356 * v22 + 200 * v21 + 136 * v11 + 301 * v10 + 284 * v9 + 364 * v8 + 458 * v12 + 5 * v20 + 61 * v23 == 211183)
s.add(154 * v22 + 55 * v21 + 406 * v20 + 107 * v12 + 80 * v10 + 66 * v8 + 71 * v9 + 17 * v11 + 71 * v23 == 96788)
s.add(335 * v22 + 201 * v21 + 197 * v11 + 280 * v10 + 409 * v9 + 56 * v8 + 494 * v12 + 63 * v20 + 99 * v23 == 204625)
s.add(428 * v18 + 1266 * v17 + 1326 * v16 + 1967 * v15 + 3001 * v14 + 81 * v13 + 2439 * v19 == 1109296)
s.add(2585 * v18 + 4027 * v17 + 141 * v16 + 2539 * v15 + 3073 * v14 + 164 * v13 + 1556 * v19 == 1368547)
s.add(2080 * v18 + 358 * v17 + 1317 * v16 + 1341 * v15 + 3681 * v14 + 2197 * v13 + 1205 * v19 == 1320274)
s.add(840 * v18 + 1494 * v17 + 2353 * v16 + 235 * v15 + 3843 * v14 + 1496 * v13 + 1302 * v19 == 1206735)
s.add(101 * v18 + 2025 * v17 + 2842 * v16 + 1559 * v15 + 2143 * v14 + 3008 * v13 + 981 * v19 == 1306983)
s.add(1290 * v18 + 3822 * v17 + 1733 * v16 + 292 * v15 + 816 * v14 + 1017 * v13 + 3199 * v19 == 1160573)
s.add(186 * v18 + 2712 * v17 + 2136 * v16 + 98 * v13 + 138 * v14 + 3584 * v15 + 1173 * v19== 1005746)

if s.check()==sat:
    model=s.model()
    print(chr(int(str(model[v2]))),end="")
    print(chr(int(str(model[v3]))),end="")
    print(chr(int(str(model[v4]))),end="")
    print(chr(int(str(model[v5]))),end="")
    print(chr(int(str(model[v6]))),end="")
    print(chr(int(str(model[v7]))),end="")
    print(chr(int(str(model[v8]))),end="")
    print(chr(int(str(model[v9]))),end="")
    print(chr(int(str(model[v10]))),end="")
    print(chr(int(str(model[v11]))),end="")
    print(chr(int(str(model[v12]))),end="")
    print(chr(int(str(model[v13]))),end="")
    print(chr(int(str(model[v14]))),end="")
    print(chr(int(str(model[v15]))),end="")
    print(chr(int(str(model[v16]))),end="")
    print(chr(int(str(model[v17]))),end="")
    print(chr(int(str(model[v18]))),end="")
    print(chr(int(str(model[v19]))),end="")
    print(chr(int(str(model[v20]))),end="")
    print(chr(int(str(model[v21]))),end="")
    print(chr(int(str(model[v22]))),end="")
    print(chr(int(str(model[v23]))),end="")

[羊城杯 2020]login

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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
from z3 import *
import hashlib

def md5_encrypt(data):
    # 创建 MD5 哈希对象
    md5 = hashlib.md5()
    
    # 更新哈希对象，data 必须是字节类型
    md5.update(data.encode('utf-8'))
    
    # 获取十六进制的 MD5 哈希值
    return md5.hexdigest()


s=z3.Solver()
a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14=Ints("a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14")

s.add((((a1 * 88 + a2 * 67 + a3 * 65 - a4 * 5) + a5 * 43 + a6 * 89 + a7 * 25 + a8 * 13 - a9 * 36) + a10 * 15 + a11 * 11 + a12 * 47 - a13 * 60) + a14 * 29 == 22748) 
s.add((((a1 * 89 + a2 * 7 + a3 * 12 - a4 * 25) + a5 * 41 + a6 * 23 + a7 * 20 - a8 * 66) + a9 * 31 + a10 * 8 + a11 * 2 - a12 * 41 - a13 * 39) + a14 * 17 == 7258) 
s.add((((a1 * 28 + a2 * 35 + a3 * 16 - a4 * 65) + a5 * 53 + a6 * 39 + a7 * 27 + a8 * 15 - a9 * 33) + a10 * 13 + a11 * 101 + a12 * 90 - a13 * 34) + a14 * 23 == 26190) 
s.add((((a1 * 23 + a2 * 34 + a3 * 35 - a4 * 59) + a5 * 49 + a6 * 81 + a7 * 25 + (a8*0x80) - a9 * 32) + a10 * 75 + a11 * 81 + a12 * 47 - a13 * 60) + a14 * 29 == 37136) 
s.add(((a1 * 38 + a2 * 97 + a3 * 35 - a4 * 52) + a5 * 42 + a6 * 79 + a7 * 90 + a8 * 23 - a9 * 36) + a10 * 57 + a11 * 81 + a12 * 42 - a13 * 62 - a14 * 11 == 27915)
s.add((((a1 * 22 + a2 * 27 + a3 * 35 - a4 * 45) + a5 * 47 + a6 * 49 + a7 * 29 + a8 * 18 - a9 * 26) + a10 * 35 + a11 * 41 + a12 * 40 - a13 * 61) + a14 * 28 == 17298)
s.add((((a1 * 12 + a2 * 45 + a3 * 35 - a4 * 9 - a5 * 42) + a6 * 86 + a7 * 23 + a8 * 85 - a9 * 47) + a10 * 34 + a11 * 76 + a12 * 43 - a13 * 44) + a14 * 65 == 19875) 
s.add(((a1 * 79 + a2 * 62 + a3 * 35 - a4 * 85) + a5 * 33 + a6 * 79 + a7 * 86 + a8 * 14 - a9 * 30) + a10 * 25 + a11 * 11 + a12 * 57 - a13 * 50 - a14 * 9 == 22784) 
s.add((((a1 * 8 + a2 * 6 + a3 * 64 - a4 * 85) + a5 * 73 + a6 * 29 + a7 * 2 + a8 * 23 - a9 * 36) + a10 * 5 + a11 * 2 + a12 * 47 - a13 * 64) + a14 * 27 == 9710) 
s.add(((((a1 * 67 - a2 * 68) + a3 * 68 - a4 * 51 - a5 * 43) + a6 * 81 + a7 * 22 - a8 * 12 - a9 * 38) + a10 * 75 + a11 * 41 + a12 * 27 - a13 * 52) + a14 * 31 == 13376) 
s.add((((a1 * 85 + a2 * 63 + a3 * 5 - a4 * 51) + a5 * 44 + a6 * 36 + a7 * 28 + a8 * 15 - a9 * 6) + a10 * 45 + a11 * 31 + a12 * 7 - a13 * 67) + a14 * 78 == 24065) 
s.add((((a1 * 47 + a2 * 64 + a3 * 66 - a4 * 5) + a5 * 43 + a6 * 112 + a7 * 25 + a8 * 13 - a9 * 35) + a10 * 95 + a11 * 21 + a12 * 43 - a13 * 61) + a14 * 20 == 27687) 
s.add(((a1 * 89 + a2 * 67 + a3 * 85 - a4 * 25) + a5 * 49 + a6 * 89 + a7 * 23 + a8 * 56 - a9 * 92) + a10 * 14 + a11 * 89 + a12 * 47 - a13 * 61 - a14 * 29 == 29250) 
s.add(((a1 * 95 + a2 * 34 + a3 * 62 - a4 * 9 - a5 * 43) + a6 * 83 + a7 * 25 + a8 * 12 - a9 * 36) + a10 * 16 + a11 * 51 + a12 * 47 - a13 * 60 - a14 * 24 == 15317)

if s.check()==sat:
    model=s.model()

direct = {
    13 : 33,
    3 : 7,
    4 : 104,
    10 : 88,
    12 : 88,
    1 : 24,
    7 : 91,
    9 : 52,
    6 : 28,
    5 : 43,
    0 : 10,
    8 : 108,
    2 : 119,
    11 : 74}

flag = [0 for i in range(15)]
for i in direct:
    flag[i] = direct[i]
    
for i in range(13, -1, -1):
    flag[i] ^= flag[i+1]
    
flag_str = ''
for i in range(14):
    flag_str += chr(flag[i])
print("NSSCTF{",end="")    
print(md5_encrypt(flag_str),end="")
print("}")

[强网杯 2022]GameMaster

[CISCN 2021初赛]babybc

2024YLCTF [Round 2] ezapk

2024 极客大挑战 我勒个z3啊

≡