Evaluating CDCL Variable Scoring Schemes

7 years 10 months ago
Evaluating CDCL Variable Scoring Schemes
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. 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.
Armin Biere, Andreas Fröhlich
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where SAT
Authors Armin Biere, Andreas Fröhlich
Comments (0)