Python Z3约束求解器解决数独问题

Z3是由Microsoft Research开发的高性能定理证明器。接下来将使用Python3中的Z3库来实现对数独问题的解决。
关于Python中Z3的使用入门，可以参考这篇博文https://blog.csdn.net/yalecaltech/article/details/90575076

问题分析

数独问题就是在一个9×99\times 99×9的格网的每个格子中填入0~9九个数字之一，使得每一行、每一列、每一宫（将整个盘面均分为9个3×33\times 33×3的九宫格，即为九个宫）中的数都不重复。记AijA_{ij}Aij为第iii行第jjj列的数，本问题的约束条件就是
∀i∀j∀k(i≠k∧j≠k→(Aij≠Aik)∧(Aij≠Akj))\forall i\forall j\forall k(i\neq k\land j\neq k\rightarrow(A_{ij}\neq A_{ik})\land(A_{ij}\neq A_{kj}))∀i∀j∀k(i=k∧j=k→(Aij=Aik)∧(Aij=Akj))
∀i∀j∀m∀n(((1≤i,m≤3)∨(4≤i,m≤6)∨(7≤i,m≤9))∧((1≤j,n≤3)∨(4≤j,n≤6)∨(7≤j,n≤9))∧(i≠m∨j≠n)→(Aij≠Amn))\forall i\forall j \forall m\forall n(((1\le i,m\le 3)\lor(4\le i,m\le 6)\lor(7\le i,m\le9))\land ((1\le j,n\le 3)\lor(4\le j,n\le 6)\lor(7\le j,n\le9))\land(i\neq m\lor j\neq n)\rightarrow(A_{ij}\neq A_{mn}))∀i∀j∀m∀n(((1≤i,m≤3)∨(4≤i,m≤6)∨(7≤i,m≤9))∧((1≤j,n≤3)∨(4≤j,n≤6)∨(7≤j,n≤9))∧(i=m∨j=n)→(Aij=Amn))

最初格子内的提示数因不能更改也应该作为约束条件加入求解器中。

完整代码如下：

from z3 import *# 约束变元数组，变元名为a_行_列
arr=[[Int('a_%d_%d'%(i+1,j+1)) for i in range(9)] for j in range(9)] # 初始条件，数字表示提示数，0表示未填入
problem=((0,2,9,0,0,0,4,0,0),(0,0,0,5,0,0,1,0,0),(0,4,0,0,0,0,0,0,0),(0,0,0,0,4,2,0,0,0),(6,0,0,0,0,0,0,7,0),(5,0,2,0,0,0,0,0,0),(7,0,0,3,0,0,0,0,5),(0,1,0,0,9,0,0,0,0),(0,0,0,0,0,0,0,6,0))# 数独规则约束
Sudoku=[And(arr[i][j]>0,arr[i][j]<10) for i in range(9) for j in range(9)]      # 数字为1~9的整数
for i in range(9):for j in range(1,9):for k in range(j):Sudoku+=[And(arr[i][j]!=arr[i][k],arr[j][i]!=arr[k][i])]        # 任一行各数两两不能相同，任一列各数两不能相同
d=[(v,h) for v in [-1,0,1] for h in [-1,0,1]]                                   # 小九宫格中各格相对中心格的偏移
for i in [1,4,7]:for j in [1,4,7]:for k in range(1,9):for l in range(k):Sudoku+=[arr[i+d[k][0]][j+d[k][1]]!=arr[i+d[l][0]][j+d[l][1]]]  # 九宫格中数两两不能相同def SolveSudoku(board):"""使用Z3约束求解器求解数独，若有解，返回表示可行解的9*9列表；若无解返回None"""global Sudoku,arrfor i in range(9):for j in range(9):if board[i][j]!=0:Sudoku+=[arr[i][j]==board[i][j]]                                # 将初始数字作为约束条件添加s=Solver()s.add(Sudoku)if s.check():                                                               # 检查是否有解m=s.model()                                                             # 获取解的模型res=[[m[arr[i][j]] for j in range(9)] for i in range(9)]                # 生成可行解的列表return reselse:return None                                                             # 无解返回None# 按行打印结果
for i in SolveSudoku(problem):print(i)

这里关于每个宫中的约束使用了一个常用技巧，通过偏移数组d将二维的区域变得可以一维遍历

代码运行结果如下

Python Z3约束求解器解决数独问题相关推荐

【python环境下Z3约束求解器学习笔记】And和Or的用法
在Z3约束求解器中,我们可能需要寻找同时满足两个条件的模型,也可能需要寻找满足两个条件中一个条件的模型,这个时候,我们可以借助And方法和Or方法来实现引入我们先来举一个简单的例子当我们想要查找 ...
re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器
推荐肉丝r0ysue课程(包含安卓逆向与js逆向): 新手一枚,如有错误(不足)请指正,谢谢!! 个人博客:点击进入题目链接:[GUET-CTF2019]re 题目下载:点击下载 IDA64位载入 ...
“芯”自主，更安全。国产三维云CAD:CrownCAD完全自主知识产权三维几何建模内核、约束求解器。
CAD软件是产品创新的工具,是研发设计师不可或缺的必备软件,它解放设计师的双手和大脑,将设计师精力更多地集中于设计和创新上.在长期的使用过程中,设计师用户既是CAD技术的受益者,也是CAD技术的历史创 ...
全自主国产PLM组件：约束求解器 ——陈立平教授就几何约束求解发表最新理论成果
2022年11月20日下午,苏州同元软控信息技术有限公司董事长.华中科技大学教授陈立平博士以"几何约束求解引擎CBA2022进展"为主题开展科研成果报告分享会,会议由上海交通大学何 ...
Matlab使用高阶求解器解决天体力学问题
使用ode78和ode89解决天体力学问题,该问题需要 ODE 求解器的每一步都具有高精度才能成功积分.和ode45都ode113无法使用默认容错来解决问题.即使使用更严格的错误阈值,ode89由于它 ...
Recurdyn和EDEM耦合报错代码C0107，找不到粒子求解器解决办法
Recurdyn中的External SPI接口已经存在,与EDEM联合仿真时报错代码C0107,找不到粒子求解器. 在系统变量新建变量,添加dll文件,变量名:SPI_PATH_EDEM,变量值:选 ...
python调用开源求解器scip求解运输问题
运输问题运输问题(transportation problem)一般是研究把某种商品从若干产地运至若干个销地而使总运费最小的一类问题.一种特殊的线性规划问题,由于其技术系数矩阵具有特殊的结构,可以使 ...
Python 调用 SCIP 求解器的选址模型代码示例
本文介绍 Python 语言调用 SCIP 求解器,求解选址模型的代码示例. 安装 SCIP 和 PySCIPOpt 安装 SCIP 求解器的教程: SCIP | 数学规划求解器SCIP超详细的使用教 ...
python调用开源求解器SCIP求解带时间窗车辆路径问题（VRPTW）
文章目录 1. 问题定义 2. 数学模型 3. python调用SCIP实现代码 4. 结果参考文献 1. 问题定义带时间窗车辆路径问题(vehicle routing problem with ...

Python Z3约束求解器解决数独问题

问题分析

Python Z3约束求解器解决数独问题相关推荐

最新文章

热门文章