sat求解器解哈密顿回路

资料：https://ozanerdem.github.io/jekyll/update/2019/11/17/representation-in-sat.html

https://modref.github.io/papers/ModRef2019_In%20Pursuit%20of%20an%20Efficient%20SAT%20Encoding%20for%20the%20Hamiltonian%20Cycle%20Problem.pdf

https://pysathq.github.io/

from pysat.solvers import Glucose3vertices_number=4   #顶点的数量
edges_number=3      #边的数量
str=input()
vertices_number,edges_number=str.split()
vertices_number=eval(vertices_number)
edges_number=eval(edges_number)check_edges=[0]*(vertices_number*vertices_number+1)#读入数据
for i in range(edges_number):num=input()num1,num2=num.split(' ')num1=eval(num1)num2=eval(num2)check_edges[(num1-1)*vertices_number+num2]=1check_edges[(num2-1)*vertices_number+num1]=1g=Glucose3()    #求解器的创建#解决重复出现的问题
for i in range(0,vertices_number):    g.add_clause([-(i*vertices_number+i+1)])for i in range(vertices_number):for j in range(vertices_number):for k in range(vertices_number):if(j!=k):g.add_clause([-(i*vertices_number+j+1),-(i*vertices_number+k+1)])for i in range(0,vertices_number):for j in range(0,vertices_number):g.add_clause([-(i*vertices_number+1+j),-(j*vertices_number+1+i)])#为每一步强制选择至少一个边缘
for i in range(vertices_number):ls=list()for j in range(vertices_number):ls.append(i*vertices_number+1+j)g.add_clause(ls)#强制访问每个顶点
for i in range(vertices_number):ls=list()for j in range(vertices_number):ls+=[j*vertices_number+1+i]g.add_clause(ls)#强制路径由真实边缘组成
for i in range(1,vertices_number*vertices_number+1):if check_edges[i]!=1:g.add_clause([-i])g.solve()
if g.solve==False:print('NO')flag=0while g.solve()==True:ans=[0]ans+=list(g.get_model())now=0the_ans=[1]for i in range(1,vertices_number+1):if(ans[i]==i):now=ithe_ans+=[now]while(True):if(ans[(now-1)*vertices_number+1]==(now-1)*vertices_number+1):breakfor i in range(vertices_number):if(ans[(now-1)*vertices_number+1+i]==(now-1)*vertices_number+1+i):now=i+1the_ans+=[now]breakls=list()for i in range(1,vertices_number*vertices_number+1):if ans[i]==i:ls+=[-i]g.add_clause(ls)if len(the_ans)!=vertices_number:continue;else:flag=1for i in range(vertices_number):print(the_ans[i],end=' ')print(1)if flag==0:print('NO')

sat求解器解哈密顿回路相关推荐

从零开始编写SAT求解器（一）
从零开始编写SAT求解器(一) 从零开始编写SAT求解器(一) 源起背景知识 SAT问题 DIMACS文件 DPLL算法项目架构从零开始编写SAT求解器(一) 源起最近在github上看到了非 ...
windows下编译以及运行cryptominisat 求解器（sat求解器）
cryptominisat是由msoos所开发的一款sat求解器,sat的具体问题另外一篇博客里有详细介绍点击打开链接,本篇文章只介绍如何在windows下运行cryptominisat,将自己遇到的 ...
求解器解的最优性 | cplex、gurobi和COPT求解器求解出来的一定是最优解吗？有理论证明吗？
求解器解的最优性 | cplex.gurobi和COPT求解器求解出来的一定是最优解吗?有理论证明吗? 作者: 刘兴禄,清华大学,清华-伯克利深圳学院博士在读欢迎关注我们的微信公众号运小筹之前有 ...
基于DPLL的SAT求解器
SAT问题什么是SAT问题? SAT问题即命题逻辑公式的可满足性问题(satisfiability problem),是计算机科学与人工智能基本问题,是一个典型的NP完全问题. 对于任一布尔变元x, ...
2-2 组合优化问题-常用模型与通用求解器
组合优化问题常用模型组合优化问题常常难以求解,我们可以把这些转化为目前已经有成熟求解器的模型. 1. 可满足性问题(Satisfiability, SAT) 上一节已经讲过,SAT 是一个 NPC ...
关于求解微分方程——初学Matlab里的 ODE求解器
学习背景最近想挖掘一下自己项目的理论深度,于是找到了老师.在老师的建议下,我们开始了漫长的研读老师的论文的旅程(论文名:Optimal Design of Adaptive Robust Contr ...
Flow Free solver[连线游戏求解器]
Fast automated solver for Flow Free puzzles written in C. 用C语言编写的连线游戏的快速自动求解器. GIF of the final pro ...
线性规划整数规划求解器SCIP的失败使用与 GLPK的成功使用
因本人科研需要,需要使用这两个求解器解数学模型. 本人的实现平台为window10,64位,基于C++,且之前已安装Visual Studio 2015. 但是SCIP的使用建议使用Linux,感觉可 ...
斗地主残局破解算法，斗地主残局暴力求解器算法，秒解各种斗地主残局
斗地主残局破解,斗地主残局暴力求解器,秒解各种斗地主残局秒解抖音.微信等各大平台的斗地主残局挑战支持自定义出牌规则输入双方的牌后单击"开始求解"按钮即可求解完成后,电脑会自 ...

sat求解器解哈密顿回路

sat求解器解哈密顿回路相关推荐

最新文章

热门文章