Too much information: CDCL solvers need to forget and perform restarts
Too much information: CDCL solvers need to forget and perform restarts
复制标题
信息过多：CDCL 求解器需要忘记并执行重新启动
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Florian Wörz
中科院分区：
文献类型：
--
作者：
Tom Krüger;Jan;Florian Wörz
冲突驱动子句学习（CDCL）是解决命题逻辑可满足性问题的非常成功的范例。这种求解器不是采用简单的深度优先回溯方法，而是以附加子句的形式了解发生冲突的原因。然而，尽管 CDCL 求解器取得了巨大成功，但人们对于什么因素以何种方式影响这些求解器的性能仍知之甚少。令人惊讶的是，本文将证明子句学习（无法消除某些子句）不仅可以提高运行时间，而且常常会使其急剧恶化。通过进行广泛的实证分析，我们发现 CDCL 求解器的运行时分布是多模态的。这种多模态可以被视为上述劣化现象的原因。同时，它也说明了尽管存在这种现象，为什么子句学习与子句删除和重新启动相结合实际上是 SAT 解答的事实上的标准。作为最后的贡献，我们将证明威布尔混合分布可以准确地描述多峰分布。因此，向基本实例添加新子句具有使运行时长尾的固有效果。这一见解提供了关于为什么重新启动和子句删除技术在 CDCL 求解器中有用的理论解释。
Conflict-driven clause learning (CDCL) is a remarkably successful paradigm for solving the satisfiability problem of propositional logic. Instead of a simple depth-first backtracking approach, this kind of solver learns the reason behind occurring conflicts in the form of additional clauses. However, despite the enormous success of CDCL solvers, there is still only a shallow understanding of what influences the performance of these solvers in what way. This paper will demonstrate, quite surprisingly, that clause learning (without being able to get rid of some clauses) can not only improve the runtime but can oftentimes deteriorate it dramatically. By conducting extensive empirical analysis, we find that the runtime distributions of CDCL solvers are multimodal. This multimodality can be seen as a reason for the deterioration phenomenon described above. Simultaneously, it also gives an indication of why clause learning in combination with clause deletion and restarts is virtually the de facto standard of SAT solving in spite of this phenomenon. As a final contribution, we will show that Weibull mixture distributions can accurately describe the multimodal distributions. Thus, adding new clauses to a base instance has an inherent effect of making runtimes long-tailed. This insight provides a theoretical explanation as to why the techniques of restarts and clause deletion are useful in CDCL solvers.
DOI：
10.1007/978-1-4419-9473-8
发表时间：
2011-01-01
期刊：
INTRODUCTION TO HEAVY-TAILED AND SUBEXPONENTIAL DISTRIBUTION
影响因子：
--
作者：
Foss, Sergey;Korshunov, Dmitry;Zachary, Stan
通讯作者：
Zachary, Stan
DOI：
10.1007/s10817-022-09623-5
发表时间：
2022
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Brakensiek, Joshua;Heule, Marijn;Mackey, John;Narváez, David
通讯作者：
Narváez, David