> For AI agents: the complete documentation index is available at https://shijin.space/llms.txt, the full documentation bundle is available at https://shijin.space/llms-full.txt. # CDCL 搜索策略：分支、重启与子句管理 前置知识：[CDCL](https://shijin.space/knowledge/sat-cdcl/index.md) 中的赋值轨迹、冲突分析、回跳与传播，以及[预处理与内处理](https://shijin.space/knowledge/sat-preprocessing/index.md)中的公式变换。 ## 推理规则之外，还要决定搜索资源怎样分配 CDCL 的传播和冲突分析说明哪些结论可以推出，但没有唯一规定下一次选择哪个变量、在一个方向上搜索多久，以及保留多少学习子句。分支、重启和子句管理分别控制这些选择；它们改变搜索路径和执行成本，仍须服从传播、学习与回跳的正确性条件 \[[1, secs. 4.3.1.2–4.3.1.4](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-MarquesSilvaLynceMalik2021CDCL)\]。 可以先把三个问题分开：分支选择下一步试探的位置，重启改变当前搜索前缀，子句管理调整可复用的推理信息。随后再观察它们如何互相影响。例如，频繁重启若保留了学习子句和变量活跃度，下一轮仍会受到上一轮冲突的引导；若删除了大量有用的学习子句，相同的分支策略也可能重新遇到旧冲突。 ## 变量选择：近期冲突给哪些变量加分 ### 用指数衰减理解活跃度 VSIDS 一类策略提高近期参与冲突分析的变量的分数，并逐渐降低较早冲突的影响。具体实现对加分对象、更新时机和分值表示有所不同，不能把某一段教学公式当成所有求解器的精确定义 \[[1, pp. 148–149](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-MarquesSilvaLynceMalik2021CDCL)\]。 设第 $t$ 次冲突中被选中加分的变量集合为 $S_t$，采用下面的指数衰减示意模型： $$ A_t(v)=\rho A_{t-1}(v)+\mathbf{1}[v\in S_t], \qquad A_0(v)=0,\quad 0<\rho<1. $$ 展开后得到 $$ A_t(v)=\sum_{i=1}^{t}\rho^{t-i}\mathbf{1}[v\in S_i]. $$ 同一次参与越接近现在，权重越大。这是在给冲突历史排序，不是在估计“变量取真”的概率，也不表示高分变量在原公式中一定出现得更多。 取 $\rho=1/2$，依次观察 $$ S_1=\{a,b\},\quad S_2=\{b,c\},\quad S_3=\{c\},\quad S_4=\{a\}. $$ 按 $(a,b,c)$ 的顺序，分数依次为 $$ \begin{aligned} \mathbf{A}_1&=(1,1,0),\\ \mathbf{A}_2&=(1/2,3/2,1),\\ \mathbf{A}_3&=(1/4,3/4,3/2),\\ \mathbf{A}_4&=(9/8,3/8,3/4). \end{aligned} $$ 第 $3$ 次冲突后 $c$ 的分数最高；第 $4$ 次之后 $a$ 又超过了 $c$。实际分支只在当前未赋值且允许决策的变量中选取最高分者，因此“全局最高分”不一定就是下一个决策变量。这里给出的是一段假定的加分事件，用于展示更新规则，不声称它对应某个求解器的实际运行轨迹。 ### 分数更新也有实现成本 上式直接实现需要每次冲突遍历全部变量。另一种等价的排序实现是只增加 $S_t$ 中变量的计数，并让每次冲突的加分量逐步增大：第 $i$ 次加分为 $\rho^{-(i-1)}$。在第 $t$ 次冲突后，把所有计数共同乘以 $\rho^{t-1}$，恰好恢复上式的分数；共同的正比例因子不改变排序。 因此可以把全局衰减转化成增长的加分量，再配合优先队列和必要的数值缩放。MiniSat 的 `varBumpActivity`、`varDecayActivity` 与变量排序结构展示了这类实现思路；分数变化与排序结构中的位置需要同步 \[[2, sec. 4.6](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-EenSorensson2003MiniSat)\]。 ## 取值选择：相位保存不等于变量排序 选中变量 $x$ 后，还要决定先尝试 $x=0$ 还是 $x=1$。相位保存（phase saving）记住变量先前使用过的取值，在变量重新成为决策对象时优先尝试这个值。保存哪些赋值、何时更新，属于具体策略的选择 \[[1, sec. 4.3.1.2.3](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-MarquesSilvaLynceMalik2021CDCL)\]。 变量活跃度回答“先决定谁”，相位保存回答“先试哪个值”。两者不能混为一个分数。例如，$a$ 的活跃度最高，而保存的相位为 $0$，就可以优先决定 $a=0$；分数高不表示应该把它设为真。 相位保存也解释了为什么重启后可能重新出现相似的赋值前缀。这并不必然是重复劳动：学习子句、变量顺序和新的根层传播可能已经改变。反过来，相位保存也不保证总能把搜索带到有解区域。 ## 重启：短尝试与长搜索怎样交替 ### 保留推理信息，撤销搜索赋值 在这里讨论的普通单次求解中，重启撤销非根层的搜索赋值，保留原公式、仍有效的学习子句及策略要求保留的启发式状态，再继续传播与分支。它不会把已学到的结论一并清空；增量调用中的假设边界需要按接口约定另行处理 \[[1, sec. 4.3.1.2](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-MarquesSilvaLynceMalik2021CDCL)\]。 重启过密可能反复支付建立搜索前缀的成本；间隔过长则可能让求解器持续停留在效果较差的方向。搜索是否有效不能只看当前赋值变量数，因为深轨迹不自动意味着接近模型，也不意味着接近短反证。 ### 按预定序列分配冲突预算 一种简单基线是按 Luby 序列分配每轮的冲突预算。若基本预算为 $B$，则依次使用 $$ B\cdot(1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,\ldots). $$ 例如 $B=100$ 时，前七轮允许 $100,100,200,100,100,200,400$ 次冲突。序列让短尝试反复出现，同时穿插更长的连续搜索。这里的预算单位是冲突次数，不是运行时间；不同冲突的处理代价可以相差很大 \[[3, sec. 3](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-BiereFroehlich2019Restarts)\]。 Luby 序列在随机算法重启中的理论动机不能直接变成对任意 CDCL 配置的最优性保证：CDCL 通常跨轮保留学习信息，各轮并不是相互独立的重新采样。 ### 根据近期学习子句调整重启 另一类方法比较近期与长期的学习子句 LBD。当近期数值持续偏高时，把它作为调整搜索方向的信号。Biere 与 Fröhlich 用快、慢两个指数移动平均实现了这一思路 \[[3, secs. 4.1–4.3](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-BiereFroehlich2019Restarts)\]。 令 $g_t$ 为第 $t$ 次冲突产生的学习子句的 LBD，分别维护 $$ \begin{aligned} f_t&=(1-\alpha_f)f_{t-1}+\alpha_f g_t,\\ s_t&=(1-\alpha_s)s_{t-1}+\alpha_s g_t, \qquad 0<\alpha_s<\alpha_f<1. \end{aligned} $$ 快平均更快响应近期变化，慢平均提供较稳定的参照。一个简化的触发条件是 $f_t>\kappa s_t$，其中 $\kappa>1$；实际策略还要处理初始化、两次重启之间的最小间隔及阻止重启的条件。 例如先有 $f_{t-1}=s_{t-1}=4$，新 LBD 为 $8$，取 $\alpha_f=1/2$、$\alpha_s=1/8$，得到 $f_t=6$、$s_t=4.5$。若 $\kappa=1.2$，数值已满足触发条件。这里的参数仅用于算例，不是推荐配置；满足条件也只是启发式信号，不是“当前分支必然无效”的证明。 ### 完备性需要单独说明 任意组合重启、学习和删除规则，并不自动保证终止。若总在形成必要进展之前重启，并丢掉已经获得的信息，就可能重复同样的搜索。允许足够长的搜索区间、或保留足够进展信息，是讨论完备性时常见的条件；实际配置仍须结合具体算法论证 \[[4, sec. 3.6.4.5](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-DarwichePipatsrisawat2021Complete)\]。 ## 子句管理：学习有收益，也有持续成本 学习子句能够提前传播、阻止重复失败；但它也占用存储，可能进入监视列表，并在后续传播时被访问。数据库越大不自动意味着求解越快，因此求解器会定期删除一部分学习子句 \[[1, sec. 4.3.1.3](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-MarquesSilvaLynceMalik2021CDCL)\]。 常见评价信息包括子句长度、LBD 和近期使用情况。长度描述每次处理可能涉及多少文字；LBD 描述记录时刻的文字跨越多少个决策层；活跃度试图捕捉近期参与推理的情况。三者提供的信号不同，没有一个量能单独证明未来收益。 例如一个四文字子句的层号是 $(1,1,4,4)$，另一个三文字子句的层号是 $(1,2,4)$，它们的 LBD 分别是 $2$ 和 $3$。较长的子句反而具有较低 LBD；如果只按长度排序，就会忽略这种差别。LBD 的计算依赖当时的轨迹，不能把不同时间的记录误当成子句的固定语法属性。 在原始公式保留且学习子句确由它蕴含的基本 CDCL 场景中，删除这些学习子句不会改变原公式的模型集合，但仍有两项额外责任：不能破坏正在使用的原因引用，也不能忽略重启与删除对搜索进展的影响。若同时进行了会改变模型集合的内处理，则需要按[公式变换及恢复规则](https://shijin.space/knowledge/sat-preprocessing/index.md)解释当前数据库，不能直接套用这个简单前提。 ## 怎样评价一种搜索策略 可以把运行成本粗略拆成传播、冲突分析、数据库维护及公式变换等部分。冲突次数减少，而每次冲突变得更昂贵时，总时间仍可能上升；总传播次数相同，访问的子句长度和内存位置不同，成本也可能不同。 比较策略至少需要固定实例集合、求解器版本、编译与参数、硬件和资源限制，并记录结果状态。超时或资源中止属于未解决，不能计作 UNSAT。含随机选择时还应保留随机种子，并观察不同运行之间的变化。 消融比较应尽量只改变一个机制：例如保持分支和子句删除策略一致，比较两种重启规则，再观察它们与其他机制组合后的变化。至少同时检查解决实例数和运行时间；不能只在双方都解决的实例上报告平均时间而隐藏超时差异。需要合并超时时，可明确采用 PAR-2 等约定：成功运行计实际时间，超时计两倍时间上限；它只是评价规则之一 \[[5, sec. 9](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-BiereEtAl2024Cadical)\]。 最近的实现也在改进“用什么量安排搜索工作”。CaDiCaL 3.0 使用近似访存工作量的 ticks 调度搜索模式和内处理，回应了冲突数与传播数不能稳定代表执行成本的问题。ticks 是实现中计算的确定性代理量，不是硬件实际测得的缓存访问次数；论文实验支持其在所评测配置中的作用，不能据此推断每个实例都会加速 \[[6, secs. 6–7](https://shijin.space/knowledge/sat-search-strategies/index.md#ref-sat-search-strategies-PollittEtAl2026Cadical)\]。 阅读新的搜索策略时，可以分别追问：它改变了哪一个选择，维护这些信息花了多少成本，在哪些实例上有收益，以及结果是否通过[独立验证](https://shijin.space/knowledge/sat-result-verification/index.md)。这四个问题把策略动机、实现代价、实验观察和正确性区分开来。 ## 参考文献 {#references-sat-search-strategies}
1\. Joao Marques-Silva, Ines Lynce, and Sharad Malik. *Conflict-driven clause learning SAT solvers*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200987).
2\. Niklas Eén and Niklas Sörensson. *An extensible SAT-solver*. Theory and applications of satisfiability testing. 2004. [DOI](https://doi.org/10.1007/978-3-540-24605-3_37).
3\. Armin Biere and Andreas Fröhlich. *Evaluating CDCL restart schemes*. Proceedings of pragmatics of SAT 2015 and 2018. 2019. [DOI](https://doi.org/10.29007/89dw).
4\. Adnan Darwiche and Knot Pipatsrisawat. *Complete algorithms*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200986).
5\. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. *CaDiCaL 2.0*. Computer aided verification. 2024. [DOI](https://doi.org/10.1007/978-3-031-65627-9_7).
6\. Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere. *CaDiCaL 3.0*. 29th international conference on theory and applications of satisfiability testing. 2026. [DOI](https://doi.org/10.4230/LIPIcs.SAT.2026.40).
## 配套演示 - [现代 SAT 求解器：传播、搜索策略与内处理 · 16:9](https://shijin.space/slides/sat-implementation/index.html) - [现代 SAT 求解器：传播、搜索策略与内处理 · 4:3](https://shijin.space/slides/sat-implementation/index-4-3.html)