Ch5 约束满足与 SAT (Constraint Satisfaction & SAT)

课件：lec5.pdf (约束满足问题 / CSP) + sat.pdf (SAT 问题)
教材：Artificial Intelligence: A Modern Approach (Russell & Norvig)，CSP 部分 Ch 6；SAT 部分补充讲义
教师：吉建民，USTC

0. 本章概述

本章把 约束满足问题 (Constraint Satisfaction Problems, CSP) 与 布尔可满足性问题 (Boolean Satisfiability, SAT) 统一在"约束"这一主题下：CSP 给出一种形式化表示语言（变量 + 值域 + 约束），让通用算法比标准搜索更强；SAT 则是 CSP 的一个特例（布尔变量 + 范式约束），也是第一个被证明为 NP-complete 的问题，是当代"通用问题求解中间语言"。二者共享同一族核心技术：回溯搜索、约束传播、冲突驱动学习、局部搜索。

第一部分：约束满足问题 (CSP)

1.1 什么是 CSP

与标准搜索的对比

• 标准搜索问题 (standard search problem)：状态是"黑盒 (black box)"——任何支持目标测试、评价函数、后继函数的数据结构均可。
• CSP：
  • 状态由变量 $X_i$ 及其取自值域 (domain) $D_i$ 的值定义；
  • 目标测试是一组约束 (constraints)，规定变量子集的合法取值组合；
  • 是一种形式化表示语言 (formal representation language)，允许设计通用 (general-purpose，而非问题特定) 的、比标准搜索更强的算法。

⭐ CSP 形式化定义

一个约束满足问题由三个部分 $X, D, C$ 构成：

• $X$：变量集 $\{X_1,\dots,X_n\}$。
• $D$：值域集 $\{D_1,\dots,D_n\}$，每个 $D_i$ 是 $X_i$ 的合法取值集合 $\{v_1,\dots,v_k\}$。
• $C$：约束集。每个约束 $C_i=\langle \text{scope},\text{rel}\rangle$：
  • scope：参与该约束的变量元组；
  • rel：定义这些变量可取值组合的关系 (relation)。
  • 关系既可显式枚举所有满足元组，也可表示为一个抽象关系，支持"测试某元组是否属于"和"枚举成员"两种操作。

状态、赋值与解

• 状态 (state)：对部分或全部变量的赋值 $\{X_i=v_i,\,X_j=v_j,\dots\}$。
• 相容 (consistent / legal) 赋值：不违反任何约束的赋值。
• 完备赋值 (complete assignment)：每个变量都被赋值。
• 部分赋值 (partial assignment)：只给部分变量赋值。
• ⭐ CSP 的解 (solution) = 相容且完备的赋值 (a consistent, complete assignment)。

1.2 经典示例

地图着色 (Map-Coloring)

• 变量 $X=\{\text{WA},\text{NT},\text{Q},\text{NSW},\text{V},\text{SA},\text{T}\}$（澳大利亚各州）。
• 值域 $D_i=\{\text{red},\text{green},\text{blue}\}$。
• 约束：相邻区域颜色不同。

  $$C=\{\text{SA}\neq\text{WA},\,\text{SA}\neq\text{NT},\,\dots,\,\text{NSW}\neq\text{V}\}$$

  其中 $\text{SA}\neq\text{WA}$ 是 $\langle(\text{SA},\text{WA}),\,\text{SA}\neq\text{WA}\rangle$ 的简写，可枚举为
  $\{(\text{red},\text{green}),(\text{red},\text{blue}),(\text{green},\text{red}),(\text{green},\text{blue}),(\text{blue},\text{red}),(\text{blue},\text{green})\}$。
• 解例：$\{\text{WA}=\text{red},\text{NT}=\text{green},\text{Q}=\text{red},\text{NSW}=\text{green},\text{V}=\text{red},\text{SA}=\text{blue},\text{T}=\text{green}\}$。

约束图 (Constraint Graph)

• 二元 CSP (Binary CSP)：每个约束只涉及两个变量。
• 约束图：节点 = 变量，弧 = 约束。
• 通用 CSP 算法利用图结构加速搜索（例：Tasmania 是独立子问题）。

密码算术 (Cryptarithmetic)

• 高阶约束示例：列约束涉及进位辅助变量 $X_1,X_2,X_3$（十/百/千位的进位）。

1.3 CSP 的分类体系

按变量类型分

按约束种类分

• 一元约束 (unary)：涉及单变量，如 $\text{SA}\neq\text{green}$。
• 二元约束 (binary)：涉及一对变量，如 $\text{SA}\neq\text{WA}$。
• 高阶约束 (higher-order)：涉及 3 个或更多变量，如密码算术列约束。
• 偏好 / 软约束 (preferences / soft constraints)：带代价，如 “red 优于 green”——导向约束优化问题 (constrained optimization problems)。

现实世界 CSP

分配问题（排课、审稿分配）、时间表、硬件配置、交通调度、工厂排程、平面布置 (floorplanning) 等；许多现实问题含实值变量。

1.4 回溯搜索 (Backtracking Search)

标准搜索的增量形式化 (incremental formulation)

• 初始状态：空赋值 $\emptyset$。
• 后继函数：给某未赋值变量赋一个不与当前赋值冲突的值；无合法值则失败。
• 目标测试：当前赋值完备。
• 性质：所有 CSP 一致；解都在深度 $n$；路径无关 → 可用 DFS；分支因子 $b=(n-l)d$，共 $n!\cdot d^n$ 叶。

⭐ 可交换性 (commutativity) 与回溯搜索

• 变量赋值可交换：$(\text{WA}=\text{red}\,\text{then}\,\text{NT}=\text{green})$ 等价于 $(\text{NT}=\text{green}\,\text{then}\,\text{WA}=\text{red})$。
• 因此每个节点只给单个变量赋值：$b=d$，叶数 $d^n$。
• ⭐ 回溯搜索 = 对 CSP 的单变量赋值深度优先搜索；是 CSP 的基本无信息算法 (basic uninformed algorithm)。
• 能力：可解 $n\approx 25$ 的 n-queens。

1.5 提升回溯效率的启发式

① 选哪个变量？—— 启发式选变量

最小剩余值（MRV, Minimum Remaining Values）：

• 选择合法取值最少的变量（“最受约束的变量”）
• 思想：早期失败（fail-fast），尽早发现死胡同
  度启发式（Degree Heuristic）：
• 当 MRV 出现平局时，选择对剩余变量约束最多的变量
• 即优先解决"牵连最多"的变量

② 值的顺序？—— 最少约束值（Least Constraining Value, LCV）

• 给定变量已选定，选对剩余变量排除值最少的值。
• 注意：计算此启发式本身需要一定开销。
• 与 MRV/LCV 组合可使 1000-queens 变得可行。

③ 能否提前检测失败？—— 前向检验 + 约束传播

前向检验 (Forward Checking)

• 思想：跟踪未赋值变量的剩余合法值；当任何变量无合法值时终止搜索。
• 比纯回溯更早发现失败，但不能发现所有早期失败（例如 NT 和 SA 不能同为 blue，前向检验不一定能立刻察觉）。

⭐ 约束传播 (Constraint Propagation)

• 定义：利用约束减少某变量合法值，进而减少其他变量合法值，如此反复。
• 比前向检验更强：反复在局部强制约束。

AC-3 算法详解

核心概念回顾

变量 $X$ 对变量 $Y$ 弧一致，当且仅当：对于 $X$ 的域 $D_X$ 中的每一个值 $x$，都存在 $Y$ 的域 $D_Y$ 中的某个值 $y$，使得二元约束 $C(X, Y)$ 被满足。

REVISE 过程

REVISE(X_i, X_j) 是 AC-3 的基本操作：检查 $X_i$ 对 $X_j$ 是否弧一致，若不成立则删除 $X_i$ 中那些在 $X_j$ 中找不到支持的值。

1
2
3
4
5
6
7

function REVISE(X_i, X_j) returns boolean
  revised := false
  for each x in D_i:
    if no value y in D_j allows (x, y) to satisfy the constraint between X_i and X_j:
      delete x from D_i
      revised := true
  return revised

• 返回 true 表示 $D_i$ 发生了改变（有值被删）
• 返回 false 表示 $D_i$ 未变（$X_i$ 对 $X_j$ 已弧一致）

AC-3 主算法

AC-3 维护一个弧队列 (queue)，初始包含 CSP 中的所有有向弧（每条二元约束产生两条有向弧：$(X_i, X_j)$ 和 $(X_j, X_i)$）。之后反复从队列取出弧调用 REVISE，若 REVISE 导致某变量的域缩小，则将所有指向该变量的弧重新入队。

1
2
3
4
5
6
7
8
9
10
11

function AC-3(csp) returns (whether consistent, modified domains)
  queue := a queue of all arcs (X_i, X_j) where i ≠ j
            and there is a constraint between X_i and X_j
  while queue is not empty:
    (X_i, X_j) := POP(queue)
    if REVISE(X_i, X_j):
      if D_i is empty:
        return false           // 无可满足赋值
      for each X_k in NEIGHBORS[X_i] \ {X_j}:
        PUSH(queue, (X_k, X_i))
  return true

为什么 REVISE 后要把 $(X_k, X_i)$ 重新入队？

当 $X_i$ 的域缩小后，之前与 $X_i$ 弧一致的邻居 $X_k$ 可能不再弧一致（因为 $X_k$ 中某些值的支持来自 $X_i$ 中被删的值）。所以需要重新检查所有 $(X_k, X_i)$ 弧。

算法性质

时间复杂度

• 每条弧最多入队 $d$ 次（因为 $D_i$ 最多被删 $d$ 次，每次删除导致指向 $X_i$ 的弧重新入队）
• 共有 $O(n^2)$ 条有向弧（二元 CSP 中最多每对变量有一条约束）
• 每次 REVISE 检查 $O(d^2)$ 对值
• 总复杂度：$O(n^2 d^3)$（或更精确地 $O(e d^3)$，其中 $e$ 为约束数）

AC-3 在搜索中的角色

AC-3 通常作为回溯搜索中的预处理或MAC (Maintaining Arc Consistency) 策略在每个赋值步骤后调用：

• 预处理：搜索前跑一次 AC-3 缩减全域
• MAC：每次赋值后调用 AC-3，检测早期失败并进一步传播约束

AC-3 检测的是局部不一致性。检测 CSP 的全部不一致性是 NP-难的 —— 若多项式时间可检测，则 P=NP。

1.7 问题结构与问题分解

独立子问题 (Independent Subproblems)

• 约束图的连通分量 (connected components) 即独立子问题（如 Tasmania 与澳洲大陆）。
• 可大幅缩减搜索空间。

子问题分解的收益

• 设每个子问题含 $c$ 个变量（共 $n$ 个），最坏代价：

  $$\frac{n}{c}\cdot d^c\quad(\text{对 }n\text{ 线性})$$

• 例：$n=80,\,d=2,\,c=20$：
  • 整体 $2^{80}$：以 $10^7$ 节点/秒需 40 亿年；
  • 分解为 $4\cdot 2^{20}$：仅需 0.4 秒。

⭐ 树结构 CSP (Tree-structured CSPs)

• 一般 CSP 最坏时间 $O(d^n)$；树结构 CSP 可在 $O(n d^2)$ 线性时间求解。
• 此性质也适用于逻辑与概率推理——语法限制 (syntactic restrictions) 与推理复杂度关系的重要范例。

树结构 CSP 算法

1. 任选一变量为根，按拓扑排序使父→子方向一致。
2. 从 $X_n$ 倒序到 $X_2$，对每条父子弧 $(X_k,X_i)$（$X_k=\text{Parent}(X_i)$）应用弧相容：
   RemoveInconsistent(Parent(X_i), X_i)。
3. 现在可从 $X_1$ 起按剩余值域一次性赋值而不产生冲突：从 $i=1$ 到 $n$，$X_i$ 与 $\text{Parent}(X_i)$ 相容地赋值。

• 复杂度：$O(n d^2)$。

近树结构与树分解 (Tree Decomposition)

• 现实问题常近树结构。树分解：把问题分解为一组连通子问题，两子问题共享约束时相连；独立求解后合并。

注：树分解与割集条件化 (cutset conditioning) 的图示细节，提取文本未完整呈现，需对照原课件查看。

1.8 CSP 的局部搜索 (Iterative Algorithms)

• 爬山、模拟退火等通常工作于完全状态 (complete states)（所有变量都已赋值）。
• 应用于 CSP：允许状态违反约束；算子是重赋值某变量。
• 变量选择：随机选任一冲突变量。
• ⭐ 值选择：最小冲突 (min-conflicts) 启发式——选造成与其他变量冲突最少的值；即以 $h(n)=\text{违反的约束总数}$ 爬山。

示例：4-Queens 与 3-SAT

• min-conflicts 对 4-queens 及（可满足的）3-SAT 实例常很有效。

加速手段

1. 模拟退火 (simulated annealing)：以随温度 $T$ 下降的概率接受"坏"移动，逃出局部极大。
2. minmax 优化（具体形式课件以图示给出，需对照原课件查看）。

第二部分：SAT 问题 (Boolean Satisfiability)

SAT 是 CSP 的布尔特例，也是当代"通用问题求解"的中间语言。本部分对应 sat.pdf。

2.1 SAT 基本定义

两种等价表述

• 布尔可满足性问题 (Boolean satisfiability problem, SAT)：给定由 AND、OR、NOT、变量和括号构成的布尔表达式，是否存在对变量 TRUE/FALSE 的赋值使整个表达式为真？
  • 例：$(x+yz̄)(x+y+z)(\bar y+\bar z)$。
• 命题可满足性问题 (Propositional satisfiability problem, SAT)：给定命题逻辑公式，是否可满足（存在一个模型）？
  • 例：$(\neg(x_1\to\neg x_2)\to x_3)\to(x_1\to(x_2\to x_3))$。
• 任意布尔表达式与命题逻辑公式都可等价转换为合取范式 (CNF)。

⭐ CNF 标准形式

• 合取范式 (conjunctive normal form, CNF)：$C_1\wedge C_2\wedge\cdots\wedge C_n$。
• 子句 $C_i$（$1\le i\le n$）：$l_1\vee l_2\vee\cdots\vee l_k$。
• 文字 (literal) $l_i$：某布尔变量或其否定。
• 例：$(\neg a_1\vee a_2)\wedge(\neg a_1\vee a_3\vee a_4)\wedge(a_1\vee\neg a_2\vee a_3\vee\neg a_4)$。
• SAT 问题：是否存在一组对所有布尔变量 TRUE/FALSE 的赋值，使整个 CNF 为真。

k-SAT

• 若 CNF $F$ 中每个子句恰好含 $k$ 个文字，称 k-SAT。
• 2-SAT：$k=2$；3-SAT：$k=3$。
• 任何 k-CNF 公式都可转换为 3-CNF（引入辅助变量，如 $(\neg a_1\vee a_2\vee x_1)\wedge(\neg a_1\vee a_2\vee\neg x_1)\wedge\cdots$）。

2.2 SAT 的计算复杂性⭐

⭐ 相变 (Phase Transition)

• 对基于 $N$ 个变量、$L$ 个子句的 k-SAT：随 $L/N$ 增大，从 100% 可满足过渡到 100% 不可满足。
• 记随机 k-SAT 为 $R_k(N,L)$，当 $N\to\infty$：

  $$\lim_{N\to\infty}\Pr[\text{sat},\,R_k(N,cN)]=\begin{cases}1 & c<c_k\\ 0 & c>c_k\end{cases}$$

• 已证 $c_2=1$，且 $3.003<c_3<4.81$；实验表明 $c_3\approx 4.28$。
• 呈 “easy-hard-easy” 模式；用 DPLL 解 3-SAT 时，$L/N\approx 4.28$ 处最困难。一般 NP 问题都有类似现象。

2.3 SAT 作为通用求解中间语言

• 把待解问题转为 SAT 求解，再把解转回原问题域。
• 为何 SAT 合适：
  1. NP-complete，每个 NP 问题可多项式归约到 SAT，表达力足够；
  2. 语法语义简单，便于设计、评价算法。
• 应用领域：
  • EDA（电子设计自动化）：
    • 组合等价性检查（Combinational Equivalence Checking）
    • 自动测试模式生成（Automatic Test Pattern Generation, ATPG）
  • AI（人工智能）：
    • 规划问题（Planning）
    • 知识推理（Knowledge Reasoning）
  • 有界模型检测（Bounded Model Checking, BMC）
  • NP 问题可以通过归约转化为 SAT 问题来求解

2.4 SAT 求解方法总览

两大类高效算法：

• “conflict-driven”（冲突驱动）：适合"大但简单"的问题
• “look-ahead”（前瞻）：适合"小但困难"的问题

单元子句与纯文字 (Unit Clauses & Pure Literals)

• 单元子句 (unit clause)：只含一个文字的子句。
  • 单元传播 (unit propagation)：对单元子句 $\{l\}$
    1. 删除所有含 $l$ 的子句；
    2. 删除所有含 $\neg l$ 的子句中的 $\neg l$。
• 纯文字 (pure literal)：在公式中只正出现或只负出现的文字。
  • 纯文字消去 (pure literal elimination)：删除所有含纯文字的子句。
• 例：CNF $(p\vee\neg q\vee\neg s)\wedge p\wedge(q\vee\neg r\vee\neg s\vee\neg t)\wedge(r\vee p)\wedge t$
  • $p$ 和 $\neg s$ 是 pure literals；$\{p\}$、$\{t\}$ 是 unit clauses。

2.5 ⭐ DPLL 算法

1
2
3
4
5
6
7
8
9
10
11
12

function DPLL(φ, σ)
  if φ is empty
    then return TRUE;           // 所有子句已满足
  if φ contains an empty clause
    then return FALSE;          // 有空子句 → 不可满足
  if l is a unit clause in φ
    then return DPLL(assign(l, φ), σ ∧ l);  // 单元传播
  if l is a pure literal in φ
    then return DPLL(assign(l, φ), σ ∧ l);  // 纯文字消除
  l := choose-literal(φ);      // 选择分支变量
  return DPLL(assign(l, φ), σ ∧ l) or
         DPLL(assign(¬l, φ), σ ∧ ¬l).     // 分支搜索

DPLL 的本质：带回溯的深度优先搜索，但通过单元传播和纯文字消除大幅剪枝。choose-literal() 的策略决定了求解效率。

DPLL 算法特点

• 二叉分支搜索（某变量的 t/f）。
• 在 unit propagation 与 pure literal elimination 基础上，尽可能晚地推迟分支。
• 只需多项式空间。
• choose-literal() 是算法关键。
• 几乎是所有精确 (complete) SAT Solver 的基础。

2.6 提升 DPLL 的技术

(1) 预处理 (Preprocessing)

对输入 CNF 预处理以便于计算：

• Sorting + subsumption（排序 + 包含消去）：

  $$\varphi_1\wedge(l_2\vee l_1)\wedge\varphi_2\wedge(l_2\vee l_3\vee l_1)\wedge\varphi_3\;\Rightarrow\;\varphi_1\wedge(l_1\vee l_2)\wedge\varphi_2\wedge\varphi_3$$

  （较短子句"吸收"包含它的较长子句。）
• 2-simplifying（二元子句化简），重复直至无新化简：
  1. 据 CNF 中二元子句构造蕴含图 (implication graph)：有二元子句 $\{\neg l,l'\}$ 则图中存在 $l\to l'$ 的边。
  2. 找出蕴含图的强连通分量 (SCC)，把 SCC 中所有文字等价为新文字。
  3. 把 CNF 中所有 SCC 文字及其否定分别用新文字及其否定替换。
  4. 应用 unit propagation 与 pure literal elimination。

(2) Look-ahead DPLL（充分利用未知搜索空间信息）

• Lookahead() 函数：若加入 $l$ 后用 unit propagation 得到矛盾，则加入 $\neg l$。
  • 比 unit propagation 更强，能推出更多；但效率损失大，实践中常不如简单 unit propagation。
• choose-literal() 启发式：
  • MOM heuristics (Maximum Occurrence in clauses of Minimum size)：选在极小子句中最常出现的文字；简单高效。
  • Jeroslow-Wang：选 score 值最大的文字：

    $$\text{score}(l):=\sum_{l\in c\,\wedge\,c\in\varphi}2^{-|c|}$$

    评估 $l$ 对满足 CNF 的贡献。
  • Satz：从候选文字集中，选经 unit propagation 后得到最小子句集的文字——充分利用 UP 结果。
• 对 “small but hard” 的问题较有效。

(3) ⭐ Conflict-driven DPLL（利用搜索过程中的已知信息，尤其是冲突）

非时序回溯 (Non-chronological backtracking / backjumping)

• 思想：当一个分支失败时：
  1. 找出导致失败的部分赋值 (conflict set)；
  2. 回溯到 conflict set 中最近的分支点 (most recent branching point)。
• conflict set 的确定：
  • 在已知部分赋值下，某文字成真是因在某子句上做 unit propagation，称该子句为该文字的原因 (cause)。例：在 $\{\neg a,\neg b\}$ 下，子句 $(a\vee b\vee\neg x)$ 是文字 $\neg x$ 的原因。
  • 出现矛盾时，存在两个互补文字；将它们的原因（子句）归结 (resolve) 为一个子句，其补文字集即当前矛盾的 conflict set。

冲突驱动子句学习 (Conflict Driven Clause Learning, CDCL)

• 思想：$C$ 是一个 conflict set，则 $\neg C$ 可加入原始子句集——保证包含 $C$ 的赋值不再发生，避免类似搜索。
• 例：当前部分赋值 $\{\neg p,q,r,\neg t,s\}$，子句 $(x\vee p\vee\neg q)$ 是 $x$ 成立的原因，子句 $(\neg x\vee\neg r\vee t)$ 是 $\neg x$ 成立的原因。则 $C=\{\neg p,q,r,\neg t\}$，可把 $(p\vee\neg q\vee\neg r\vee t)$ 加入原始子句集。
• 问题：可能导致空间膨胀——用其他技术控制学习，并在需要时丢弃学到的子句。
• 其他技术：two-watched-literals unit propagation、adaptive branching。
• 对 “big but simple” 的问题较有效。

2.7 局部搜索算法 (GSAT / WalkSAT)

• 不构造解，而是修改完整赋值以不断满足更多子句。
• ⭐ 不能证明公式的不可满足性。
• 主要方法：GSAT、WalkSAT；以及模拟退火、禁忌搜索 (Tabu search)、遗传算法、杂合方法（结合 DPLL 与局部搜索）。
• 一般需多项式空间；对一些（可满足的）问题非常有效。

GSAT

1
2
3
4
5

Repeat MAX-TRIES times or until all clauses satisfied:
    T := random truth assignment
    Repeat MAX-FLIPS times or until all clauses satisfied:
        v := variable which flipping maximizes # of satisfied clauses
        T := T with v's value flipped

核心思想：贪心地翻转使满足子句数增加最多的变量。通过**重启（restart）**跳出局部最优。

• 可加入 restarts 和 greediness；贪心搜索，寻找较好的"邻居"。

WalkSAT

1
2
3
4
5
6

Repeat MAX-TRIES times or until all clauses satisfied:
    T := random truth assignment
    Repeat MAX-FLIPS times or until all clauses satisfied:
        c := unsat clause chosen at random
        v := var in c chosen either greedily or at random
        T := T with v's value flipped

• 关注未满足的子句。

与 CSP 局部搜索的联系：WalkSAT 的 min-conflicts 思想与 CSP 的 min-conflicts 启发式一脉相承——都是从冲突出发做贪心修复。

2.8 一些 SAT Solvers

• 自 2002 起每年举办 SAT Competition (satcompetition.org)；较强者：Chaff (2001)、MiniSAT (2003)、zChaff (2004)。

2.9 SAT 应用：硬件验证 (Hardware Verification)

Model Checking

1. 将硬件设计描述为有限状态机 $M$（初始状态 + 状态转移关系）；
2. 把需满足的性质 $P$ 用时序逻辑描述；
3. 判断 $M$ 是否是 $P$ 的模型，即 $M\models P$。

性质类型

• 安全性 (safety)：“$x$ always holds”——从初始状态出发，任何可达状态上 $x$ 成立（$x$ 一般是命题公式）。
• 活性 (liveness)：“there will be a point in time when $x$ holds”——如请求终被回答。

⭐ 有界模型检测 (Bounded Model Checking, BMC)

• 判断性质 “always $p$” 是否在长度 $\le k$ 的运行周期内成立。
• 转为 SAT：是否存在一条长度 $\le k$、从初始状态到 $p$ 不成立状态的路径？
• 用谓词 $I(s)$ 刻画初始状态（每个状态 $s=(x_1,\dots,x_n)$ 是变量集合），用 $\tau(s,s')$ 表达后继关系。BMC 等价为下面公式是否可满足：

  $$I(s_0)\wedge\bigwedge_{i=0}^{k-1}\tau(s_i,s_{i+1})\wedge\bigvee_{i=0}^{k}\neg p(s_i)$$

  • 可满足 → 找到 “always $p$” 的反例；
  • 不可满足 → 不存在这样的路径，可增大 $k$ 再验证。

BMC 示例：二进制加法器

• 计数器不断循环从 $c=0$ 加到 $c=2$。证明 “initially $c\neq 3$ 则 always $c\neq 3$”。
• 状态 $s_i=(x_1^i,x_0^i)$，计数器 $c=2x_1+x_0$。
• 初始条件：$I(s_0)=\neg(x_0^0\wedge x_1^0)$（即 $c_0\neq 3$）。
• 转移关系：

  $$\tau(s_i,s_{i+1})=(x_1^{i+1}\equiv x_0^i)\wedge(x_0^{i+1}\equiv\neg(x_1^i\vee x_0^i))$$

• 性质：$p(s_i)=\neg(x_1^i\wedge x_0^i)$。
• SAT solver 可证明对任意 $k$，BMC 对应公式都不可满足，故 always $p$ 总成立。

2.10 SAT 的扩展

SMT (Satisfiability Modulo Theories)

• 对函数词和谓词有特殊解释的一阶公式是否可满足的判定问题。
  • 例：判断
    $(\sin(x)^3=\cos(\log y\cdot x)\vee b\vee -x^2\ge 2.3y)\wedge(\neg b\vee y<-34.4\vee \exp(x)>y/x)$
• SAT solver 高效但不能处理数字运算、线性约束等；SMT 可处理这类约束。
• SMT solver 本质：高效 SAT solver 不断调用一个处理特殊约束的求解器——把子句中原子先当普通命题原子交给 SAT solver，需要时再调用特殊约束求解器判断原子真假。
• SMT 问题一般是 NP-complete。

QBF (Quantified Boolean Formula problem)

• 容许 $\forall$（for all）和 $\exists$（there exists）出现的布尔表达式的可满足判定问题。
  • 例：$\forall x\,\exists y\,\exists z.\,(x\vee y\vee z)\wedge(\neg x\vee\neg y\vee\neg z)$。
• QBF 是 PSPACE-complete，比 SAT 更复杂，尚无可实用的 QBF solver。

2.11 计算复杂性补遗

“容易"与"困难”

• 需指数时间才出结果 → “困难”（如 TSP 货郎担问题）。
• 多项式时间 $O(n^k)$（$k$ 常数、$n$ 输入规模）可出结果 → “容易”；但"容易"是相对的（$O(n^{100})$ 实际也可能很难）。

计算模型：图灵机

• 图灵机模型是计算机计算能力的极限，目前尚无超越它的计算模型。

确定性 vs 非确定性图灵机

• 确定性图灵机 (DTM)：转移函数单值。

  $$\delta:Q\times T\to Q\times T\times\{L,R\}$$

• 非确定性图灵机 (NTM)：转移函数多值。

  $$\delta:Q\times T\to\mathcal{P}(Q\times T\times\{L,R\})$$

  • 含猜想阶段与验证阶段。

⭐ P 类与 NP 类

• P：在确定性图灵机上多项式时间可解。
• NP：在非确定性图灵机上多项式时间可解；等价地，在确定性图灵机上多项式时间可验证。
• $\mathbf{P}\subseteq\mathbf{NP}$；P ?= NP——大多数学者认为 $\mathbf{P}\neq\mathbf{NP}$。

NP-hard 与 NP-complete

• NP-hard：每个 NP 问题都可在多项式时间归约到 $Q$。
• NP-complete：既是 NP 问题，又是 NP-hard。
• 性质：所有 NP-complete 问题对多项式归约关系构成等价类（自反、对称、传递）；若找到一个 NPC 问题的多项式算法，则 $\mathbf{P}=\mathbf{NP}$。

关键概念速查表

本章关键概念清单

• [ ] 写出 CSP 三元组 ⟨X, D, C⟩ 的定义，并说明"解 = 相容且完备的赋值"
• [ ] 区分一元/二元/高阶/软约束，并能给出每类的例子
• [ ] 解释离散有限/无限值域与连续变量 CSP 的复杂度差异
• [ ] 用可交换性论证为何回溯搜索每节点只赋单变量（$b=d$，叶数 $d^n$）
• [ ] 说出 MRV、度启发式、最少约束值 (LCV) 各自的作用与使用时机
• [ ] 说明前向检验与约束传播的差别，以及为何约束传播更强
• [ ] 写出节点/弧/路径相容、k-相容、强 k-相容的定义
• [ ] 给出 AC-3 的复杂度 $O(n^2d^3)$ 并说明"检测全部不一致是 NP-hard"
• [ ] 解释 Alldiff 全局约束
• [ ] 用子问题分解推导 $\frac{n}{c}d^c$ 的代价，并解释 $2^{80}$ vs $4\cdot 2^{20}$ 的差距
• [ ] 描述树结构 CSP 的 $O(nd^2)$ 算法三步骤
• [ ] 描述 min-conflicts 局部搜索的工作方式（完全状态 + 冲突变量 + 最小冲突值）
• [ ] 写出 SAT 的两种定义，并说明任意布尔/命题公式都可转为 CNF
• [ ] 写出 CNF、子句、文字的定义，并解释 k-SAT 与 3-CNF 转换
• [ ] 列出 SAT/3-SAT/2-SAT/Horn-SAT 各自的复杂性与复杂性类
• [ ] 陈述 Cook 定理，并解释 SAT 为何是"首个 NPC 问题"
• [ ] 描述 SAT 相变现象（easy-hard-easy，$c_3\approx 4.28$）
• [ ] 默写 DPLL 伪代码，说明单元传播与纯文字消去的化简规则
• [ ] 解释 DPLL 的预处理（sorting+subsumption、2-simplifying 与蕴含图 SCC）
• [ ] 说出 Look-ahead 的三种 choose-literal 启发式（MOM / Jeroslow-Wang / Satz）及 score 公式
• [ ] 解释 backjumping（非时序回溯）如何确定 conflict set
• [ ] 描述冲突驱动子句学习 (CDCL) 的思想，并指出其空间膨胀问题
• [ ] 默写 GSAT 与 WalkSAT 的算法结构，说明二者差异及"不能证不可满足"
• [ ] 列出 GRASP / zChaff / MiniSAT / mach_dl 的代表技术与特点
• [ ] 写出 BMC 转 SAT 的公式 $I(s_0)\wedge\bigwedge\tau\wedge\bigvee\neg p$
• [ ] 区分安全性 (safety) 与活性 (liveness) 性质
• [ ] 说明 SMT 与 QBF 的定义及其复杂性（NP-complete / PSPACE-complete）
• [ ] 区分确定性/非确定性图灵机、P/NP、NP-hard/NP-complete，并说明 P ?= NP