z3求解

之前有题应该使用z3求解的一直没有完成,今天就好好学习一下z3,把这题解决了顺便记录一下z3求解的使用!

z3求解大致模版:

1
2
3
4
5
6
from z3 import *
x=Int('x') //定义变量
solver=Solver() //构造求解器
solver.add(x==1)//添加约束条件
if solver.check()==sat: //如果有解返回值为sat否则返回unsat
print solver.model() //打印解

之前一题的z3使用分析:

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
from z3 import *
num=BitVec("num",33) //这里定义了num为一个32位的二进制数字,至于为什么要写33,是我尝试了很多次无解后发现写33就有解了2333
array=[
164,
25,
4,
130,
126,
158,
91,
199,
173,
252,
239,
143,
150,
251,
126,
39,
104,
104,
146,
208,
249,
9,
219,
208,
101,
182,
62,
92,
6,
27,
5,
46]
b=range(32)
for i in range(32):
temp=0
for j in range(i):
temp^=array[j]
b[i]=temp
solver=Solver()
solver.add(array[0]^(num&0xff)^b[0]==ord('F')). //根据题目添加条件
solver.add(array[1]^((num>>1)&0xff)^b[1]==ord('L'))
solver.add(array[2]^((num>>2)&0xff)^b[2]==ord('A'))
solver.add(array[3]^((num>>3)&0xff)^b[3]==ord('G'))
solver.add(array[4]^((num>>4)&0xff)^b[4]==ord('{'))
for i in range(5,31): //多次重复的输入可以用循环来操作
solver.add(array[i]^((num>>i)&0xff)^b[i]<=90)
solver.add(array[i]^((num>>i)&0xff)^b[i]>=65)
solver.add(array[31]^((num>>31)&0xff)^b[31]==ord('}'))
if solver.check()==sat :
print solver.model() //得到正确的num

这种简单的z3求解的运用不是很难,但是却比爆破之类的方法来的快很多。
其实今天也没学习多少有关z3的,之前一直无解只有因为定义的时候没用33……

文章目录
|