从逻辑bingo开始的SAT介绍和Z3求解。
总之，我想写这个博客很久了。这个题目是25年10月份的时候做的，但是因为沉迷vibe coding导致一直都没写。今天我的周用量快给我用完了，所以来写点博客。
题目 & 解题思路
总之题目就是下面这样，是一张 5x5 的表格。每个格子里写着一句话，或者说一句断言。规则很简单：
- 如果某个格子的称述为真，那么这个格子就得打勾
- 如果某个格子的称述为假，那么这个格子就不打勾
- 最终答案必须满足bingo的条件：也就是5个勾连成一条线，不管是一整行还是一整列，或者说是一条对角线都行
虽然这个题看起来比较简单，但实际上每个格子的断言都依赖其他格子的真假，而这个格子的真假又会影响其他格子断言的真假，最后就会形成一个巨大的依赖链，大家相互依赖。
所以实际上还是有点困难的（并非困难）。
当然手动解题的思路我这里就不说了，本质上就是一个个试。其实暴力搜索也是可以的，只需要枚举2^25=33554432状态，然后对每种状态检查一下它是否满足题意就行，由于检查这个解的时间复杂度是O(1)，所以暴力破解也不会很慢。
不过这里我想说的不是暴力，而是使用SAT求解器来解这个题。因为SAT可以很好的handle上面说的相互以来的问题。
SAT 布尔可满足性问题 Boolean Satisfiability Problem
ok,那么说道这里，我们需要简单的来说说我大学上的课程(PHIL 220)中的SAT了，SAT即是Boolean Satisfiability Problem，也就是布尔可满足性问题。
布尔可满足性问题简单来说就是寻找：“是否存在一组布尔变量赋值，使得整个逻辑公式为真。”
比如我们有三个变量：A B C，以及一个逻辑公式约束:
(A or B) and (not B) and (not C)观察得知，当A = True, B = False, C = False的时候，整个公式为真，所以这个公式即是可满足的，也就是satisfiable。
但是如果我们看另外一个逻辑约束公式
A and (not A)这个就很明显了，不管A取True还是False，A和not A总有一个是假的，所以整个式子永远不可能成立。
在这种情况下，这公式就是不可满足的，即unsatisfiable。
原题 -> SAT/SMT
诶，这个时候就会有小朋友要问了：你说的这个和我们这个逻辑 bingo 题有什么关系呢？
别急，这是这道题其实很容易转化成一道SAT风格的约束问题。
为什么呐，首先每个格子的陈述只有两种状态，也就是 真 / 假。而题目又规定了打勾的条件即是格子中陈述的真假：
- 陈述为真 -> 这个格子打勾
- 陈述为假 -> 这个格子不打勾
所以我们完全可以把每个格子作为一个布尔变量进行建模。
grid[i][j] == True # True即表示改格子中的称述为真，需要打勾
grid[j][j] == False # False即表示该格子中的称述为假，不能打勾然后前面提到，每个格子的真假又依赖其他格子的打勾状态，也就是依赖其他格子的真假状态。诶，这不正好就是一个逻辑公式么。
grid[i][j] == (grid[x][y] and grid[x+1][y+1] ........)于是这个问题就变成了：“是否存在一个5x5的布尔变量矩阵，使所有的条件成立。” 而这样我们就满足了题目要求的第一条和第二条要求。
如果再加上bingo的条件，也就是
- 存在一整行都被打勾
- 或者存在一整列都被打勾
- 或者存在一条对角线都被打勾
当然严格来说，这题不算是纯SAT，因为里面还包含一部分计数和比较，比如：比如有几个勾，需要勾的总是少于12等。这些内容更准确地说属于**SMT (Satisfiability Modulo Theories)**的范畴，也就是在SAT之上再加一些整数和比较运算。
不过从思想上来说，它和SAT是一脉相承的。因为这些计数条件理论上也都可以继续展开，最后reduce成SAT - 只要把所有的情况都列出来就好了(所以其实还是SAT)。
比如在三个变量A B C里，“恰好有 2 个为真”可以写成：
(A and B and not C) or (A and not B and C) or (not A and B and C)而像“总数小于 12”这种条件，本质上也可以写成很多种情况的or，也就是把总数等于1，2,3,4...的条件全部都用or连接。只不过那样会非常啰嗦，所以实际写代码的时候我们当然不会这么干，而是直接交给支持整数约束的求解器去做。
SAT -> 求解
那么我们现在知道这个问题可以完美的转化成SAT/SMT问题了，那么下一步我们要怎么建模并求解呢。
我们都知道，SAT是一个NP-complete问题，什么是NP-complete我就不多说了。
总之我们有一个非常好用的库叫做z3，这个库是一个非常强大的SMT求解器，而且写起来非常的方便。
怎么安装我就不说了，现在大模型一搜就知道了。接下来要做的事情，就是把题目中的自然语言一句句翻译成约束条件。
约束翻译
我们首先需要建立一个5x5的布尔变量矩阵。
其中
grid[i][j] == True表示第 i+1 行第 j+1 列被打勾grid[i][j] == False表示第 i+1 行第 j+1 列这个格子不打勾
from z3 import *
solver = Solver()
grid = [[Bool(f"cell_{i}_{j}") for j in range(5)] for i in range(5)]辅助函数: 打勾的个数
Z3 里的布尔值不能直接相加，所以我们通常写一个辅助函数：
def count_true(vars):
return Sum([If(v, 1, 0) for v in vars])例如整张表里打勾格子的总数，可以转化为：
total_true = count_true([grid[i][j] for i in range(5) for j in range(5)])某一行和某一列的个数，可以转化为
def count_row(i):
return count_true([grid[i][j] for j in range(5)])
def count_col(j):
return count_true([grid[i][j] for i in range(5)])辅助函数： 某个格子的邻居
题目里很多条件跟“周围格子”有关，所以可以写一个helper函数来简化:
def moore_neighbors(i, j):
neighbors = []
for di in [-1, 0, 1]:
for dj in [-1, 0, 1]:
if di == 0 and dj == 0:
continue
ni = i + di
nj = j + dj
if 0 <= ni < 5 and 0 <= nj < 5:
neighbors.append(grid[ni][nj])
return neighbors定义bingo
后面有几个格子的断言直接和“是不是一整行 / 一整列 / 对角线”有关，且判断bingo也需要这几个条件，所以这里先把这几个条件定义出来：
full_rows = [And([grid[i][j] for j in range(5)]) for i in range(5)]
full_cols = [And([grid[i][j] for i in range(5)]) for j in range(5)]
full_diag1 = And([grid[i][i] for i in range(5)])
full_diag2 = And([grid[i][4 - i] for i in range(5)])
has_full_row = Or(full_rows)
has_full_col = Or(full_cols)
has_full_diag = Or(full_diag1, full_diag2)开始翻译
总之前面提到了，某个格子是否打勾，就是该格子的陈述是否为真。
也就是
solver.add(grid[i][j] == xxxxx)知道了这个方式就可以正式开始翻译了。
第 1 行第 1 列：这个格子应该打勾
这个格子说的是“我这个格子应该打勾”。那它本身就等价于真，也就是直接把它设成 True。
solver.add(grid[0][0] == True)第 1 行第 2 列：整张表打勾的格子个数 ≤ 12
前面已经有 total_true 了，所以直接写：
solver.add(grid[0][1] == (total_true <= 12))第 1 行第 3 列：第 2 列打勾格子数量小于第 3 列
这个就是直接比较第 2 列和第 3 列的打勾数量：
solver.add(grid[0][2] == (count_col(1) < count_col(2)))第 1 行第 4 列：这一格所在行打勾格子数量小于所在列
这个格子在第1行第4 ，所以它说的所在行就是第 1 行，所在列就是第 4 列，因此翻译成：
solver.add(grid[0][3] == (count_row(0) < count_col(3)))第 1 行第 5 列：答案中 5 个连成一线的格子是一整列
前面已经定义过 has_full_col 了，所以直接写：
solver.add(grid[0][4] == has_full_col)第 2 行第 1 列：这个格子周围 5 格中打勾的格子个数是奇数
solver.add(grid[1][0] == (count_true(moore_neighbors(1, 0)) % 2 == 1))第 2 行第 2 列：整张表打勾的格子个数 ≥ 13
solver.add(grid[1][1] == (total_true >= 13))第 2 行第 3 列：不存在周围格子均未被打勾的格子
也可以翻译成：对于每个格子来说，它周围至少有一个格子被打勾
所以可以写成：对所有格子 (i, j)，moore_neighbors(i, j) 里至少有一个是真的。
这里的 Or(moore_neighbors(i, j)) 表示这个格子的邻居里至少有一个被打勾。再对全部格子做一个 And，就表示“每个格子都满足这个条件”。
solver.add(grid[1][2] == And([Or(moore_neighbors(i, j)) for i in range(5) for j in range(5)]))第 2 行第 4 列：表格四个角上的格子恰有 2 个打勾
四个角分别是：左上(0,0)，右上(0,4)，左下(4,0)，右下(4,4)
所以先把它们取出来，然后查看个数
corners = [grid[0][0], grid[0][4], grid[4][0], grid[4][4]]
solver.add(grid[1][3] == (count_true(corners) == 2))第 2 行第 5 列：答案中 5 个连成一线的格子是一整行
和前面“是一整列”一样，直接使用 has_full_row：
solver.add(grid[1][4] == has_full_row)第 3 行第 1 列：中心格被打勾
中心格就是整个 5x5 的正中间，也就是第 3 行第 3 列，对应下标 (2, 2)。
所以这个格子说的就是：grid[2][2] == True。而“这个格子为真”就意味着它和 grid[2][2] 的真假一致，因此可以直接写成：
solver.add(grid[2][0] == grid[2][2])第 3 行第 2 列：左上角的九宫格有 ≥ 5 个格子打勾
“左上角的九宫格”就是左上角那个 3x3 区域，也就是坐标 (0..2, 0..2)。
先把这些格子取出来，然后判断是否数量大于5即可：
top_left_3x3 = [grid[i][j] for i in range(3) for j in range(3)]
solver.add(grid[2][1] == (count_true(top_left_3x3) >= 5))第 3 行第 3 列：不存在上下相邻且均被打勾的两个格子
这句话也可以翻译成：对于所有竖直相邻的两个格子，不允许它们同时被打勾
所以可以枚举所有 (i, j) 和它正下方 (i+1, j) 的配对，然后要求每一对都不能同时为真：
no_vertical_adjacent_true = And([
Not(And(grid[i][j], grid[i + 1][j]))
for i in range(4) for j in range(5)
])
solver.add(grid[2][2] == no_vertical_adjacent_true)这里 i 只需要到 3，因为再往下就没有下一行了。
第 3 行第 4 列：不存在上下左右均勾但自身不勾的格子
这句读起来比较绕，但是实际上他的意思就是: 不存在某个格子，它的上、下、左、右都被打勾了，但是它自己没打勾
也就等价于：对每个内部格子，如果它的上、下、左、右都被打勾，那么它自己也必须被打勾
所以可以写成很多个Implies：
cross_conditions = []
for i in range(1, 4):
for j in range(1, 4):
cross_conditions.append(
Implies(
And(grid[i - 1][j], grid[i + 1][j], grid[i][j - 1], grid[i][j + 1]),
grid[i][j]
)
)
solver.add(grid[2][3] == And(cross_conditions))这里只枚举内部格子，是因为边界格子没有完整的上下左右四个方向。
第 3 行第 5 列：答案中 5 个连成一线的格子是斜对角线
这里对应的就是“存在一条对角线被完全打勾”，所以直接使用 has_full_diag：
solver.add(grid[2][4] == has_full_diag)第 4 行第 1 列：存在某个格子周围打勾格子数量 ≥ 7
这句的意思是：至少存在一个格子，它周围邻居里被打勾的数量大于等于7
所以直接把所有格子都枚举一遍，只要有一个满足就行：
solver.add(grid[3][0] == Or([
count_true(moore_neighbors(i, j)) >= 7
for i in range(5) for j in range(5)
]))第 4 行第 2 列：这一格所在行打勾格子数量小于所在列
这个格子在第4行第2列，所以它说的是：第4行打勾数小于第2列打勾数
翻译成：
solver.add(grid[3][1] == (count_row(3) < count_col(1)))第 4 行第 3 列：存在 4 个格子均被打勾的 2×2 正方形
这个就是看整个5x5里有没有某个2x2小方块全为真。
一个5x5里一共有4 x 4 = 16个可能的2x2正方形，所以枚举一下全部加上：
solver.add(grid[3][2] == Or([
And(grid[i][j], grid[i][j + 1], grid[i + 1][j], grid[i + 1][j + 1])
for i in range(4) for j in range(4)
]))第 4 行第 4 列：这个格子周围 8 格中打勾的格子数量是偶数
solver.add(grid[3][3] == (count_true(moore_neighbors(3, 3)) % 2 == 0))第 4 行第 5 列：请先将这个格子打勾
这个其实没什么好说的，直接打勾就完事了：
solver.add(grid[3][4] == True)第 5 行第 1 列：第 5 列打勾格子数量小于 3
solver.add(grid[4][0] == (count_col(4) < 3))第 5 行第 2 列：第 2 列打勾格子数量大于 3
solver.add(grid[4][1] == (count_col(1) > 3))第 5 行第 3 列：第 1 列打勾格子数量大于 3
solver.add(grid[4][2] == (count_col(0) > 3))第 5 行第 4 列：第 3 列打勾格子数量在所有列中最小
这句话的意思是：第 3 列的打勾数量小于等于其他每一列
也就是对所有列 k 都满足：
count_col(2) <= count_col(k)即
solver.add(grid[4][3] == And([count_col(2) <= count_col(k) for k in range(5)]))这里用的是“小于等于”，也就是允许并列最小。如果你想解释成“严格最小”，那就得改成 < 并额外处理。不过从中文语义上看，“最小”通常写成 <= 是比较自然的。
第 5 行第 5 列：存在一整行或一整列没有打勾的格子
这句就是在说：存在某一整行全都没打勾 或者 存在某一整列全都没打勾
full_false_rows = [And([Not(grid[i][j]) for j in range(5)]) for i in range(5)]
full_false_cols = [And([Not(grid[i][j]) for i in range(5)]) for j in range(5)]
solver.add(grid[4][4] == Or(Or(full_false_rows), Or(full_false_cols)))最后补上必须形成 Bingo
除了每个格子的文字断言，我们还必须把题目本身的全局条件也加进去。也就是最终答案必须至少形成一条Bingo线：
solver.add(Or(has_full_row, has_full_col, has_full_diag))求解
到这里整个题目就已经被翻译成一套完整的约束了，直接运行我们可以非常快的得到答案。
(ctfenv)00:13:56 $ python solver.py
solution #0 in 0.008947 seconds
X O O X O
X X X X X
O X O X O
O X O O X
X O O X O
solution #1 in 0.004438 seconds
X O O X O
X X X X X
O X O X O
O X O O X
X X O X O怎么枚举所有解
顺便说一下，Z3 不只是可以找一个解，也可以把所有解都枚举出来，思路很简单：
- 先让solver找到一个解
- 添加一条约束，要求下一个解至少有一个格子与当前的解不同
- 重复
就好了
一些想说的
没啥好总结的，写这个博客的主要原因就是找到一个很好的例子可以让我记录一边sat问题和z3求解器。但是还是写点别的什么东西吧：
总之我当时做这道题的时候，我尝试了多个AI，包括但不限于chatgpt, gemini, claude, deepseek, qwen。结果愣是没有一个ai就能解出来的，甚至连“可以往sat求解这个方向去建模”都没有想到。
而我当时第一时间就把这题和sat求解关联上，并顺利的解出了答案。当时我还沾沾自喜，哈哈，看起来ai还是没有我聪明啊。
然后没想到，才过去一年不到，我刚刚尝试了一下chatgpt，chatgpt已经能够很快的想到使用sat去求解了，整个过程甚至只用了3分钟不到。
有时我真的想啊，如果AI总能这么快的帮我解决问题，那我是否还会不会愿意自己去认真思考思考？是否还会像以前一样，xian在自己大脑里思考，建模，分析问题，再一步步把答案找出来。
我感觉不止是我，很多人现在遇到问题的第一反应已经不是自己想，而是直接把问题丢给ai，先看看ai能不能帮我解决问题。AI把原来需要一天去思考去完成的事情，压缩到了1分钟，半分钟，甚至于1秒钟。面对一个能够很快解决问题的方案，我们是否还能静下心来，认真的理解问题，思考解法，然后去享受问题最终解决的那一个时刻？还是说我们会越来越习惯与直接索取答案，最终失去独立思考的耐心，甚至是能力？
我不知道。
也许真正的问题是当思考变得不再必要时，我们是否还会主动选择思考，主动选择这个带领我们人类从原始走向现代的能力。
希望我们所有人都能正确使用AI，而不是成为AI的奴隶。
Reference
完整代码
import time
from z3 import *
solver = Solver()
grid = [[Bool(f"cell_{i}_{j}") for j in range(5)] for i in range(5)]
def count_true(vars):
return Sum([If(v, 1, 0) for v in vars])
def count_row(i):
return count_true([grid[i][j] for j in range(5)])
def count_col(j):
return count_true([grid[i][j] for i in range(5)])
def moore_neighbors(i, j):
neighbors = []
for di in [-1, 0, 1]:
for dj in [-1, 0, 1]:
if di == 0 and dj == 0:
continue
ni = i + di
nj = j + dj
if 0 <= ni < 5 and 0 <= nj < 5:
neighbors.append(grid[ni][nj])
return neighbors
total_true = count_true([grid[i][j] for i in range(5) for j in range(5)])
# Bingo 相关
full_rows = [And([grid[i][j] for j in range(5)]) for i in range(5)]
full_cols = [And([grid[i][j] for i in range(5)]) for j in range(5)]
full_diag1 = And([grid[i][i] for i in range(5)])
full_diag2 = And([grid[i][4 - i] for i in range(5)])
has_full_row = Or(full_rows)
has_full_col = Or(full_cols)
has_full_diag = Or(full_diag1, full_diag2)
# 第1行
solver.add(grid[0][0] == True)
solver.add(grid[0][1] == (total_true <= 12))
solver.add(grid[0][2] == (count_col(1) < count_col(2)))
solver.add(grid[0][3] == (count_row(0) < count_col(3)))
solver.add(grid[0][4] == has_full_col)
# 第2行
solver.add(grid[1][0] == (count_true(moore_neighbors(1, 0)) % 2 == 1))
solver.add(grid[1][1] == (total_true >= 13))
solver.add(grid[1][2] == And([Or(moore_neighbors(i, j)) for i in range(5) for j in range(5)]))
corners = [grid[0][0], grid[0][4], grid[4][0], grid[4][4]]
solver.add(grid[1][3] == (count_true(corners) == 2))
solver.add(grid[1][4] == has_full_row)
# 第3行
solver.add(grid[2][0] == grid[2][2]) # “中心格被打勾”
top_left_3x3 = [grid[i][j] for i in range(3) for j in range(3)]
solver.add(grid[2][1] == (count_true(top_left_3x3) >= 5))
no_vertical_adjacent_true = And([
Not(And(grid[i][j], grid[i + 1][j]))
for i in range(4) for j in range(5)
])
solver.add(grid[2][2] == no_vertical_adjacent_true)
cross_conditions = []
for i in range(1, 4):
for j in range(1, 4):
cross_conditions.append(
Implies(
And(grid[i - 1][j], grid[i + 1][j], grid[i][j - 1], grid[i][j + 1]),
grid[i][j]
)
)
solver.add(grid[2][3] == And(cross_conditions))
solver.add(grid[2][4] == has_full_diag)
# 第4行
solver.add(grid[3][0] == Or([
count_true(moore_neighbors(i, j)) >= 7
for i in range(5) for j in range(5)
]))
solver.add(grid[3][1] == (count_row(3) < count_col(1)))
solver.add(grid[3][2] == Or([
And(grid[i][j], grid[i][j + 1], grid[i + 1][j], grid[i + 1][j + 1])
for i in range(4) for j in range(4)
]))
solver.add(grid[3][3] == (count_true(moore_neighbors(3, 3)) % 2 == 0))
solver.add(grid[3][4] == True)
# 第5行
solver.add(grid[4][0] == (count_col(4) < 3))
solver.add(grid[4][1] == (count_col(1) > 3))
solver.add(grid[4][2] == (count_col(0) > 3))
solver.add(grid[4][3] == And([count_col(2) <= count_col(k) for k in range(5)]))
full_false_rows = [And([Not(grid[i][j]) for j in range(5)]) for i in range(5)]
full_false_cols = [And([Not(grid[i][j]) for i in range(5)]) for j in range(5)]
solver.add(grid[4][4] == Or(Or(full_false_rows), Or(full_false_cols)))
# 必须形成 Bingo
solver.add(Or(has_full_row, has_full_col, has_full_diag))
def print_model(model):
result = []
for i in range(5):
row = []
for j in range(5):
row.append('X' if is_true(model.evaluate(grid[i][j])) else 'O')
result.append(row)
for row in result:
print(' '.join(row))
print()
def find_one():
t1 = time.time()
if solver.check() == sat:
print("solved in", time.time() - t1, "seconds")
print_model(solver.model())
else:
print("unsat")
def find_all():
idx = 0
t1 = time.time()
while solver.check() == sat:
t2 = time.time()
model = solver.model()
print(f"solution #{idx} in {t2 - t1:.6f} seconds")
print_model(model)
block_constraint = Or([
grid[i][j] != model.evaluate(grid[i][j])
for i in range(5) for j in range(5)
])
solver.add(block_constraint)
idx += 1
t1 = time.time()
if __name__ == "__main__":
find_all()题目 As Text
| \ | 第1列 | 第2列 | 第3列 | 第4列 | 第5列 |
|---|---|---|---|---|---|
| 第1行 | 这个格子应该打勾 | 整张表打勾的格子个数≤12 | 第2列打勾格子数量小于第3列 | 这一格所在行打勾格子数量小于所在列 | 答案中5个连成一线的格子是一整列 |
| 第2行 | 这个格子周围5格中打勾的格子个数是奇数 | 整张表打勾的格子个数≥13 | 不存在周围格子均未被打勾的格子 | 表格四个角上的格子恰有2个打勾 | 答案中5个连成一线的格子是一整行 |
| 第3行 | 中心格被打勾 | 左上角的九宫格有≥5个格子打勾 | 不存在上下相邻且均被打勾的两个格子 | 不存在上下左右均勾但自身不勾的格子 | 答案中5个连成一线的格子是斜对角线 |
| 第4行 | 存在某个格子周围打勾格子数量≥7 | 这一格所在行打勾格子数量小于所在列 | 存在4个格子均被打勾的2×2正方形 | 这个格子周围8格中打勾的格子数量是偶数 | 请先将这个格子打勾 |
| 第5行 | 第5列打勾格子数量小于3 | 第2列打勾格子数量大于3 | 第1列打勾格子数量大于3 | 第3列打勾格子数量在所有列中最小 | 存在一整行或一整列没有打勾的格子 |