关键词: 布尔可满足性问题, 冲突驱动子句学习, 分支启发式, 社区结构

Abstract: Due to the presence of community structures in industrial SAT (satisfiability) instances, both the variable state independent decaying sum(VSIDS) and learning rate branching (LRB) heuristics fail to effectively leverage such structures. To address this issue, a branch optimization algorithm based on community reward, namely Cr, is proposed. The core principle of the Cr algorithm is to increase the activity scores of variables within the same community, thereby focusing the search on local solution spaces to reduce restart and backtracking costs, ultimately improve solving efficiency. Firstly, variables are classified into bridge variables and internal variables based on their connectivity within the community. Subsequently, communities are categorized into three types according to the variables they contain. Then, focusing on variable types and community types, different approaches are explored to increase the activity scores of variables within the same community. The determination of whether variables belong to the same community is based on the current community settings, which is in turn determined by the variable with the highest activity scores. Variable types and the current community are two key factors in the Cr algorithm. In preliminary experiments using the Minisat, Maplesat, and Glucose solvers, the impact of these two factors on solving efficiency was analyzed through the global learning rate (GLR), the Incr sequence, and the reward factor α proposed in this paper. Furthermore, based on the analysis results, the Cr algorithm was applied to the advanced SAT solver lstech_maple. Experiments demonstrate that leveraging community structures can effectively enhance the efficiency of advanced SAT solvers. To explain the potential role of communities in conflict-driven clause learning(CDCL) search, the community continuity index (CCI) is proposed, and its role is interpreted in conjunction with the literal block distance (LBD) metric.

Key words: boolean satisfiability , problem;conflict-driven clause learning(CDCL);branching heuristic;community structure