這是一道數獨題第一次碰見想寫一下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_cinstance = [[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

總結

以上是生活随笔為你收集整理的moectf chall 数独题 z3约束器求解的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。