文献学习——A Deep Dive into Conflict Generating Decisions

Abstract.

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. CDCL中的选择启发式方法优先考虑最近冲突中涉及的变量。虽然只有一小部分决策会产生冲突，但很多决策会产生多重冲突。

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.

译文：我们还展示了在同一个mc决策中学习的连续子句之间的重要联系，其中一个学习到的子句触发下一个子句的学习，形成一个子句链。

译文：这导致我们考虑冲突之间的相似性，为此我们制定了冲突邻近性的概念作为相似性度量。

译文：最后，我们提出了公共原因变量约简(CRVR)作为一种新的决策策略，从mc决策的学习子句中降低一些变量的选择优先级。

1 Introduction

 ......

The clause learning process in CDCL can generate more than one conflict for one decision. In the following, we categorize each conflict-producing decision as a single conflict (sc) or a multi-conflicts (mc) decision, depending on whether it produces one, or more than one, conflict. We label the resulting learned clauses sc and mc clauses accordingly.

译文：CDCL中的子句学习过程可以为一个决策产生多个冲突。在下面，我们将每个产生冲突的决策分类为单个冲突(sc)或多个冲突(mc)决策，这取决于它是产生一个还是多个冲突。我们将得到的学习到的从句相应地标记为sc和mc从句。

Conflicts play a crucial role in CDCL search. A better understanding of conflict generating decisions is a step towards a better understanding of CDCL and may open up new directions to improve CDCL search. Motivated by this, here we study conflict producing decisions in CDCL. The contributions of this work are:

译文：冲突在CDCL搜索中起着关键作用。更好地理解冲突生成决策是更好地理解CDCL的一步，并可能为改进CDCL搜索开辟新的方向。基于此，本文研究了CDCL中的冲突产生决策。这项工作的贡献是: