sat求解器是一个大数据系统

Posted 2021-03-01 海阔凭鱼跃越

Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers

• Jia Hui Liang
• Vijay Ganesh
• Ed Zulkoski
• Atulan Zaman
• Krzysztof Czarnecki

Liang J.H., Ganesh V., Zulkoski E., Zaman A., Czarnecki K. (2015) Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers. In: Piterman N. (eds) Hardware and Software: Verification and Testing. HVC 2015. Lecture Notes in Computer Science, vol 9434. Springer, Cham

 

---

7 Interpretation of Results

We began our research by posing a series of questions regarding VSIDS, and we now interpret the results obtained in light of these questions.

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

（1）What is special about the class of variables that VSIDS chooses to additively bump? 译文：vsid选择的这类变量有什么特别之处?

 In the bridge variables experiment (Sect. 3), we showed that VSIDS disproportionately favored bridge variables.

译文：在桥变量实验(第3节)中，我们发现vsid对桥变量的偏爱程度非常高。

 

Even though SAT instances have large number of bridge variables on average, the frequency with which VSIDS picks, bumps, and learns bridge variables is much higher.

译文：尽管SAT实例平均有大量的桥接变量，但是VSIDS挑选、碰撞和学习桥接变量的频率要高得多。

 

There is no a priori reason to believe that VSIDS would behave like this. This surprising result, plus a previous result that good community structure correlates with faster solving time [38], suggests CDCL solvers exploit community structure.

译文：这个令人惊讶的结果，加上之前的一个结果，即良好的社区结构与更快的解决时间[38]相关，表明CDCL求解者利用了社区结构。

 

More precisely, they target variables linking distinct communities, possibly as a way to solve by divide-and-conquer approach.

译文：更准确地说，他们的目标是连接不同社区的变量，这可能是采用分治法解决问题的一种方法。

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

In the VSIDS vs. TGC experiments (Sect. 4), we used the Spearman’s rank correlation coefficient to show that the VSIDS and TGC rankings are strongly correlated.

译文：在VSIDS与TGC的实验中(第4节)，我们使用Spearman的等级相关系数来表明VSIDS与TGC的等级具有很强的相关性。

 

From our experiments, we can say that for all the VSIDS variants considered in this paper, additive bumping matches with the increase in centrality of the chosen variables.

译文：从我们的实验中可以看出，对于本文考虑的所有VSIDS变量，加性凸点都与所选变量中心性的增加相匹配。

 

We also observe from our results that the variables that solvers pick for branching have very high TGC rank. The concept of centrality allows us to define in a mathematically precise the intuition many solver developers have had, i.e., that branching on “highly constrained variables” is an effective strategy.

译文：我们还从结果中观察到，求解者为分支选择的变量具有非常高的TGC秩。中心性的概念允许我们以精确的数学方式定义许多求解程序开发人员具有的直觉，即，在“高度约束变量”上进行分支是一种有效的策略。

 

Our bridge variable experiment combined with the TGC experiment suggests that VSIDS focuses on high-centrality bridge variables.

译文：我们的桥梁变量实验结合TGC实验表明，vsid侧重于高中心性桥梁变量。

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

 （2）What role does multiplicative decay play in making VSIDS so effective?译文：在使vsid如此有效的过程中，乘法衰减起了什么作用?

(Answered by Contribution IV, that in turn led to a new adaptive VSIDS presented as Contribution V.) We show that multiplicative decay is essentially a form of exponential smoothing (Sect. 5).

译文：我们证明了乘法衰减本质上是指数平滑的一种形式(第五节)。

 

We add an explanation as to why this is important, namely, that exponential smoothing favors variables that persistently occur in conflicts and this is a better strategy for root-cause analysis.

译文：我们增加了一个解释，为什么这是重要的，即，指数平滑有利于在冲突中持续发生的变量，这是一个更好的策略，为根源分析。

 

We designed a new VSIDS technique, we call adaptVSIDS, based on the above results, wherein we rapidly decay the VSIDS activity if the learnt clause LBDs are large (Sect. 6). We showed that this technique is better than mVSIDS on the SAT Competition 2013 benchmark.

译文：根据以上结果，如果所学习的子句LBDs较大，则VSIDS活性迅速衰减。

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

（3）Is VSIDS temporally and spatially focused? (Answered by Contribution II.)译文：vsid是否关注时间和空间?

We show that VSIDS exhibits spatial focus and temporal focus (Sect. 3), forms of locality in search. While there has been speculation among solver researchers that CDCL with VSIDS solvers perform local search, we precisely define spatial and temporal locality in terms of the community structure.

译文：我们发现VSIDS表现出空间焦点和时间焦点(第3节)，即搜索的局部性形式。虽然有研究者推测CDCL和VSIDS求解器执行局部搜索，但我们根据群落结构精确地定义了空间和时间上的局部性。

---

 

8 Related Work

Marques-Silva and Sakallah are credited with inventing the CDCL technique [34]. The original VSIDS heuristic was invented by the authors of Chaff [36].

Armin Biere [8] described the low-pass filter behavior of VSIDS, and Huang et al. [26] stated that VSIDS is essentially an EMA.

译文：Armin Biere[8]描述了VSIDS的低通滤波行为，Huang等人[26]认为VSIDS本质上是EMA（指数移动平均）

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Katsirelos and Simon [30] were the first to publish a connection between eigenvector centrality and branching heuristics. In their paper [30], the authors computed eigenvector centrality (via Google PageRank) only once on the original input clauses and showed that most of the decision variables have higher than average centrality.

译文：Katsirelos和Simon[30]首先发表了特征向量中心性和分支启发法之间的联系。

译文：作者对原始输入子句仅计算了一次特征向量中心性(通过谷歌PageRank)，结果表明大多数决策变量的中心性高于平均中心性。

 

Also, it bears stressing that their definition of centrality is not temporal. By contrast, our results correlate VSIDS ranking with temporal degree and eigenvector centrality, and show the correlation holds dynamically throughout the run of the solver.

译文：此外，它还需要强调，它们对中心性的定义不是暂时的。

译文：我们的结果将vsid排序与时间度和特征向量的中心性联系起来，并在整个求解过程中动态地展示了相关性。

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Also, we noticed that the correlation is also significantly stronger after extending centrality with temporality. Simon and Katsirelos do hypothesize that VSIDS may be picking bridge variables (they call them fringe variables). However, they do not provide experimental evidence for this.

译文：此外，我们注意到，在将中心性与时间性延长后，相关性也显著增强。Simon和Katsirelos假设vsid可能会选择桥接变量(他们称之为边缘变量)。然而，他们并没有为此提供实验证据。

To the best of our knowledge, we are the first to establish the following results regarding VSIDS: first, VSIDS picks, bumps, and learns high-centrality bridge variables; second, VSIDS-influenced search is more spatially and temporally focused than other branching heuristics we considered; third, explain the importance of EMA (multiplicative decay) to the effectiveness of VSIDS; and fourth, invent a new adaptive VSIDS branching heuristic based on our observations.

译文：据我们所知，我们首先确定了关于vsid的下列结果:

译文：首先，vsid挑选、颠簸和学习高中心性桥接变量;

译文：其次，与我们考虑的其他分支启发法相比，受vsid影响的搜索更关注空间和时间;

译文：第三，解释EMA(乘法衰减)对vsid有效性的重要性（本质上是指数平滑的一种形式）；

译文：基于我们的观察，发明一种新的自适应vsid分支启发法。