A branching heuristic based on variable decision levels
Zhonghe Du, Zhenming Song · 2017
Efficient branching heuristic is a key feature of modern SAT solvers. Firstly, this paper introduced VSIDS heuristic and VSIDS-based heuristics like EVSIDS and ACIDS. Based on VSIDS, a new heuristic termed DLBH that considers variable decision levels was proposed to promote the efficiency of variable selection process. Then, instances showed the comparison among EVSIDS, ACIDS and DLBH. Finally, experimental results indicated that MiniSat solver with DLBH outperforms solvers MiniSat with VSIDS and Glucose.