Armin Biere, Andreas Fröhlich,
"Evaluating CDCL Variable Scoring Schemes"
: Proc. 18th Intl. Conf. on Theory and Applications of Satisfiability Testing, Serie Lecture Notes in Computer Science (LNCS), Vol. 9340, Springer, Seite(n) 405-422, 2015
Original Titel:
Evaluating CDCL Variable Scoring Schemes
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 18th Intl. Conf. on Theory and Applications of Satisfiability Testing
Original Kurzfassung:
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.