SAT 求解器重启策略

非时序回跳只撤销到当前 learned clause 指定的层，restart 则主动放弃整段非根上下文。它之所以不是白费工作，是因为冲突留下的子句与活动度仍在：下一阶段面对的是更强的公式和改变后的决策排序。短阶段广泛试探不同区域，长阶段则保证有机会完成需要深搜索的证明。

这种机制针对 SAT 搜索常见的重尾行为：某个分支顺序可能很快成功，也可能在巨大局部区域里耗尽资源，而事前难以识别。Restart 用可控预算限制一次坏选择的损失；它不能弥补错误编码、无效学习或永久不公平的分支规则。

若基础预算为 100 次冲突，前七轮 Luby 预算是

这些是各轮独立上限，不是从启动起的累计阈值。设上一轮从冲突中学到

重启后 $q,d$ 都未赋值，$L$ 暂不传播；若新阶段先得到 $q=1$，它便立即强制 $d=0$，原冲突区域已被永久改形。若 restart 错误地删除 $L$，搜索仍可能可靠，但失去这项记忆；若保留的 $L$ 本来不是输入的逻辑后果，则任何 schedule 都救不了可靠性。

无界序列是重要但并非孤立的充分条件。若每次长阶段开始后，分支启发式仍以一种不公平方式反复选择同样前缀，长预算也可能被浪费；相反，某些保留子句的 CDCL 状态机会凭持续学习证明终止，不必等待一次完整无重启搜索。动态策略常以经验阈值触发，它们在基准上有效不等于对所有公式支配 Luby 或几何 schedule。

Restart 与 phase saving 常配合：求解器回到根层，却在重新遇到变量时先尝试上轮极性，得到“保留局部赋值方向、重新排列决策次序”的效果。活动度衰减、子句删除和 restart 周期共同决定跨阶段保留多少记忆，因此调参不能只看一个旋钮。

增量 SAT 还需区分内部 restart 与查询边界。撤销 assumptions 后开始下一次查询会改变有效前提集合；含局部 assumption 的学习子句必须通过显式 assumption literal 保持条件化。可复现实验应报告 schedule、基础预算、动态触发统计及随机种子，并以多次运行分布评价重尾波动。