重访用于SAT的决策图方法
计算机科学中的逻辑
2018-05-10 v1
摘要
使用决策图消除SAT中变量的符号化子句分发变体被证明在困难组合实例上表现良好。在本文中，我们重访该方法的现有ZDD与BDD两种变体。我们进一步研究了用于选择下一个待消除变量的不同启发式。我们的实现进一步利用了开源BDD库Sylvan的并行特性。
引用
@article{arxiv.1805.03496,
title = {Revisiting Decision Diagrams for SAT},
author = {Tom van Dijk and Rüdiger Ehlers and Armin Biere},
journal= {arXiv preprint arXiv:1805.03496},
year = {2018}
}