Understanding VSIDS

Significance

对现代SAT求解器中普遍使用的VSIDS及其变种进行了分析，并给出了解释，对SAT问题的启发式搜索具有指导性的意义。

Motivation

VSIDS：在最近推断过的子句中，出现次数多的变量，更为“关键”。

• 子句代表了变量之间的相关性，VSIDS关注相关性强的变量
• 通过图论中的社区结构和桥接变量进行解释。

Contribution

主要分析了VSIDS为什么高效。

• 挑选高中心性的桥接变量。
• 倾向于从较小的社区中选择变量。
• 倾向于从最近的社区中选择变量。

提出了一种自适应移动平均的快速分支启发式算法。

Details

VSIDS是CDCL SAT求解器中的分支启发式方法。在求解时对所有变量进行排序，即改变变量的枚举顺序。主要分析了cVSIDS（Chaff首次使用VSIDS）和mVSIDS（MiniSAT）中的VSIDS。

VSIDS介绍

• 活跃评分，初始化和VSIDS排名

  为每个变量分配一个浮点数activity，初始化为0，将变量的activity降序排序顺序称为VSIDS排名。

• 加法碰撞（Additive Bump）和乘法衰减（Multiplicative Decay）

  • cVSIDS：学习到子句中的变量活跃性+1
  • mVSIDS：冲突分析期间的活动变量（包括学习到的子句）活跃性+1

  所有变量的活跃性定期乘一个常数

• 每次赋值（猜变量）时选择活跃性最高的。

社区结构和桥接变量

VIG（变量关联图）

VIG中的顶点是所有变量，对于变量，的权重为：

其中代表子句的长度。

社区结构：子图内边数量多于出边（桥）数量

桥接变量：VIG中桥的顶点

验证方法：Louvain方法（社区结构）+基尼系数（统计度量）

时间中心性

TVIG（时间变量关联图）

VIG中的顶点是所有变量，对于变量，的权重为：

其中代表子句的长度，代表指数平滑系数，代表现在时间于学习到该子句的时间戳的差值。

度中心性（TDC）：顶点的度。

特征向量中心性（TEC）：图的邻接矩阵的最大特征值对应的特性向量的值。

验证方法：Spearman等级相关系数+Top-k排名比较

指数移动平均（EMA）和乘法衰减

将变量的活跃度理解为信号（方波），乘法衰减可以理解为低频滤波器。

自适应移动平均的快速分支启发式算法

adaptVSIDS：定义一个lbdema为已经学习到的字面量块距离（LBD）的平均值，当前学习的LBD小于lbdema时，使用0.99衰减率，大于时使用0.75衰减率。（典型衰减率为0.95）

Evaluation

• 对VSIDS有效性的分析较为完备
• 通过图的结构进一步推断，社区结构性强的SAT问题具有良好的可分性
• 可以通过这种可分性加强SAT问题的并行性，但具体实现有些困难，现有的基于KISSAT的并行求解器gimsatul

总结

现代SAT求解器中普遍使用VSIDS方法及其变种作为启发式搜索的方法之一，该论文对这个方法的合理性给出了解释，对SAT问题的启发式搜索策略的选择具有指导性的意义。VSIDS方法是优先选择在最近推断过的子句中，出现次数多的变量，在后续的变量枚举时优先枚举。由于子句代表了变量之间的相关性，作者使用图论中的社区结构和桥接变量进行解释。VSIDS高效的原因主要包括：挑选高中心性的桥接变量、倾向于从较小的社区中选择变量和倾向于从最近的社区中选择变量。作者对VSIDS的有效性分析较为完备，对该论文进一步思考，社区结构性强的SAT问题具有良好的可分性，可以通过这种可分性提高SAT问题的并行性。