理解冲突驱动子句学习 SAT 求解器中的 VSIDS 分支启发式
计算机科学中的逻辑
2015-09-16 v3
摘要
冲突驱动子句学习 SAT 求解器的性能关键依赖于变量状态独立衰减和（VSIDS）分支启发式。尽管 VSIDS 在近十五年前被提出，且此后许多其他 SAT 求解分支启发式被提议，VSIDS 仍是最有效的分支启发式之一。在本文中，我们通过回答以下关键问题推进对 VSIDS 的理解。我们提出的第一个问题是“VSIDS 选择加性碰撞的那类变量有何特殊？”在回答此问题时，我们表明 VSIDS 绝大多数挑选、碰撞并学习桥变量，定义为连接 SAT 实例社区结构中不同社区的变量。这令人惊讶，因为 VSIDS 的发明早于社区结构与 SAT 求解器性能之间联系的发现十余年。此外，我们展示将 VSIDS 视为排序函数时与 temporal graph centrality measures（时间图中心性度量）强相关。综合这两发现，我们得出结论：VSIDS 挑选高中心性桥变量。第二个问题是“乘法衰减在使 VSIDS 如此有效中扮演什么角色？”我们展示乘法衰减表现得像指数移动平均（EMA），偏好持续出现在冲突中（信号）的变量而非间歇出现（噪声）的变量。第三个问题是“VSIDS 是否在时间和空间上聚焦。”我们展示 VSIDS 不成比例地从少数社区挑选变量，不同于例如随机分支启发式。我们综合这些发现发明了一种新的自适应 VSIDS 分支启发式，在 SAT Competition 2013 基准上比最著名的 VSIDS 变体之一求解了更多实例。
引用
@article{arxiv.1506.08905,
title = {Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers},
author = {Jia Hui Liang and Vijay Ganesh and Ed Zulkoski and Atulan Zaman and Krzysztof Czarnecki},
journal= {arXiv preprint arXiv:1506.08905},
year = {2015}
}