A New Rewarding Mechanism for Branching Heuristic in SAT Solvers

DOI

10.2991/ijcis.2019.125905649How to use a DOI?

Keywords

Satisfiability problem; Conflict-driven clause learning; Branching heuristic; Literal block distance

Abstract

Decision heuristic strategy can be viewed as one of the most central features of state-of-the-art conflict-driven clause-learning SAT solvers. Variable state independent decaying sum (VSIDS) still is the dominant branching heuristics because of its low cost. VSIDS consists of a rewarding mechanism for variables participating in the conflict. This paper proposes a new rewarding mechanism for branching strategy, rewarding variables differently depended on information provided by the conflict analysis process, that is to say, the literal block distance value of the learnt clause and the size of the backtrack level decided by the learnt clause. We implement it as part of the Glucose 3.0 solver and MapleCOMSPS solver. Compared with Glucose 3.0, the number of solved instances of the improved Glucose_LBD + BTL is enhanced by 6.0%; compared with MapleCOMSPS, the number of solved instances of MapleCOMSPS_LBD + BTL is added by 3.4%. These empirical results further shed light on the proposed heuristic having the advantage of solving Application benchmark from the SAT Competitions 2015–2017.

Copyright

© 2019 The Authors. Published by Atlantis Press SARL.

Open Access

This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)
View full text (HTML)

TY  - JOUR
AU  - Wenjing Chang
AU  - Yang Xu
AU  - Shuwei Chen
PY  - 2019
DA  - 2019/01/28
TI  - A New Rewarding Mechanism for Branching Heuristic in SAT Solvers
JO  - International Journal of Computational Intelligence Systems
SP  - 334
EP  - 341
VL  - 12
IS  - 1
SN  - 1875-6883
UR  - https://doi.org/10.2991/ijcis.2019.125905649
DO  - 10.2991/ijcis.2019.125905649
ID  - Chang2019
ER  -