双监视文字

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

Watch 是对子句状态的惰性索引，不是对两个“最重要文字”的语义判断。它们可随搜索改变，且不影响模型集合。回溯无需恢复 watch 的结论针对按决策层撤销完整 trail 后缀的标准搜索：传播已在每次新决策前完成，撤销时同时删除对应传播后果。不能把它理解为任意删除单个赋值都无需处理。

例如 $a\vee b$ 在 $a=0$ 后强制 $b=1$。若只删掉 $b=1$ 而保留 $a=0$，子句重新成为单位，却没有任何 watch 刚刚变假来唤醒它；标准层回溯不会留下这种不完整撤销状态。保留 watch 位置与正确维护 trail 是两个相互配合的责任。

取子句

初始监视 $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 安全摘除，悬空索引会造成漏传播或访问已释放内存。

实际扫描还可先检查另一只 watch：若它已经为真，整条子句已满足，可以直接跳过搜索替代者。这个快捷检查只是省扫描；若缓存的满足文字后来被撤销，仍必须按当前赋值重新判断，不能把“以前满足过”当作永久满足。

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

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