首页
社区
课程
招聘
[原创]第二题 南冥神功 z3约束求解
发表于: 2021-5-12 13:44 6095

[原创]第二题 南冥神功 z3约束求解

2021-5-12 13:44
6095

最后几分钟没提交上。
题目比较明确
迷宫问题,需要将所有0都遍历成1。然后用z3约束求解一下得到答案
图片描述

table1和table2表示每个字符需要约束的结果v10和v7

图片描述

 
from z3 import *
x = Int('x')
table1 = [1,3,3,1,3,3,1,0,2,0,5,5,3,5,5,1,1,1,1,3,3,2,2]
table2 = [2,4,2,2,4,2,1,1,1,0,0,4,4,0,0,2,0,2,2,4,2,3,1]
idx2 = []
for i in range(len(table1)):
    solve(5-(i+x)%6==table1[i],(i+x/6)%6==table2[i],x>=0,x<=36)
 
str = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"
idx = [16,19,0,31,4,21,10,4,31,20,14,31,26,35,28,31,12,23,16,19,0,0,23]
for i in range(len(idx)):
    print(str[idx[i]],end='')
from z3 import *
x = Int('x')
table1 = [1,3,3,1,3,3,1,0,2,0,5,5,3,5,5,1,1,1,1,3,3,2,2]
table2 = [2,4,2,2,4,2,1,1,1,0,0,4,4,0,0,2,0,2,2,4,2,3,1]

[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课

收藏
免费 2
支持
分享
最新回复 (0)
游客
登录 | 注册 方可回帖
返回
//