深入探讨冲突产生的决策
A Deep Dive into Conflict Generating Decisions
摘要：
布尔可满足性（SAT）是一个著名的NP完全问题。尽管这种理论上的困难，SAT求解器基于冲突驱动子句学习（CDCL）可以解决大型SAT实例从许多重要的领域。CDCL从冲突中学习子句，这是一种允许求解器修剪其搜索空间的技术。CDCL中的选择算法优先考虑最近冲突中涉及的变量。虽然只有一小部分决策会产生冲突，但许多决策会产生多个冲突。在本文中，我们详细研究了CDCL中的冲突生成决策。我们调查的影响，单冲突（SC）的决定，只产生一个冲突，和多冲突（MC）的决定，产生两个或更多。我们经验性地描述了这两种类型的决定的基础上，每种类型的决定所产生的学习条款的质量。我们还显示了一个重要的连接在同一MC决策，其中一个学习的子句触发下一个形成一个链的子句的学习连续的子句之间的学习。这导致考虑冲突之间的相似性，为此，我们制定了conflictsproximity的概念作为一个相似性度量。我们发现，在mc决策的冲突更密切相关的连续冲突产生的SC决定。最后，我们开发了共同原因变量减少（CRVR）作为一种新的决策策略，减少了一些变量的选择优先级从学习条款的MC决策。我们在三个领先的求解器中实施的CRVR的实证评估显示了SAT竞赛-2020主赛道基准测试的性能提升。
英文摘要：
Boolean Satisfiability (SAT) is a well-known NP-complete problem. Despite this theoretical hardness, SAT solvers based on Conflict Driven Clause Learning (CDCL) can solve large SAT instances from many important domains. CDCL learns clauses from conflicts, a technique that allows a solver to prune its search space. The selection heuristics in CDCL prioritize variables that are involved in recent conflicts. While only a fraction of decisions generate any conflicts, many generate multiple conflicts. In this paper, we study conflict-generating decisions in CDCL in detail. We investigate the impact of single conflict (sc) decisions, which generate only one conflict, and multi-conflict (mc) decisions which generate two or more. We empirically characterize these two types of decisions based on the quality of the learned clauses produced by each type of decision. We also show an important connection between consecutive clauses learned within the same mc decision, where one learned clause triggers the learning of the next one forming a chain of clauses. This leads to the consideration of similarity between conflicts, for which we formulate the notion of conflictsproximity as a similarity measure. We show that conflicts in mc decisions are more closely related than consecutive conflicts generated from sc decisions. Finally, we develop Common Reason Variable Reduction (CRVR) as a new decision strategy that reduces the selection priority of some variables from the learned clauses of mc decisions. Our empirical evaluation of CRVR implemented in three leading solvers demonstrates performance gains in benchmarks from the main track of SAT Competition-2020.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
