为啥叫英雄救美？？？？全程没看到美女
sub_391240 对输入数据进行转换
这个函数有点小坑.....
$B$BP => 12123
sub_391000 9x9 数独 check
数独输出如下
用 z3 脚本解一下数独
得到结果
反推输入
table1 = [0x24, 0x42, 0x50, 0x56, 0x3A, 0x75, 0x62, 0x66, 0x59, 0x70, 0x7D, 0x5D, 0x44, 0x74, 0x4E, 0x3E, 0x61, 0x54, 0x5E, 0x4D, 0x47, 0x6D, 0x4A, 0x51, 0x23, 0x2A, 0x48, 0x72, 0x60, 0x4F, 0x27, 0x77, 0x6A, 0x69, 0x63, 0x30, 0x21, 0x68, 0x64, 0x79, 0x7B, 0x6F, 0x5A, 0x7A, 0x2D, 0x40, 0x6E, 0x2B, 0x3F, 0x26, 0x25, 0x73, 0x5F, 0x2F, 0x67, 0x3C, 0x65, 0x5B, 0x57, 0x29, 0x58, 0x55, 0x78, 0x52, 0x46, 0x53, 0x4C, 0x52, 0x41, 0x3B, 0x2E, 0x6C, 0x3D, 0x43, 0x45, 0x6B, 0x76, 0x4B, 0x2D, 0x28, 0x71]
table1 = [0x24, 0x42, 0x50, 0x56, 0x3A, 0x75, 0x62, 0x66, 0x59, 0x70, 0x7D, 0x5D, 0x44, 0x74, 0x4E, 0x3E, 0x61, 0x54, 0x5E, 0x4D, 0x47, 0x6D, 0x4A, 0x51, 0x23, 0x2A, 0x48, 0x72, 0x60, 0x4F, 0x27, 0x77, 0x6A, 0x69, 0x63, 0x30, 0x21, 0x68, 0x64, 0x79, 0x7B, 0x6F, 0x5A, 0x7A, 0x2D, 0x40, 0x6E, 0x2B, 0x3F, 0x26, 0x25, 0x73, 0x5F, 0x2F, 0x67, 0x3C, 0x65, 0x5B, 0x57, 0x29, 0x58, 0x55, 0x78, 0x52, 0x46, 0x53, 0x4C, 0x52, 0x41, 0x3B, 0x2E, 0x6C, 0x3D, 0x43, 0x45, 0x6B, 0x76, 0x4B, 0x2D, 0x28, 0x71]
map1 = [0x00000000, 0x00000004, 0x00000000, 0x00000007, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000009, 0x00000002, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000006, 0x00000000, 0x00000007, 0x00000008, 0x00000003, 0x00000000, 0x00000000, 0x00000000, 0x00000005, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000001, 0x00000000, 0x00000000, 0x00000000, 0x00000003, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000002, 0x00000000, 0x00000001, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000005, 0x00000000, 0x00000000, 0x00000000, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000004, 0x00000009, 0x00000000, 0x00000000, 0x00000000, 0x00000007, 0x00000001, 0x00000003, 0x00000000, 0x00000005, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000009, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000008, 0x00000000, 0x00000006, 0x00000000]
mat = []
for y in range(9):
line = list()
for x in range(9):
line.append(map1[y * 9 + x])
mat.append(line)
map1 = [0x00000000, 0x00000004, 0x00000000, 0x00000007, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000009, 0x00000002, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000006, 0x00000000, 0x00000007, 0x00000008, 0x00000003, 0x00000000, 0x00000000, 0x00000000, 0x00000005, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000001, 0x00000000, 0x00000000, 0x00000000, 0x00000003, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000002, 0x00000000, 0x00000001, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000005, 0x00000000, 0x00000000, 0x00000000, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000004, 0x00000009, 0x00000000, 0x00000000, 0x00000000, 0x00000007, 0x00000001, 0x00000003, 0x00000000, 0x00000005, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000009, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000008, 0x00000000, 0x00000006, 0x00000000]
mat = []
for y in range(9):
line = list()
for x in range(9):
line.append(map1[y * 9 + x])
mat.append(line)
0 4 0 7 0 0 0 0 0
9 2 0 0 0 0 6 0 7
8 3 0 0 0 5 4 0 0
0 1 0 0 0 3 0 0 0
0 0 0 2 0 1 0 0 0
0 0 0 5 0 0 0 4 0
0 0 4 9 0 0 0 7 1
3 0 5 0 0 0 0 9 4
0 0 0 0 0 8 0 6 0
0 4 0 7 0 0 0 0 0
9 2 0 0 0 0 6 0 7
8 3 0 0 0 5 4 0 0
0 1 0 0 0 3 0 0 0
0 0 0 2 0 1 0 0 0
0 0 0 5 0 0 0 4 0
0 0 4 9 0 0 0 7 1
3 0 5 0 0 0 0 9 4
0 0 0 0 0 8 0 6 0
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 = [[0, 4, 0, 7, 0, 0, 0, 0, 0],
[9, 2, 0, 0, 0, 0, 6, 0, 7],
[8, 3, 0, 0, 0, 5, 4, 0, 0],
[0, 1, 0, 0, 0, 3, 0, 0, 0],
[0, 0, 0, 2, 0, 1, 0, 0, 0],
[0, 0, 0, 5, 0, 0, 0, 4, 0],
[0, 0, 4, 9, 0, 0, 0, 7, 1],
[3, 0, 5, 0, 0, 0, 0, 9, 4],
[0, 0, 0, 0, 0, 8, 0, 6, 0]]
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")
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 = [[0, 4, 0, 7, 0, 0, 0, 0, 0],
[9, 2, 0, 0, 0, 0, 6, 0, 7],
[8, 3, 0, 0, 0, 5, 4, 0, 0],
[0, 1, 0, 0, 0, 3, 0, 0, 0],
[0, 0, 0, 2, 0, 1, 0, 0, 0],
[0, 0, 0, 5, 0, 0, 0, 4, 0],
[招生]科锐逆向工程师培训(2024年11月15日实地，远程教学同时开班, 第51期)
