-
题名基于社区结构的CDCL启发式算法
- 1
-
-
作者
何飞
王晓峰
唐傲
彭庆媛
华盈盈
王军霞
-
机构
北方民族大学计算机科学与工程学院
-
出处
《计算机工程与科学》
2026年第4期718-730,共13页
-
基金
国家自然科学基金(62062001)
宁夏青年拔尖人才项目(2021)
北方民族大学研究生创新项目(YCX23153)。
-
文摘
工业SAT实例存在社区结构,而VSIDS和LRB未能有效利用这种结构。针对该问题,提出一种基于社区奖励的Cr分支优化算法。Cr算法的核心原理是增加相同社区变量的活性分数,以集中搜索局部解空间来降低重启和回溯成本,从而提高求解效率。首先依据社区中变量连接方式,将变量区分为桥变量和内变量,再根据社区中的变量将社区划分为3种类型。接着围绕变量和社区类型,尝试不同方法增加相同社区变量的活性分数。相同社区的判断依据当前社区的设置,而当前社区由活性最高的变量决定。变量类型和当前社区是Cr算法的2个关键因素,在Minisat、Maplesat和Glucose求解器的初步实验中,通过全局学习率GLR、提出的Incr序列和奖励因子α,分析了这3个因素对求解效率的影响。进一步地,依据分析结果在先进SAT求解器lstech_maple中应用Cr算法,实验表明利用社区结构可以有效提高先进SAT求解器的效率。为解释社区在冲突驱动子句学习CDCL搜索中可能起到的作用,提出社区连续指数CCI,并结合LBD解释社区的作用。
-
关键词
布尔可满足性问题
冲突驱动子句学习
分支启发式
社区结构
-
Keywords
boolean satisfiability problem
conflict-driven clause learning(cdcl)
branching heuristic
community structure
-
分类号
TP301.6
[自动化与计算机技术]
-
-
题名基于变量混合特征的分支启发式策略
被引量：2
- 2
-
-
作者
艾森阳
宋振明
沈雪
-
机构
西南交通大学数学学院
西南交通大学系统可信性自动验证国家地方联合工程实验室
-
出处
《计算机系统应用》
2020年第3期200-205,共6页
-
基金
国家自然科学基金(61673320)。
-
文摘
先进的SAT求解器能够通过有效的分支启发式策略解决大型应用实例.目前VSIDS策略是最具有代表性的基于冲突分析的分支策略,它因其稳健性而被广泛使用,但在每次冲突分析中其判定变量活性的增量方式过于单一.针对此问题,本文提出了一种基于变量混合特征的分支启发式算法,目的是充分地利用参与冲突分析的变量所携带的不同信息特征来区分变量,来进一步指导变量活性增长.并将所提出的分支策略算法嵌入到Glucose4.1中形成求解器Glucose4.1+MFBS,通过对比测试,实验结果表明改进的分支算法比原本的VSIDS策略,具有一定的优势,求解明显个数增加.
-
关键词
SAT问题
cdcl算法
分支启发式
冲突分析
学习子句
-
Keywords
SAT problem
cdcl algorithm
branch heuristic
conflict analysis
learning clause
-
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
-
-
题名基于近期文字极性分配的学习子句评估算法
- 3
-
-
作者
冯心妍
吴贯锋
张丁荣
王恪铭
-
机构
西南交通大学信息科学与技术学院
西南交通大学系统可信性自动验证国家地方联合工程实验室
西南交通大学数学学院
西南交通大学计算机与人工智能学院
-
出处
《计算机工程与科学》
CSCD
北大核心
2023年第11期1941-1948,共8页
-
基金
国家自然科学基金(62106206)。
-
文摘
为了维护学习子句数据库的大小,并以合理的成本执行单元传播,在SAT求解器求解过程中需要对学习子句进行评估,从而删除对求解过程无用的子句。因此,需要对学习子句数据库进行动态管理,包含对学习子句的分析和删除等,并提出新的评估子句有用性的方法,从而保留对求解最有促进作用的学习子句,以提高求解效能。从捕获学习子句近期的极性分配出发,结合现代求解器的回溯环节中常用到的基于字面极性的启发式方法——进度节省,来推断给定学习子句与剩余搜索步骤的相关性。以最先进的2种基于冲突驱动子句学习算法CDCL的求解器Glucose和MapleLCMDistChronoBT求解器为基准,针对其在子句评估环节的算法进行改进测试。实验结果表明,这种基于近期文字极性分配的子句评估策略能够普遍提高CDCL串行和并行求解器的求解效率,有效改善了原有求解器在一些问题上求解耗时过长的问题,并在先进求解器的水平上多求解了2个合取范式CNF文件,单个文件的平均求解时间缩短了13~34 s。
-
关键词
SAT问题
子句评估策略
cdcl
学习子句
-
Keywords
SAT problem
clause evaluation strategy
conflict driven clause learning(cdcl)
learnt clause
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
TP391
[自动化与计算机技术—计算机应用技术]
-
