• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

Computer Engineering & Science

Previous Articles     Next Articles

A dynamic reward and punishment based branching
heuristic algorithm for CDCL SAT solvers

CHEN Xiulan,LIU Ting   

  1. (NationalLocal Joint Engineering Laboratory of System Credibility Automatic Verification,
    Southwest Jiaotong University,Chengdu 610031,China)
  • Received:2018-05-24 Revised:2018-07-13 Online:2019-03-25 Published:2019-03-25

Abstract:

Branching heuristic algorithms play an important role in CDCL SAT solvers, and the conventional branching heuristic algorithms are more concerned with the number of conflicts when calculating the activity scores of variables and do not consider the influence of the decision level or conflict decision level. In order to improve the efficiency of solving SAT problem, we propose a dynamic reward and punishment based branching method (DRPB), which is inspired by the EVSIDS and ACIDS. Whenever a conflict occurs, the DRPB updates the activity score of variables by integrating the numbers of conflicts, decision-making level, conflict decision level, and conflict frequency of variables. We improve the Glucose version 3.0 by replacing the VSIDS algorithm with the DRPB, and conduct an empirical evaluation not only on instances of SATLIB benchmarks, but also on 2015 and 2016 SAT competitions. Experimental results show that compared with the traditional and single variable branching heuristic algorithms, the proposed strategy can reduce the size of the search tree and improve the performance of the SAT solvers by reducing the branches of the search tree and the number of Boolean constraint propagation.

 

 

 

Key words: SAT problem, branching heuristic algorithm, VSIDS, decision level, conflict decision level, conflict frequency of variable