The conflict-index is the total number of conflicts that occurred so far。

variable bumping–

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 occurring in antecedents used to derive the learned clause through a regular input resolution chain [25] from existing clauses.

decision heuristic–

decision score、decision variable、dynamic decision heuristics

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

VSIDS (variable state independent decaying sum) 

CDCL (conflict-driven clause learning) 

ACIDS (average conflict-index decision score)

EVSIDS (exponential VSIDS),

VMTF (variable move-to-front) scheme   

normalized VSIDS (NVSIDS) [6], is an exponential moving average on how often a variable occurred in antecedents of learned clauses [6].

另：

clause move-to-front (CMTF)

binary decision diagrams (BDDs) [18]

first-order dynamic decision heuristics

second-order dynamic heuristics

phase saving [22]–

However, almost all modern CDCL solvers implement phase saving [22], which always reassigns the decision variable to the last phase it was previously assigned.

 关于EVSIDS 

Typical values for g are in the range of 1.01 to 1.2. Small values have been
shown to be useful for hard satisfiable instances (like cryptographic instances).
Large values are useful with very frequent restarts, particularly in combination
with the reuse-trail technique [28]. In Glucose 2.3, even without reusing the trail, it was thus suggested to slowly decrease g over time from a large value to a small one.1 In the (new) version of Lingeling used in our experiments, g is kept at 1.2.

关于VSIDS

VSIDS. The variable state independent decaying sum (VSIDS) of Chaff [5] maintains a variable score for each variable. The basic idea is that variables with large score are preferred decisions. 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. This process is also called variable rescoring.

 可以对照下表：

Variable scores play a role while (a) bumping variables participating in deriving
a learned clause, (b) deciding or searching for the next decision variable, (c)
unassigning variables during backtracking, (d) rescoring variable scores either
for explicit smoothing in VSIDS or due to protecting scores from overflow during
bumping, and (e) comparing past decisions on the trail to maximize trail
reuse [28].

First, we explain a fast implementation for VMTF, focusing on (a)-(c).

Next, we address its extension to precise scoring schemes using floating-point numbers, which in previous implementations followed the example set by MiniSAT to use a binary heap data structure.

Last, we discuss (d) and (e).

The reuse-trail optimization [28] is based on the following observation. After
a restart, it often happens that the same decisions are taken and the trail ends
up with the same assigned variables. Thus, the whole restart was useless.

By comparing scores of assigned previous decisions with the score of the next decision variable before restarting, this situation can be avoided. With some effort, this technique can be lifted to our generic queue implementation. To simplify the comparison in favor of a clean experiment, the results presented in Sect 4 are without reuse-trail (except for sc14ayv, the old 2014 version of Lingeling).

 实验提供的概况信息

（1）   

In our experiments in Sect. 4, the default decision heuristic (evsids in Tab. 2) bumped on average 276 literals per learned clause of average length 105 (on 275 considered instances).      ——学习子句平均长度为105，参与活跃度碰撞的变元平均为276个。

（2）

However, the number of propagated variables per decision can be quite large (on average, 323 propagations per decision for 275 benchmarks in the evsids column in Tab. 2). Removing them eagerly is too costly.——（采用EVSIDS决策策略）每次决策平均传播323个文字。

（3）

MiniSAT/Glucose use 10¹⁰⁰ as an upper score limit, which is only a slightly smaller maximum limit than ours 2⁵¹² ≈ 10154, but then does not use any truncation for small scores, which means that the minimum score exponent inMiniSAT is (roughly) 2⁻¹⁰. So Lingeling uses 9 bits for positive scores and 9 bits for negative scores, while MiniSAT uses slightly less than 9 bits for positives scores and (almost) full 10 bits for negative scores.

additive bumping and multiplicative decay

Conflict-Driven Clause-Learning (CDCL) SAT solvers crucially depend on the Variable State Independent Decaying Sum (VSIDS) branching heuristic for their performance. Although VSIDS was proposed nearly fifteen years ago, and many other branching heuristics for SAT solving have since been proposed, VSIDS remains one of the most effective branching heuristics. Despite its widespread use and repeated attempts to understand it, this additive bumping and multiplicative decay branching heuristic has remained an enigma.

——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. https://doi.org/10.1007/978-3-319-26287-1_14