VSIDS 分支启发式

一次冲突暴露了当前公式中刚刚活跃的一片约束。若变量反复出现在近期冲突原因里，围绕它作新决策往往能较快触发传播或新的冲突，从而继续细化这一局部结构。指数衰减让很久以前的热点逐渐让位，而不是让早期偶然事件永久统治队列。

VSIDS 的“state independent”不表示它与求解状态无关；名称强调分数不直接按变量当前真、假、未赋值三态定义。实际活动度高度依赖已学子句、冲突分析和 restart 历史。它是一种在线反馈控制，而不是对变量语义重要性的静态测量。

取 $\rho =1/2$，变量初始活动度均为零。三次冲突的 bump 集依次为

按递推计算，$(A(a),A(b),A(c))$ 依次为

若三者均未赋值，第三次冲突后选择 $b$。这个计算还说明一次旧 bump 的权重每过一轮减半。若实现使用不断增大的 increment，数值会不同，但除以共同尺度后排序一致；把两种表示的原始数值直接比较没有意义。

边界在于“近期活跃”不等于“应取真”，也不保证产生最小搜索树。某些构造实例会诱导启发式长期关注错误区域，改变 tie-breaking 或随机种子即可令运行时间大幅变化。VSIDS 不承担可靠性：即使分数更新有 bug，只要求解器仍公平探索并验证冲突，可能只是变慢；若启发式永久饿死某些必要决策，则终止性和完备性才会受损。活动度也不是概率，不能解释为变量属于模型的置信度。

高活动变量与 learned clauses 共同形成短期搜索焦点。Restart 后 trail 被清空而活动度通常保留，使下一阶段围绕刚才的冲突区域重新排列决策；若连活动度也清零，restart 就失去这部分跨阶段记忆。Clause activity 与 variable activity 是不同队列：前者常用于决定保留哪些 learned clauses，后者用于分支，不能混用阈值。

实际评估需固定衰减率、bump 集定义、phase policy、restart 与子句删除，因为这些机制相互反馈。只报告“启用了 VSIDS”不足以复现实验。自适应分支算法可以混合活动度、学习率或随机探索，但任何更换都应通过运行分布而非单个最快样例比较。