Adding a LBD-based rewarding mechanism in branching heuristic for SAT solvers
Wenjing Chang, Guanfeng Wu, Yang Xu · 2017
Decision heuristic strategy plays a critical role in DPLL-based propositional SAT solvers. Variable State Independent Decaying Sum (VSIDS) branching heuristic can be viewed as one of the most central features of state-of-the-art Conflict-Driven Clause-Learning (CDCL) SAT solvers. VSIDS consists of a rewarding mechanism for these variables participating in conflict. In this paper, we propose a new decision strategy - Rvar_LBD - extension of the rewarding mechanism by rewarding more variables that yield are involved in learnt clauses with small Literal Block Distance value, and implement it as part of Glucose3.0 solver. These empirical results further shed light on the proposed heuristic has the advantage of solving application and craft benchmarks from the SAT Competitions 2014 to 2016.