z3solver求解器

丰富的线上&线下活动,深入探索云世界

做任务,得社区积分和周边

最真实的开发者用云体验

让每位学生受益于普惠算力

让创作激发创新

资深技术专家手把手带教

遇见技术追梦人

技术交流,直击现场

海量开发者使用工具、手册,免费下载

极速、全面、稳定、安全的开源镜像

开发手册、白皮书、案例集等实战精华

为开发者定制的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))

THE END
1.关于八皇后问题以及回溯递归思想大家好,我是“Stephen·谢”,本文以古老的八皇后问题的文字解释和代码实现,将递归回溯的思想概念介绍给大家。 国际象棋中的皇后比中国象棋里的大车还厉害,皇后能横向,纵向和斜向移动,在这三条线上的其他棋子都可以被吃掉。所谓八皇后问题就是:将八位皇后放在一张8x8的棋盘上,使得每位皇后都无法吃掉别的皇后,(即https://www.jianshu.com/p/65c8c60b83b8
2.递归算法学习系列之八皇后问题八皇后问题递归算法递归算法学习系列之八皇后问题 1.引子 中国有一句古话,叫做“不撞南墙不回头",生动的说明了一个人的固执,有点贬义,但是在软件编程中,这种思路确是一种解决问题最简单的算法,它通过一种类似于蛮干的思路,一步一步地往前走,每走一步都更靠近目标结果一些,直到遇到障碍物,我们才考虑往回走。然后再继续尝试向前。https://blog.csdn.net/garfielder007/article/details/48811597/
3.栈(stack)递归(八皇后问题)排序算法分类,时间和空间复杂度简介栈(stack)、递归(八皇后问题)、排序算法分类,时间和空间复杂度简介,一、栈的介绍:1)栈的英文为(stack)2)栈是一个先入后出(FILO-FirstInLastOut)的有序列表。3)栈(stack)是限制线性表中元素的插入和删除只能在线性表的同一端进行的一种特殊线性表。允许插入和删除的一端https://blog.51cto.com/u_15127559/4525280
4.CPP递归与回溯入门·八皇后问题腾讯云开发者社区【CPP】递归与回溯入门·八皇后问题 八皇后问题,一个经典的回溯算法问题。在8*8的国际象棋棋盘上如何才能放上八只皇后棋子,使它们彼此不会互相攻击到。皇后,是能攻击到以自己为中心的横线竖线和正斜线的强大棋子,在这样的棋盘上摆放8个皇后,这个程序就是要解决到底有多少种摆放法。历史上有那么多的大师研究这个https://cloud.tencent.com/developer/article/1670153
5.经典回溯算法——八皇后问题经典回溯算法——八皇后问题 八皇后问题是由19世纪数学家“搞死先生”(高斯先生)提出的,具体的问题是这样的: 在国际象棋的棋盘中(有8×8格)摆放8个皇后,这八个皇后不能相互攻击到(皇后的攻击方向很广:横着,竖着,斜着都能攻击),即8个皇后不能处于同行、同列、同一正反对角线上,这样就不能相互攻击到了。那么https://www.nowcoder.com/discuss/83692
6.科学网—经典的算法回顾子问题重叠性质是指在用递归算法自顶向下对问题进行求解时,每次产生的子问题并不总是新问题,有些子问题会被重复计算多次。动态规划算法正是利用了这种子问题的重叠性质,对每一个子问题只计算一次,然后将其计算结果保存在一个表格中,当再次需要计算已经计算过的子问题时,只是在表格中简单地查看一下结果,从而获得较https://blog.sciencenet.cn/blog-315535-665392.html
7.23Julia编程示例–递归趣例Julia语言入门23.2.2 递归算法 穷举法完全不考虑已经摆放的棋子,所以另一种更好的做法是使用递归算法,先在第一行摆下一颗棋子,这有8种摆法;然后,在第二行试图摆下第二颗棋子,使得与第一颗棋子不冲突;再考虑第三颗棋子,如此一直到第八颗棋子。这个过程中如果某颗棋子无法摆放,就退回到上一颗棋子的下一个位置;找到一种摆法https://www.math.pku.edu.cn/teachers/lidf/docs/Julia/html/_book/exa-recurse.html
8.八皇后(最小冲突法)解决八皇后问题 用简单的java语言解决了八皇后问题,适用于初学者。 上传者:u012249535时间:2013-12-07 算法设计文档(含回溯法 递归法 贪心算法 背包) 算法讲的很详细,对学习算法和准备面试工作的朋友都很有帮助,推荐你下载学习! 上传者:chendonghui198484时间:2010-11-26 https://www.iteye.com/resource/u010890477-7014031
9.11.5.八皇后问题?求解—Python3教程文档如果下一个皇后和当前皇后的水平距离为0(在同一列)或与它们的垂直距离相等(位于一条对角线上),这个表达式就为真;否则为假。 基线条件? 八皇后问题解决起来有点棘手,但通过使用生成器并不太难。然而,如果你不熟悉递归,就 很难自己想出这里的解决方案。另外,这个解决方案的效率不是特别高,因此皇后非常多时,其https://www.osgeo.cn/python-tutorial/advfea-queenseight.html
10.C语言回溯法解八皇后问题(八皇后算法)C语言八皇后问题(N皇后问题)的回溯法求解一、问题描述在一个国际象棋棋盘上放置八个皇后,使得任何两个皇后之间不相互攻击,求出所有的布棋方法,并推广到N皇后情况。二、参考资料啥文字都不用看,B站上有个非常详细的动画视频解说,上链接!!!Click Here!三、源代码https://www.jb51.net/article/233081.htm
11.算法精粹:经典计算机科学问题的Python实现数字图书馆灯塔2.3.1 表达问题 2.3.2 求解 2.4 现实世界的应用 2.5 习题 第3 章 约束满足问题 3.1 构建约束满足问题的解决框架 3.2 澳大利亚地图着色问题 3.3 八皇后问题 3.4 单词搜索 3.5 字谜(SEND+MORE=MONEY) 3.6 电路板布局 3.7 现实世界的应用 3.8 习题 第4 章 图问题 4.1 地图就是图 4.2 搭建图的框架 4.3 查https://www.dtdjzx.gov.cn/szlib/jykj/2817585.jhtml
12.C++代码(2)八皇后问题huaxiazhihuoC++代码(2)八皇后问题 八皇后实在太有名了,我也就不废话了。利用回溯算法,不难写出其代码,相信各位同学也都干过了。那这篇文章还有何新意呢?难道是向各位展示在下的代码要比各位好,绝对不是。只因用C++写代码的时候,很容易就陷入各种细节的纠缠中,必须牢记大刀阔斧地砍除无关紧要的细节,始终坚持用C++清晰地表http://www.cppblog.com/huaxiazhihuo/archive/2011/07/13/150889.aspx
13.算法学习与应用从入门到精通2.5.1 贪心算法基础 23 2.5.2 实践演练—解决“装箱” 问题24 2.5.3 实践演练—解决 “找零方案”问题 26 2.6 试探法算法思想 27 2.6.1 试探法算法基础 27 2.6.2 实践演练—解决 “八皇后”问题 28 2.6.3 实践演练—体彩29选 7彩票组合 29 2.7 迭代算法 30 2.7.1 迭代算法基础 30 2.7.2 实践演练—http://reader.hnlib.com/Book/Detail/377965