-
题名SAT问题求解器重启策略对比分析
被引量：2
- 1
-
-
作者
郭莹
张斌
张长胜
-
机构
东北大学信息科学与工程学院
宁夏理工学院电气信息工程学院
-
出处
《小型微型计算机系统》
CSCD
北大核心
2013年第12期2729-2733,共5页
-
基金
国家教育部少数民族高级骨干人才培养基金项目(教民[2008-8])资助
国家自然科学基金项目(61073062
+1 种基金
61100090)资助
东北大学中央高校基本科研业务费项目(N11024006)资助
-
文摘
已有研究表明,在SAT求解器中引入重启可以极大地提高求解性能,并已出现了许多不同重启策略.目前还缺少全面的对比分析研究.为了避免重启策略选择的随意性,同时启发设计更好的重启策略,本文选择了具有代表性的7种重启策略,以目前广泛采用的Minisat为基本求解器,在国际SAT2011竞赛中实际应用类基准测试集之上进行了实验对比分析.结果表明:(1)不同重启策略对SAT求解器的求解过程和求解性能影响巨大;(2)在应用类测试集上,几何序列调度策略的平均综合性能优于其他策略;(3)在限定范围内,重启频率越大,求解器综合性能越好;(4)增量变化的重启频率可以克服固定重启频率导致不完备搜索的问题.
-
关键词
可满足性问题
求解器
冲突驱动子句学习
重启策略
-
Keywords
satisfiability problem
solver
conflict-driven clause learning
restart strategy
-
分类号
TP18
[自动化与计算机技术—控制理论与控制工程]
-
-
题名基于社区结构的CDCL启发式算法
- 2
-
-
作者
何飞
王晓峰
唐傲
彭庆媛
华盈盈
王军霞
-
机构
北方民族大学计算机科学与工程学院
-
出处
《计算机工程与科学》
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
[自动化与计算机技术]
-
-
题名基于演绎长度的学习子句删除策略
被引量：3
- 3
-
-
作者
常文静
徐扬
吴贯锋
-
机构
西南交通大学信息科学与技术学院
系统可信性自动验证国家地方联合工程实验室
西南交通大学数学学院
-
出处
《计算机工程与应用》
CSCD
北大核心
2018年第16期30-36,共7页
-
基金
国家自然科学基金(No.61673320)
中央高校基本科研业务费专项资金(No.2682018ZT10)
-
文摘
学习子句删除策略是CDCL-SAT求解器中的一个重要内容,可以避免内存爆炸和加速单元传播。评估学习子句有用性的标准不同导致所删除的学习子句是不同的,极大地影响求解效率。基于CDCL算法的求解过程可被形式化为增加管理学习子句策略的归结演绎过程,基于此,提出一种基于演绎长度的学习子句评估方法,并与现有的基于文字块距离的评估方法结合,根据排序子句的基准不同,形成两种不同的结合算法。采用国际SAT竞赛的基准实例,与目前主流的求解器进行了实验对比分析。结果表明,所提的结合算法能更好地评估学习子句的有用性,较基于文字块距离策略的求解个数提高了4.1%,说明所提策略具有一定的优势。
-
关键词
可满足性问题
冲突驱动子句学习
学习子句删除
演绎长度
-
Keywords
satisfiability problem
conflict driven clause learning
learned clauses reduction
length of deduction
-
分类号
TP311.1
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种基于识别重复路径的动态决策策略
被引量：3
- 4
-
-
作者
常文静
徐扬
-
机构
西南交通大学信息科学与技术学院
西南交通大学数学学院
系统可信性自动验证国家地方联合工程实验室
-
出处
《计算机学报》
EI
CSCD
北大核心
2019年第10期2309-2322,共14页
-
基金
国家自然科学基金（61673320）
中央高校基本科研业务费基金(2682018ZT10）资助~~
-
文摘
在现有基于冲突学习子句的求解器中,重启和变量相位存储技术的频繁应用,导致重启之后产生大量重复变量赋值序列,在求解过程中对变量重复赋值会浪费求解资源.本文提出一种基于识别重复路径的动态决策策略.首先,检测搜索过程中产生的重复赋值变量序列,算法中参数依据子句数与变元数的比率而动态变化;其次,更新参与冲突次数最多的变量的活跃值,选择合适的分支决策变量,改变变量赋值序列.本文基于国际SAT竞赛中知名求解器Glucose3.0,MapleCOMSPS,Glucose4.1以及Lingeling,分别实现了改进算法——DDIDT.实验结果可得,改进求解器Glucose_DDIDT相比Glucose3.0降低决策数为11.2%~61.6%,且Glucose_DDIDT求解难度较大实例的个数提高了63.9%.针对求解2015年到2017年SAT竞赛的应用类型的实例,Glucose_DDIDT相比Glucose3.0的求解个数增长了6.0%;改进求解器MapleCOMSPS_DDIDT相比MapleCOMSPS求解个数提高了2.5%;相比Glucose4.1,改进求解器Glucose4.1_DDIDT的求解个数增长了3.1%;虽然Lingeling_DDIDT求解实例总数相比Lingeling只增加1个,但求解时间有所减少.实验表明,所提策略可有效识别重复路径,适时选择合适的分支决策变量,改变搜索路径,减少计算时间.
-
关键词
可满足问题
冲突驱动学习子句
重启
分支决策策略
重复赋值序列
-
Keywords
satisfiability problem
conflict driven clause learning
restart
branching decision strategy
duplicate trail
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名基于变量混合特征的分支启发式策略
被引量：2
- 5
-
-
作者
艾森阳
宋振明
沈雪
-
机构
西南交通大学数学学院
西南交通大学系统可信性自动验证国家地方联合工程实验室
-
出处
《计算机系统应用》
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
[自动化与计算机技术—计算机系统结构]
-
-
题名基于回跳层数的SAT求解器学习子句删除策略
被引量：1
- 6
-
-
作者
沈雪
陈树伟
徐扬
吴贯锋
-
机构
西南交通大学数学学院
西南交通大学信息科学与技术学院
系统可信性自动验证国家地方联合工程实验室
-
出处
《计算机应用研究》
CSCD
北大核心
2020年第11期3316-3320,共5页
-
基金
国家自然科学基金资助项目(61673320)
中央高校基本科研业务费专项资金资助项目(2682018ZT10,2682018CX59)。
-
文摘
目前学习子句删除策略广泛采用的是基于LBD的评估方式,LBD评估方式在每次执行删除时都会删除前一半LBD值大的学习子句,这种方式对LBD值大的学习子句的删除过于激进。针对此问题,提出了一种利用冲突回跳层数(back-jump levels)的评估方式来保留LBD值较大的有用学习子句。以CDCL(conflict driven clause learning)完备算法为框架,在子句删除环节形成了BJL删除算法。通过测试2017年SAT国际竞赛例,对新改进的版本与原版求解器进行了对比实验。实验表明,所提策略可显著提高求解器的求解性能和求解效率。
-
关键词
可满足性问题
冲突驱动子句学习
LBD
回跳层数
-
Keywords
satisfiability problem
conflict driven clause learning
literal block distance(LBD)
back-jump levels
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-
-
题名基于奖励机制的SAT求解器分支策略
被引量：2
- 7
-
-
作者
沈雪
陈树伟
艾森阳
-
机构
西南交通大学数学学院
系统可信性自动验证国家地方联合工程实验室
-
出处
《计算机科学》
CSCD
北大核心
2020年第7期42-46,共5页
-
基金
国家自然科学基金(61673320)
中央高校基本科研业务费专项资金(2682018ZT10,2682018CX59)。
-
文摘
分支决策是CD CL(Conflict Driven Clause Learning)求解器一个十分关键的环节,一个好的分支策略可以减少分支决策次数进而提高SAT求解器的效率。目前,先进的分支策略大都结合了冲突分析过程,但分支策略对参与冲突分析的变量奖励方法有所不同,因此所挑选出的决策变量会有所差异。文中考虑到决策变量总是在未赋值变量中选取的这一重要事实,在EVSIDS(Exponential Variable State Independent Decaying Sum)分支策略的基础上提出了一种新的分支策略,称为基于奖励机制的分支策略(简称RACT分支策略)。RACT分支策略对冲突分析中被撤销赋值的变量再次给予奖励,以增大未赋值变量中频繁参与冲突分析的变量被选择为分支变量的可能性。最后,将所提出的分支策略嵌入到Glucose4.1求解器中以形成新的求解器Glucose4.1+RACT,以2017年SAT竞赛中的350个实例为实验数据集来测试RACT分支策略的有效性。实验结果表明,求解器Glucose4.1+RACT比原版求解器能求解出更多的实例个数,尤其在求解可满足实例的个数上增加了13.5%,此外在求解350个竞赛实例上所花费的总时间较Glucose4.1减少了3.9%,以上实验数据均说明所提分支策略可以有效减少搜索树的分支决策次数并给出正确的搜索空间,进而提高了SAT求解器的求解能力。
-
关键词
可满足性问题
完备算法
冲突驱动子句学习
回溯搜索
分支策略
-
Keywords
Satisfiability problem
Complete algorithms
conflict driven clause learning
Backtrack search
Branching strategy
-
分类号
TP181
[自动化与计算机技术—控制理论与控制工程]
-
-
题名基于近期文字极性分配的学习子句评估算法
- 8
-
-
作者
冯心妍
吴贯锋
张丁荣
王恪铭
-
机构
西南交通大学信息科学与技术学院
西南交通大学系统可信性自动验证国家地方联合工程实验室
西南交通大学数学学院
西南交通大学计算机与人工智能学院
-
出处
《计算机工程与科学》
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
[自动化与计算机技术—计算机应用技术]
-
