丰富的线上&线下活动，深入探索云世界
做任务，得社区积分和周边
最真实的开发者用云体验
让每位学生受益于普惠算力
让创作激发创新
资深技术专家手把手带教
遇见技术追梦人
技术交流，直击现场
海量开发者使用工具、手册，免费下载
极速、全面、稳定、安全的开源镜像
开发手册、白皮书、案例集等实战精华
为开发者定制的Chrome浏览器插件
各位小伙伴大家好，今天我将给大家演示一个非常高级的工具，SMT求解器。应用领域非常广，解各类方程，解各类编程问题（例如解数独），解逻辑题等都不在话下。
今天小小明就将带大家看看这其中的精彩：
z3-solver是由MicrosoftResearch(微软)开发的SMT求解器，它用于检查逻辑表达式的可满足性，可以找到一组约束中的其中一个可行解，缺点是无法找出所有的可行解（对于规划求解问题可以是scipy）。
z3-solver可应用于软/硬件的验证与测试、约束求解、混合系统的分析、安全、生物，以及几何求解等问题。Z3主要由C++开发，提供了.NET、C、C++、Java、Python等语言调用接口，下面以python接口展开讲解。
z3可直接通过pip安装：
z3中有3种类型的变量，分别是整型(Int)，实型(Real)和向量(BitVec)。
对于整数类型数据，基本API：
对于实数类型的API与整数类型一致，向量(BitVec)则稍有区别：
simplify(表达式)，对可以简化的表达式进行简化。
下面我们看看z3的基本用法：
先以一个简单例子入门：
比如使用z3解二元一次方程：
$x-y=3$
$3x-8y=4$
solve直接求解：
fromz3import*x,y=Reals('xy')solve(x-y==3,3*x-8*y==4)[y=1,x=4]如果需要取出指定变量的结果，可以使用Solver求解器：
x,y=Reals('xy')solver=Solver()qs=[x-y==3,3*x-8*y==4]forqinqs:solver.add(q)ifsolver.check()==sat:result=solver.model()print(result)print("x=",result[x],",y=",result[y])[y=1,x=4]x=4,y=1可以通过solver.assertions()查看求解器已经添加的约束和约束的个数：
assertions=solver.assertions()print(assertions)print(len(assertions))[x-y==3,3*x-8*y==4]2如果需要删除约束条件，则需要在添加约束前调用solver.push()方法。
下面我们如下方程为例进行演示：
$x>10$
$y=x+2$
获取结果：
x,y=Ints('xy')solver=Solver()solver.add(x>10,y==x+2)print("当前约束：",solver.assertions())ifsolver.check()==sat:print("结果：",solver.model())else:print(solver.check())当前约束：[x>10,y==x+2]结果：[x=11,y=13]下面我们再增加一个可以被删除的约束y<11：
solver.push()solver.add(y<11)print("当前约束：",solver.assertions())ifsolver.check()==sat:print("结果：",solver.model())else:print(solver.check())当前约束：[x>10,y==x+2,y<11]unsat可以看到这种约束下，无有效解。
删除约束，再计算一次：
solver.pop()print("当前约束：",solver.assertions())ifsolver.check()==sat:print("结果：",solver.model())else:print(solver.check())当前约束：[x>10,y==x+2]结果：[x=11,y=13]注意：没有push过的约束条件时直接pop会导致报出Z3Exception:b'indexoutofbounds'错误。线性多项式约束约束条件为：
$$x>2\\y<10\\x+2*y=7\\$$
上述约束x和y都是整数，我们需要找到其中一个可行解：
x,y=Ints('xy')solve([x>2,y<10,x+2*y==7])结果：
[y=0,x=7]当然，实际可行的解不止这一个，z3只能找到其中一个可行的解。
约束条件为：
$x^2+y^2>3$
$x^3+y<5$
上述约束x和y都是实数，我们需要找到其中一个可行解：
x,y=Reals('xy')solve(x**2+y**2>3,x**3+y<5)结果：
[y=2,x=1/8]很快就计算出了一个可行解。
高中物理中的匀变速直线运动公式为：
$s=v_it+\frac12at^2$
$v_f=v_i+at$
举个例子，以30m/s的速度前进时踩下刹车，如果减速的加速度为$-8m/s^2$，求刹车完毕时，汽车的刹车距离是多少？
直接解题：
s,v_i,a,t,v_f=Reals('sv__iatv__f')equations=[s==v_i*t+(a*t**2)/2,v_f==v_i+a*t,]print("运动方程:",equations)variables=[v_i==30,v_f==0,a==-8]print("参数变量:",variables)print("结果:")solve(equations+variables)运动方程:[s==v__i*t+(a*t**2)/2,v__f==v__i+a*t]参数变量:[v__i==30,v__f==0,a==-8]结果:[a=-8,v__f=0,v__i=30,t=15/4,s=225/4]可以看到刹车距离是225/4m，刹车历时15/4s。
需要获取指定变量的结果则需要Solver求解器：
之前我演示过程序自动玩数独：
文中对于一个困难级别的数独，python优化后的算法耗时达到3.2秒，核心逻辑使用C语言改写后耗时达到毫秒级。
下面我使用z3求解器来解决这个问题，这样可以在不使用其他语言开发的情况，纯Python就能达到不错的性能。
首先，我们根据数独游戏的规则创建约束条件：
fromz3import*#9x9整数变量矩阵X=[[Int(f"x_{i}_{j}")forjinrange(9)]foriinrange(9)]#每个单元格在1,2,3,...8,9中包含一个值cells_c=[And(1<=X[i][j],X[i][j]<=9)foriinrange(9)forjinrange(9)]#每行每个数字最多出现一次rows_c=[Distinct(X[i])foriinrange(9)]#每列每个数字最多出现一次cols_c=[Distinct([X[i][j]foriinrange(9)])forjinrange(9)]#每个3x3方格每个数字最多出现一次sq_c=[Distinct([X[3*i0+i][3*j0+j]foriinrange(3)forjinrange(3)])fori0inrange(3)forj0inrange(3)]#数独完整约束条件sudoku_c=cells_c+rows_c+cols_c+sq_c依然针对之前那个Python耗时3秒多的数独：
#需要求解的数独，0表示空单元格board=[[0,0,0,6,0,0,0,3,0],[5,0,0,0,0,0,6,0,0],[0,9,0,0,0,5,0,0,0],[0,0,4,0,1,0,0,0,6],[0,0,0,4,0,3,0,0,0],[8,0,0,0,9,0,5,0,0],[0,0,0,7,0,0,0,4,0],[0,0,5,0,0,0,0,0,8],[0,3,0,0,0,8,0,0,0]]求解：
有一个8x8的棋盘，希望往里放8个棋子（皇后），每个棋子所在的行、列、对角线都不能有另一个棋子。
下图中左图是满足条件的一种方法，又图是不满足条件的。八皇后问题就是期望找到满足这种要求的放棋子方式：
如果我们要求找到所有满足条件的解，则只想使用回溯算法进行递归求解，但是如果只需要一个可行解时，我们则可以使用z3求解器。
首先创建约束条件：
#每个皇后必须在不同的行中，记录每行对应的皇后对应的列位置Q=[Int(f'Q_{i}')foriinrange(8)]#每个皇后在列0,1,2,...,7val_c=[And(0<=Q[i],Q[i]<=7)foriinrange(8)]#每列最多一个皇后col_c=[Distinct(Q)]#对角线约束diag_c=[If(i==j,True,And(Q[i]-Q[j]!=i-j,Q[i]-Q[j]!=j-i))foriinrange(8)forjinrange(i)]直接求解可以得到一个可行解中，其中每个皇后的列位置：
solve(val_c+col_c+diag_c)结果：
[Q_3=5,Q_1=1,Q_7=6,Q_5=2,Q_4=0,Q_0=3,Q_2=7,Q_6=4]当然我们还可以把结果打印的清晰一点：
defprint_eight_queen(result):forcolumninresult:foriinrange(8):ifi==column:print(end="Q")else:print(end="*")print()s=Solver()s.add(val_c+col_c+diag_c)ifs.check()==sat:result=s.model()result=[result[Q[i]].as_long()foriinrange(8)]print("每行皇后所在的列位置：",result)print_eight_queen(result)结果：
每行皇后所在的列位置：[5,3,1,7,4,6,0,2]*****Q*****Q*****Q*************Q****Q*********Q*Q*********Q*****安装依赖问题安装程序时往往存在依赖和冲突的关系，通过z3可以轻松求解正确的包的安装顺序。
例如：
假设要安装包a编码如下：
fromz3import*a,b,c,d,e,f,g,z=Bools('abcdefgz')#1.包a依赖于包b、c和zq1=And([Implies(a,dep)fordepin[b,c,z]])#2.包b依赖于包dq2=Implies(b,d)#3.包c，依赖于d或e，以及f或gq3=Implies(c,And([Or(d,e),Or(f,g)]))#4.包d与包e冲突q4=Or(Not(d),Not(e))#5.包d与包g冲突q5=Or(Not(d),Not(g))s=Solver()#安装包as.add(a,q1,q2,q3,q4,q5)ifs.check()==sat:m=s.model()#x()返回Z3表达式，x.name()返回字符串r=[x.name()forxinmifis_true(m[x])]print("安装a:")print(r)else:print("无效的安装配置")安装a:['z','b','d','f','c','a']为了方便调用我们可以将依赖和冲突封装成单独的方法：
defDependsOn(pack,deps):ifis_expr(deps):returnImplies(pack,deps)else:returnAnd([Implies(pack,dep)fordepindeps])defConflict(*packs):returnOr([Not(pack)forpackinpacks])definstall_check(*problem):s=Solver()s.add(problem)ifs.check()==sat:m=s.model()#x()返回Z3表达式，x.name()返回字符串r=[x.name()forxinmifis_true(m[x])]print(r)else:print("无效的安装配置")再次调用安装a：
a,b,c,d,e,f,g,z=Bools('abcdefgz')print("安装a:")install_check(a,DependsOn(a,[b,c,z]),DependsOn(b,d),DependsOn(c,[Or(d,e),Or(f,g)]),Conflict(d,e),Conflict(d,g),)安装a:['z','b','d','f','c','a']安装a和g：
print("安装a和g:")install_check(a,g,DependsOn(a,[b,c,z]),DependsOn(b,d),DependsOn(c,[Or(d,e),Or(f,g)]),Conflict(d,e),Conflict(d,g),)安装a和g:无效的安装配置可以看到z3成功计算出存在冲突的a和g。
在解决了编程问题后，我们最后玩两道逻辑题：
A.甲、乙、丙都是窃贼B.甲和乙都是窃贼C.丙是窃贼D.甲是窃贼
完整解题代码：
#abc分别代表甲、乙、丙是否是盗贼a,b,c=Bools('abc')#三人至少有一个是窃贼q1=Or(a,b,c)#如甲是窃贼，则乙一定是同案犯；q2=Implies(a,b)#乙一定不是q3=Not(b)s=Solver()s.add(q1,q2,q3)options=[#甲、乙、丙都是窃贼And(a,b,c),#甲甲和乙都是窃贼And(a,b),#丙是窃贼c,#甲是窃贼a]result=[]foranswer,optioninzip("ABCD",options):s.push()s.add(option)print(answer,s.check(),s.assertions())ifs.check()==sat:result.append(answer)s.pop()print("最终答案：","".join(result))Aunsat[Or(a,b,c),Implies(a,b),Not(b),And(a,b,c)]Bunsat[Or(a,b,c),Implies(a,b),Not(b),And(a,b)]Csat[Or(a,b,c),Implies(a,b),Not(b),c]Dunsat[Or(a,b,c),Implies(a,b),Not(b),a]最终答案：C上述结果可以看到只有第3条的结果为sat（有解），说明对应的选项C是正确的。
题目如下：
矿工甲：发生事故的原因是设备问题；矿工乙：有人违反了操作规程，但发生事故的原因不是设备问题；矿工丙：如果发生事故的原因是设备问题，那么有人违反操作规程；矿工丁：发生事故的原因是设备问题，但没有人违反操作规程。
如果上述四人的断定中只有一个人为真，则以下可能为真的一项是（）。
A.矿工甲的断定为真B.矿工乙的断定为真C.矿工丁的断定为真D.矿工丙的断定为真，有人违反了操作规程E.矿工丙的断定为真，没有人违反操作规程
首先需要定义题目中的两个命题，设备是否有问题和是否有人违反操作规程。
equipment=Bool('equipment')#设备是否有问题violation=Bool('violation')#是否违反操作规程qs=[#甲：发生事故的原因是设备问题；equipment,#乙：有人违反了操作规程，但发生事故的原因不是设备问题；And(violation,Not(equipment)),#丙：如果发生事故的原因是设备问题，那么有人违反操作规程；Implies(equipment,violation),#丁：发生事故的原因是设备问题，但没有人违反操作And(equipment,Not(violation)),]s=Solver()#上述四人的断定中只有一个人为真s.add(Sum([If(q,1,0)forqinqs])==1)#逐个判断各个选项是否正确options=[qs[0],qs[1],qs[3],And(qs[2],violation),And(qs[2],Not(violation))]result=[]foranswer,optioninzip("ABCDE",options):s.push()s.add(option)print(answer,s.check(),s.assertions())ifs.check()==sat:result.append(answer)s.pop()print("最终答案：","".join(result))