-
-
[原创]第二题 南冥神功 z3约束求解
-
2021-5-12 13:44 5307
-
最后几分钟没提交上。
题目比较明确
迷宫问题,需要将所有0都遍历成1。然后用z3约束求解一下得到答案
table1和table2表示每个字符需要约束的结果v10和v7
1 2 3 4 5 6 7 8 9 10 11 12 | 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 = '') |
[培训]二进制漏洞攻防(第3期);满10人开班;模糊测试与工具使用二次开发;网络协议漏洞挖掘;Linux内核漏洞挖掘与利用;AOSP漏洞挖掘与利用;代码审计。
赞赏
他的文章
看原图