朝向 SAT 求解器中重启的复杂性理论理解
计算复杂性
2020-05-12 v2
摘要
重启是一类被广泛使用且对冲突驱动子句学习（CDCL）布尔 SAT 求解器效率不可或缺的技术。尽管此类策略的实用性已在经验上得到充分确立，但对于重启是否确实对 CDCL 求解器的能力至关重要的理论解释仍然缺乏。在本文中，我们证明了一系列刻画各类 SAT 求解器模型下重启能力的理论结果。更确切地说，我们做出如下贡献。首先，我们使用一族可满足实例，证明了带重启的{\it 醉酒}随机化 CDCL 求解器模型与不带重启的同一模型之间存在指数级分离。其次，我们表明，对于一族不可满足实例，采用 VSIDS 分支与重启（重启后活动度清零）的 CDCL 求解器配置比不带重启的相同配置在能力上指数级更强。据我们所知，这些是涉及 SAT 求解器中重启的首个分离结果。第三，我们表明，相对于若干带非确定性静态变量与值选择的 CDCL 和 DPLL 求解器模型，重启并不增加任何证明复杂性理论上的能力。
引用
@article{arxiv.2003.02323,
title = {Towards a Complexity-theoretic Understanding of Restarts in SAT solvers},
author = {Chunxiao Li and Noah Fleming and Marc Vinyals and Toniann Pitassi and Vijay Ganesh},
journal= {arXiv preprint arXiv:2003.02323},
year = {2020}
}