TY - GEN
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.
UR - https://www.scopus.com/pages/publications/84951016535
U2 - 10.1007/978-3-319-24318-4_29
DO - 10.1007/978-3-319-24318-4_29
M3 - Conference proceedings
SN - 9783319243177
VL - 9340
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 405
EP - 422
BT - Theory and Applications of Satisfiability Testing – SAT 2015 - 18th International Conference, Proceedings
A2 - Heule, Marijn
A2 - Weaver, Sean
PB - Springer
ER -