TY - CHAP
T1 - Evaluating CDCL Variable Scoring Schemes
AU - Biere, Armin
AU - Fröhlich, Andreas
PY - 2015
Y1 - 2015
N2 - 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. 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. 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.
AB - 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. 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. 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.
M3 - Chapter
VL - 9340
T3 - Lecture Notes in Computer Science (LNCS)
SP - 405
EP - 422
BT - Proc. 18th Intl. Conf. on Theory and Applications of Satisfiability Testing
PB - Springer
ER -