前言#

在 SAT 的精确算法中，其框架都是基于分支限界算法，其主体框架如下：

while True:
	conf = propagation()
	if conf is None:
		decide()
	else:
		resolve()

其中，resolve 用于回溯以撤销冲突的赋值，decide 用于决策变量的赋值，并继续探索树的下一层级，所有被决策的变量都会被记录到 trail 中，用于冲突时撤销赋值

如果我们想要求解的更快，那么决策的变量顺序是十分重要的

VSIDS 启发式策略#

一个好的启发式需要具有两个重要的特征：

1. 策略有效，在这里指选出来的变量能够快速剪枝，降低求解时间
2. 计算简单

然而这两点之间存在一个 trade-off，一个好的启发式就是平衡这两点，既要又要。

VSIDS ²，全称为 Variable State Independent Decaying Sum，其策略如下：

1. 每个变量的每个 该内容未公开或不可用 都有一个 inc，初始化为
2. 每当有一个子句被加入到子句库中，子句中的每个文字的 inc 都会增加
3. 拥有最高 inc 值的未赋值的变量与极性被选择，若存在相等的，随机选择一个（可以使用其他启发式配置，最简单的为随机）
4. 所有 inc 在一段时间后会除以一个常数

求解器中的 VSIDS#

现代求解器中最流行的是 MiniSAT 中提出的 EVSIDS（the exponential variant of VSIDS），它通过动态调整变量分数来优先选择在近期冲突中频繁出现的变量，从而提升求解效率，其做法为：

1. 变量分数初始化为 0，增量值 inc 默认为 1。
2. 每次冲突后，inc 会乘以 1/decay 进行衰减，其中 decay 初始为 0.8，每 5000 次冲突增加 0.01，最大不超过 0.95。
3. 在冲突子句中的变量分数会通过增加 inc 来“提升”（bumped），使得这些变量在后续搜索中更易被选中。

这种设计通过指数衰减平衡了历史信息与近期活动，帮助求解器快速聚焦于可能引发冲突的变量。

另一个优化#

由于 SAT 求解器会花费将近 90% 的时间在 BCP 这个过程中，因此在提出 VSIDS 的同时，文章中也有另一个关于 BCP 的优化，也就是我们熟知的双观察字

脚注#

1. Haralick, Robert M. and Gordon L. Elliott. “Increasing Tree Search Efficiency for Constraint Satisfaction Problems.” Artificial Intelligence (1979). ↩

2. Moskewicz, Matthew W. et al. “Chaff: engineering an efficient SAT solver.” Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232) (2001): 530-535. ↩