封面是约束关系示意,不是一组皇后合法解;右侧九格图标不代表完整数独盘面。
AI 写回溯代码,最让人放心不下的往往不是递归能否结束,而是“得到一张填满的表”是否真等于解出了题。N 皇后需要行、列、对角线互不攻击;标准数独还多了九宫格和原题线索不能被覆盖。
下面用自包含程序分别检查它们。没有向模型发请求,也没有声称剪枝提速了多少;代码是评审用教学实现。
先看约束,再讨论少搜几个节点
N 皇后按行放置,可以通过构造保证每行一枚,再检查列差与行差。数独则按行、列、3×3 宫计算候选集合。MRV 选择候选最少的空格,属于变量排序,不能删除合法候选。Berkeley CSP 教材对此有明确解释。
本篇数独检查器与求解器分开:即使搜索返回填满的表,还要确认每个单元约束成立、原线索保持。否则“递归成功”可能只是错误终止条件。
def queens(n): if type(n) is not int or n < 1: raise ValueError("n must be positive") out = [] def dfs(cols): row = len(cols) if row == n: out.append(tuple(cols)) return for c in range(n): if all(c != old and abs(c-old) != row-r for r, old in enumerate(cols)): dfs(cols+[c]) dfs([]) return out groups = [] groups += [[9*r+c for c in range(9)] for r in range(9)] groups += [[9*r+c for r in range(9)] for c in range(9)] groups += [[9*(br+r)+bc+c for r in range(3) for c in range(3)] for br in (0,3,6) for bc in (0,3,6)] peers = [set(j for g in groups if i in g for j in g)-{i} for i in range(81)] def valid_partial(b): return (len(b) == 81 and all(type(x) is int and 0 <= x <= 9 for x in b) and all(len([b[i] for i in g if b[i]]) == len(set(b[i] for i in g if b[i])) for g in groups)) def solve(board, mrv=True): if not valid_partial(board): raise ValueError("invalid clues") b = list(board) def dfs(): empty = [i for i, v in enumerate(b) if not v] if not empty: return b[:] choices = {i: sorted(set(range(1,10))-{b[j] for j in peers[i]}) for i in empty} i = min(empty, key=lambda x: (len(choices[x]), x)) if mrv else empty[0] for value in choices[i]: b[i] = value answer = dfs() if answer is not None: return answer b[i] = 0 return None return dfs() def check_answer(clues, answer): return (answer is not None and valid_partial(answer) and 0 not in answer and all(not x or answer[i] == x for i, x in enumerate(clues))) assert [len(queens(n)) for n in range(1,9)] == [1,0,0,2,10,4,40,92] for placement in queens(8): assert len(set(placement)) == 8 assert all(abs(placement[i]-placement[j]) != j-i for i in range(8) for j in range(i+1,8)) rows = ["530070000","600195000","098000060","800060003","400803001", "700020006","060000280","000419005","000080079"] clues = [int(c) for row in rows for c in row] for mrv in (False, True): assert check_answer(clues, solve(clues, mrv)) invalid = clues[:] invalid[2] = 5 try: solve(invalid) except ValueError: pass else: raise AssertionError("duplicate clue accepted") # No duplicate givens, but first empty cell has no candidate. impossible = [0]*81 impossible[:9] = [1,2,3,4,5,6,7,8,0] impossible[17] = 9 assert valid_partial(impossible) and solve(impossible) is None print("queens 1..8, sudoku baseline/MRV, invalid and unsatisfiable checked")Python 3.9.6 隔离运行通过。数独实例的两种搜索都通过约束检查;这并没有证明该实例唯一解。若要验证唯一性,必须继续枚举到第二个解或穷尽,不能把“找到第一个”写成“唯一”。
正确性证据与速度证据各算各的
N 皇后最坏搜索仍是组合爆炸,数独回溯也是指数级搜索;MRV 不提供所有实例都更快的保证。当前实现为清晰起见,每次递归重算候选,有额外开销。没有记录节点和耗时,就不报告减少百分比。
日后比较剪枝,应固定候选值顺序和终止规则,只改变变量选择;同时保存访问节点定义、实例、解数量和运行环境。否则一个求“首解”、另一个数“全部解”,比出来的时间没有意义。
EvalPlus和 Hypothesis可作为扩大反例检查的材料,本次没有运行它们。动态文档发稿前复核。可运行证据只覆盖上面程序及有限输入,模型输出质量仍待真实对照。