VMTF(variable move-to-front )strategy学习

Posted 2021-03-02 yuweng1689

文献学习——Evaluating CDCL Variable Scoring Schemes

作者：Armin Biere ( B ) and Andreas Fröhlich    ------大牛，CaDiCal、YalSAT、Lingeling等求解器的研发团队负责人

这是作者2015年发表的文献，其中深入讲解了VMTF。该技术目前是应用求解unsat样例最有效，能多求出近10个。

 

VMTF最早见文献：

Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master’s thesis,
Simon Fraser University (2004)

---

 

Abstract.

The VSIDS (variable state independent decaying sum) decision heuristic invented in the context of the CDCL (conflict-driven clause
learning) SAT solver Chaff, is considered crucial for achieving high efficiency of modern SAT solvers on application benchmarks.

译文：VSIDS(可变状态独立衰减和)决策启发法是在冲突驱动子句学习SAT求解器的背景下发明的，它被认为是实现现代SAT求解器在应用基准上的高效率的关键。

This paper proposes ACIDS (average conflict-index decision score), a variant of VSIDS. The ACIDS heuristics is compared to the original implementation of VSIDS, its popular modern implementation EVSIDS (exponential VSIDS), the VMTF (variable move-to-front) scheme, and other related decision heuristics.

译文：本文提出了一种改进的方案——平均冲突指数决策得分。将ACIDS的启发法与vsid的原始实现进行比较，后者是流行的现代实现EVSIDS(指数级) VSIDS)、VMTF(变量前移)方案以及其他相关的决策启发法。

 

They all share the important principle to select those variables as decisions, which recently participated in conflicts. The main
goal of the paper is to provide an empirical evaluation to serve as a
starting point for trying to understand the reason for the efficiency of these decision heuristics.

译文：它们都有一个重要的原则，即选择那些最近参与冲突的变量作为决策。本文的主要目的是提供一个经验评估，作为一个起点，试图了解这些决策启发的效率的原因。

In our experiments, it turns out that EVSIDS, VMTF, ACIDS behave very similarly, if implemented carefully.

译文：在我们的实验中，结果表明EVSIDS、VMTF和酸的行为非常相似，如果仔细实施的话。

---

1 Introduction

VSIDS  ----- variable state independent decaying sum (VSIDS) decision heuristic。　　　　

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engi-
neering an efficient SAT solver. In: Proceedings of the 38th Design Automation
Conference, DAC 2001, pp. 530–535. ACM, Las Vegas, June 18–22, 2001

 

EVSIDS  -------    exponential VSIDS (EVSIDS)

Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Kleine
Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 28–33. Springer,
Heidelberg (2008)

 

The EVSIDS heuristic allows fast
selection of decision variables and adds focus to the search, but also is able to pick
up long-term trends due to a “smoothing” component, as argued in [6].

译文：EVSIDS启发式允许快速选择决策变量，并将重点添加到搜索中，但也能够通过“平滑”组件获取长期趋势，如[6]中所述。

 

On the practical side, there have been various attempts to improve on the
EVSIDS scheme. These include the variable move-to-front (VMTF) strategy
of the Siege SAT solver [8], the BerkMin strategy [9], which is focusing on
recently learned clauses, and the clause move-to-front (CMTF) strategies of
HaifaSAT [10] and PrecoSAT [11].

译文：在实践方面，已经有各种改进的尝试EVSIDS方案。这些策略包括围攻卫星解算器[8]的可变移动到前线(VMTF)策略，BerkMin策略[9]，它关注于最近学习的子句，以及子句移动到前线(CMTF)策略HaifaSAT[10]和PrecoSAT[11]。

 

 VMTF  ------  variable move-to-front (VMTF) strategy

Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master’s thesis,
Simon Fraser University (2004)。

 

 CMTF  -------  the clause move-to-front (CMTF) strategie

　　　　对应于两类求解器HaifaSAT [10] and PrecoSAT [11]

 

ACIDS  ------  本文提出的策略 average conflict-index decision score (ACIDS)

 

---

 

2.Decision Heuristics

本节将变元决策各种策略的来龙去脉讲的非常清楚。

 

知识点1：决策启发式可以转变为变量选择启发式

Modulo initialization, typically based on (one-sided)
Jeroslow-Wang’s heuristic [20], phase saving turns the decision heuristic into a
variable selection heuristic.

译文：模块化初始化、通常基于(单侧)Jeroslow-Wang的启发式[20]和相位保持三项技术的成熟，使得决策启发式可以转变为变量选择启发式。

 

Accordingly, we focus on variable selection, which in
turn will be based on selecting a variable with the highest decision score.

译文：因此，我们将重点放在变量选择上，而变量选择将基于选择具有最高决策得分的变量

 

知识点2：

The original VSIDS implementation in Chaff
worked as follows：

Variables are stored in an array used to search for a decision
variable. After learning a clause, the score of its variables is incremented. Further,
every 256th conflict, all variable scores are divided by 2, and the array is sorted
w.r.t. decreasing score.

译文：变量存储在一个数组中，用于搜索决策变量。在学习了一个子句之后，它的变量得分会增加。此外，每256次冲突，所有变量得分除以2，数组按w.r.t递减排序。

 

The process of updating scores of variables is also referred to as variable bumping [7].

Note, however, that in modern solvers and also in our experiments
we not only bump variables of the learned clause, but all seen variables occur-
ring in antecedents used to derive the learned clause through a regular input
resolution chain [25] from existing clauses.

译文：然而，请注意，在现代的求解程序中，以及在我们的实验中，我们不仅碰撞了习得子句的变量，而且所有可见的变量都发生了—通过现有子句的常规输入解析链[25]派生习得子句的先行词中的环

 

An essential optimization in Chaff
is to cache the position of the last found decision variable with maximum score
in the ordered array.

译文：Chaff的一个基本优化是将最后一个找到的决策变量的位置与最大得分一起缓存到有序数组中。

知识点3：

增加变量得分与增加学习子句参与冲突索引的次数

INC (or inc in the experiments)

SUM (or sum in our experiments)

The decide procedure selects the next decision variable, by searching for the
first unassigned variable in the ordered array, starting at the lower end, e.g., the
variable with the highest score during sorting. An essential optimization in Chaff
is to cache the position of the last found decision variable with maximum score
in the ordered array. This position is used as starting point for the next search. If
a variable in the array with a position smaller than the cached maximum score
position becomes unassigned then the maximum score position is updated to
that position. During rescoring, similar updates might be necessary.

The first part of VSIDS, e.g., only incrementing scores, constitutes an approx-
imation of dynamic DLIS. It counts occurrences of variables in clauses, ignor-
ing whether a clause is satisfied or not, or even removed during learned clause
deletions [3] (called clause database reduction in the following). This restricted
version of VSIDS without smoothing is denoted INC (or inc in the experiments).

As an alternative to using frequent rescoring, we propose that the smoothing
part of VSIDS can also be approximated by adding the conflict-index to the score
instead of just incrementing it. The conflict-index is the total number of conflicts
that occurred so far. We call this scheme SUM (or sum in our experiments).

 

知识点4：EVSIDS.

 

知识点5：VMTF

 

知识点6：ACIDS

 

 

---

 

3.VMTF

 

 

---