这是一道数独题第一次碰见想写一下wp
此题是2021moectf的题目
拖入ida看看
cheak123是关键函数
分别进去看看
cheak1 判断每一横排的数字为1-9不重复
cheak2 判断每一竖排的数字为1-9不重复
cheak3 判断九宫格里的数字为1-9且不重复
然后知道这是一道数独, 如下
box = [0x00, 0x00, 0x05, 0x00, 0x00, 0x04, 0x03, 0x06, 0x00,
0x00, 0x00, 0x00, 0x00, 0x05, 0x00, 0x00, 0x02, 0x04,
0x00, 0x04, 0x09, 0x06, 0x07, 0x00, 0x00, 0x00, 0x00,
0x01, 0x00, 0x06, 0x00, 0x02, 0x00, 0x00, 0x03, 0x00,
0x09, 0x00, 0x00, 0x07, 0x00, 0x00, 0x01, 0x00, 0x08,
0x00, 0x03, 0x00, 0x00, 0x00, 0x05, 0x00, 0x09, 0x00,
0x02, 0x00, 0x00, 0x05, 0x00, 0x07, 0x00, 0x00, 0x09,
0x07, 0x00, 0x04, 0x00, 0x00, 0x00, 0x08, 0x00, 0x00,
0x00, 0x09, 0x00, 0x00, 0x04, 0x00, 0x00, 0x00, 0x06]
可以用数独在线求解器或者z3约束器来求解
下面写个z3
from z3 import *
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
for i in range(9) ]
cells_c = [ And(1 <= X[i][j], X[i][j] <= 9)
for i in range(9) for j in range(9) ]
rows_c = [ Distinct(X[i]) for i in range(9) ]
cols_c = [ Distinct([ X[i][j] for i in range(9) ])
for j in range(9) ]
sq_c = [ Distinct([ X[3*i0 + i][3*j0 + j]
for i in range(3) for j in range(3) ])
for i0 in range(3) for j0 in range(3) ]
sudoku_c = cells_c + rows_c + cols_c + sq_c
instance = [[0x00, 0x00, 0x05, 0x00, 0x00, 0x04, 0x03, 0x06, 0x00],
[0x00, 0x00, 0x00, 0x00, 0x05, 0x00, 0x00, 0x02, 0x04],
[0x00, 0x04, 0x09, 0x06, 0x07, 0x00, 0x00, 0x00, 0x00],
[0x01, 0x00, 0x06, 0x00, 0x02, 0x00, 0x00, 0x03, 0x00],
[0x09, 0x00, 0x00, 0x07, 0x00, 0x00, 0x01, 0x00, 0x08],
[0x00, 0x03, 0x00, 0x00, 0x00, 0x05, 0x00, 0x09, 0x00],
[0x02, 0x00, 0x00, 0x05, 0x00, 0x07, 0x00, 0x00, 0x09],
[0x07, 0x00, 0x04, 0x00, 0x00, 0x00, 0x08, 0x00, 0x00],
[0x00, 0x09, 0x00, 0x00, 0x04, 0x00, 0x00, 0x00, 0x06]]
instance_c = [ If(instance[i][j] == 0,
True,
X[i][j] == instance[i][j])
for i in range(9) for j in range(9) ]
s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
for i in range(9) ]
print_matrix(r)
else:
print("failed to solve")
官网文档有可以直接白嫖,然后自己可以复现一下
得到
[[8, 2, 5, 9, 1, 4, 3, 6, 7],
[6, 7, 1, 3, 5, 8, 9, 2, 4],
[3, 4, 9, 6, 7, 2, 5, 8, 1],
[1, 8, 6, 4, 2, 9, 7, 3, 5],
[9, 5, 2, 7, 6, 3, 1, 4, 8],
[4, 3, 7, 1, 8, 5, 6, 9, 2],
[2, 6, 8, 5, 3, 7, 4, 1, 9],
[7, 1, 4, 2, 9, 6, 8, 5, 3],
[5, 9, 3, 8, 4, 1, 2, 7, 6]]
#8291767138932581849755263447186268341129653538127