摘要
工业SAT实例存在社区结构,而VSIDS和LRB未能有效利用这种结构。针对该问题,提出一种基于社区奖励的Cr分支优化算法。Cr算法的核心原理是增加相同社区变量的活性分数,以集中搜索局部解空间来降低重启和回溯成本,从而提高求解效率。首先依据社区中变量连接方式,将变量区分为桥变量和内变量,再根据社区中的变量将社区划分为3种类型。接着围绕变量和社区类型,尝试不同方法增加相同社区变量的活性分数。相同社区的判断依据当前社区的设置,而当前社区由活性最高的变量决定。变量类型和当前社区是Cr算法的2个关键因素,在Minisat、Maplesat和Glucose求解器的初步实验中,通过全局学习率GLR、提出的Incr序列和奖励因子α,分析了这3个因素对求解效率的影响。进一步地,依据分析结果在先进SAT求解器lstech_maple中应用Cr算法,实验表明利用社区结构可以有效提高先进SAT求解器的效率。为解释社区在冲突驱动子句学习CDCL搜索中可能起到的作用,提出社区连续指数CCI,并结合LBD解释社区的作用。
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.
作者
何飞
王晓峰
唐傲
彭庆媛
华盈盈
王军霞
HE Fei;WANG Xiaofeng;TANG Ao;PENG Qingyuan;HUA Yingying;WANG Junxia(School of Computer Science and Engineering,North Minzu University,Yinchuan 750021;The Key Laboratory of Images&Graphics Intelligent Processing of State Ethnic Affairs Commission,North Minzu University,Yinchuan 750021,China)
出处
《计算机工程与科学》
2026年第4期718-730,共13页
Computer Engineering & Science
基金
国家自然科学基金(62062001)
宁夏青年拔尖人才项目(2021)
北方民族大学研究生创新项目(YCX23153)。
关键词
布尔可满足性问题
冲突驱动子句学习
分支启发式
社区结构
boolean satisfiability problem
conflict-driven clause learning(CDCL)
branching heuristic
community structure
