Chapter 2. Interlude: The Eight-Queen Puzzle

用八皇后完整程序训练Lua table状态、1-based索引、局部函数、递归回溯、冲突不变量、解输出与确定性回归证据。

从完整程序开始检验第一章基础

第四版把Eight-Queen Puzzle放在Getting Started之后，是有意让读者先看到一个短而完整的Lua程序。棋盘有8行8列，要放8个皇后，使任意两个不共享row、column或diagonal。我们固定“第row行只放一个queen”，于是state只需table board[row] = column；row冲突被表示法消除，搜索只检查column和diagonal。

先预测：是否需要复制完整board才能尝试每个candidate；board[row]在递归返回后必须设nil吗；为什么只检查之前rows就够；打印函数若把board保存到列表会发生什么；N=8应该输出多少解。答案依赖state owner与不变量，而不是递归语法本身。

是整段程序的证明核心。每次进入search(row)都假设prefix安全；只把通过predicate的candidate加入prefix；child返回后当前层继续尝试，因此归纳地不会探索非法prefix。

Representing and testing board configurations：用Table表示Board

Lua sequence从1开始，非常适合让row 1..N直接作为key。Value是column number；尚未放置的row为nil。Table是mutable reference，所有recursive activations共享同一board，因此必须明确每层只写自己的board[row]。Previous rows由ancestors拥有，future rows不应参与validity。

local function new_board(size)
  local board = {}
  for row = 1, size do
    board[row] = nil
  end
  return board
end
 
local board = new_board(8)
assert(board[1] == nil and #board == 0)

显式写nil只是教学，空table已没有keys。注意#board在partial/sparse state上不是“已放queen数量”的可靠定义；递归row参数才是进度source of truth。搜索结束后若清理每层slot，board又成为empty table；若只覆盖，旧future slot可能残留并误导printer，所以termination/emission只读取1..N，或return时清理。

冲突公式：Column与两条Diagonal

已放queen (priorRow, priorColumn)与candidate (row, column)冲突条件：同列 priorColumn == column；同一descending diagonal时 priorColumn - priorRow == column - row；同一ascending diagonal时 priorColumn + priorRow == column + row。等价写法是absolute column distance等于row distance。

应只读safe prefix并返回boolean，不修改board。它遍历1 .. row-1，因为future rows不存在，current row也尚未commit。

local function is_place_ok(board, row, column)
  for prior_row = 1, row - 1 do
    local prior_column = board[prior_row]
    if prior_column == column
      or prior_column - prior_row == column - row
      or prior_column + prior_row == column + row then
      return false
    end
  end
  return true
end

A complete recursive backtracking Lua program：Choice Point与State Ownership

每层遍历columns 1..N，安全就assign、递归下一row、返回后再试下一column。属于当前activation。Assignment不是永久commit，它只是当前DFS路径上的state。

若child只同步读取board，下一次assignment会自然overwrite同一slot；显式board[row] = nil仍有价值：它恢复representation invariant、避免debug/emitter读到stale future rows，并让异常/提前终止策略更清楚。若callback可能保留board，必须copy snapshot；否则所有保存项都alias同一table，最终看见相同状态。

Base Case与Solution Emission Boundary

当row > size，prefix已有size个安全queen，就是一个解。必须决定三件事：emitter能否保留value；输出失败是否停止search；solution顺序是否是contract。

打印可以同步读取当前board，不保留reference；收集测试结果要copy。用characters生成每row时，内层column只比较board[row]，不要依赖pairs顺序。输出不是搜索correctness的一部分，最好由callback注入，count测试无需写console。

local function solve_queens(size, emit)
  local board, count = {}, 0
 
  local function search(row)
    if row > size then
      count = count + 1
      emit(board, size, count)
      return
    end
 
    for column = 1, size do
      if is_place_ok(board, row, column) then
        board[row] = column
        search(row + 1)
        board[row] = nil
      end
    end
  end
 
  search(1)
  return count
end
 
local total = solve_queens(8, function() end)
assert(total == 92)

若要保存solutions，emitter内部循环1..size复制columns。Shallow copy足够，因为values是numbers；若每row存table，则要明确deep-copy depth。Production library还应validate size为nonnegative integer并设置work limit，避免不可信N导致长时间搜索。

Printing Solutions而不污染Search

Printer把representation转换为display。每row构造N个cells，queen位置写Q，其它写.；用table.concat一次输出，避免大量string concatenation。Solution间插入编号和空行。Printer不修改board，不读globals，不决定search是否完整。

可以用compact representation验证，例如N=4的两个column vectors {2,4,1,3}与{3,1,4,2}。若展示顺序不重要，test把每个vector编码为comma-separated key并比较set；若DFS order是教学证据，则锁定candidate iteration为1..N并测试exact list。

Known Counts与Search Evidence Ledger

让回溯从“看起来能跑”变成可回归：N=1有1解，N=2和3有0解，N=4有2解，N=8有92解。对N=4可保存完整trace，N=8只count避免大量输出干扰。

复杂度、Symmetry与优化边界

Naive candidate tree上界接近N的排列规模，predicate每次扫描prior rows。Column/diagonal sets可把check降为constant-time，symmetry可减少首行搜索，但先保留简单版本作为oracle。优化后必须仍输出92个完整解；若只求fundamental solutions或乘对称数，contract已经变化。

Lua中可用三个tables记录used column、down diagonal、up diagonal，并在assign/undo成对更新。任何漏undo会错误prune，任何shared global会让多次solve互相污染。先用simple predicate和known counts建立oracle，再benchmark N增大时的nodes/time，才决定优化。

本章回顾：短程序也需要Invariant与Evidence

board[row]=column用representation消除row冲突，但partial/sparse table不能依赖length operator计进度。
同列与两类diagonal equality构成pure validity predicate。
每个recursive activation拥有一个row的choice/mutation/restore，shared board只在当前DFS路径有效。
Base case在row大于size时emits solution；保留solution必须copy，打印与搜索分离。
N=1、2/3、4、8的known counts和独立checker组成确定性回归门。