双监视文字

朴素传播每次都问所有子句“你现在只剩一个出口吗”。双监视反过来让子句只在一个关键出口关闭时醒来。只要还能把观察点移到另一个未关闭出口，就无需知道其他文字的精确状态；当再也移不动时，另一观察点便是最后出口或冲突证据。

Watch 是对子句状态的惰性索引，不是对两个“最重要文字”的语义判断。它们可随搜索改变，且不影响模型集合。恰因为索引只响应从未赋值到假的收紧动作，回溯把假值恢复为未赋值时无需把 watch 移回历史位置：约束只会放松，不会漏掉新单位或新冲突。

取子句

初始监视 $a,\mathrm{\neg }b$。赋值 $a=0$ 后，$a$ 变假；扫描发现 $c$ 未赋值，于是把第一只 watch 移到 $c$。随后赋值 $b=1$，$\mathrm{\neg }b$ 变假；扫描发现 $d$ 未赋值，把第二只 watch 移到 $d$。现在 watches 为 $c,d$，而 $a,\mathrm{\neg }b$ 已假。

再赋 $c=0$ 时，处理 watch $c$。非监视候选 $a,\mathrm{\neg }b$ 都假，找不到替代者；若 $d$ 未赋值，$C$ 成为单位子句并传播 $d=1$；若此前已有 $d=0$，两只 watches 及所有其他文字均假，报告冲突；若 $d=1$，子句已满足。三个分支直接覆盖处理规则，没有假设“两只 watch 非假”。

复杂度边界需要按实际 literal inspections 讨论。一次长子句扫描可能访问很多文字；缓存上次扫描位置可避免每次从头开始，但回溯、restart 和反复迁移仍影响总成本。不能把并查集的近常数摊还界套到 watch，也不能仅凭“每子句两个指针”宣称整轮传播严格线性。删除子句时还必须从两个 watch lists 安全摘除，悬空索引会造成漏传播或访问已释放内存。

双监视把传播成本集中到受当前赋值直接威胁的子句，是 CDCL 能频繁到达传播不动点的关键工程机制。二元子句可直接监视两个文字并在其中一个变假时传播另一个；对极多二元子句，专用 implication lists 还能减少通用扫描开销，但仍需保持相同逻辑结果。

在增量 SAT 中，assumption 撤销不要求恢复 watch，新增子句却必须初始化两个合法观察点并立即检查它在当前 trail 下是否已经单位或冲突。证明日志通常不记录 watch 移动，因为它们没有逻辑含义；checker 只验证传播或学习所依赖的子句，而求解器实现测试则应另行覆盖 watch-list 完整性。