-
题名求解QBF问题的启发式调查传播算法
被引量：11
- 1
-
-
作者
殷明浩
周俊萍
孙吉贵
谷文祥
-
机构
东北师范大学计算机学院
吉林大学教育部符号计算与知识工程重点实验室
吉林大学计算机科学与技术学院
-
出处
《软件学报》
EI
CSCD
北大核心
2011年第7期1538-1550,共13页
-
基金
国家自然科学基金(60773097
60803102)
-
文摘
提出了一种启发式调查传播算法,并基于该算法设计了一种QBF(quantified Boolean formulae)求解器——HSPQBF(heuristic survey propagation algorithm for solving QBF)系统.它将Survey Propagation信息传递方法应用到QBF求解问题中.利用Survey Propagation作为启发式引导DPLL(Davis,Putnam,Logemann and Loveland)算法,选择合适的变量进行分支,从而可以减小搜索空间,并减少算法回退的次数.在分支处理过程中,HSPQBF系统结合了单元传播、冲突学习和满足蕴涵学习等一些优秀的QBF求解技术,从而能够提高QBF问题的求解效率.实验结果表明,HSPQBF无论在随机问题上还是在QBF标准测试问题上都有很好的表现,验证了调查传播技术在QBF问题求解中的实际价值.
-
关键词
人工智能
QBF问题
QBF问题求解器
因子图
调查传播
冲突学习
满足蕴涵学习
-
Keywords
artificial intelligence
quantified Boolean formulae problem
QBF（quantified Boolean formulae）solver
factor graph
survey propagation
conflict driven learning
satisfiability directed implicationand learning
-
分类号
TP181
[自动化与计算机技术—控制理论与控制工程]
-
-
题名基于演绎长度的学习子句删除策略
被引量：3
- 2
-
-
作者
常文静
徐扬
吴贯锋
-
机构
西南交通大学信息科学与技术学院
系统可信性自动验证国家地方联合工程实验室
西南交通大学数学学院
-
出处
《计算机工程与应用》
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
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种基于识别重复路径的动态决策策略
被引量：2
- 3
-
-
作者
常文静
徐扬
-
机构
西南交通大学信息科学与技术学院
西南交通大学数学学院
系统可信性自动验证国家地方联合工程实验室
-
出处
《计算机学报》
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
[自动化与计算机技术—计算机系统结构]
-
-
题名SAT问题求解器重启策略对比分析
被引量：2
- 4
-
-
作者
郭莹
张斌
张长胜
-
机构
东北大学信息科学与工程学院
宁夏理工学院电气信息工程学院
-
出处
《小型微型计算机系统》
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
[自动化与计算机技术—控制理论与控制工程]
-
-
题名基于奖励机制的SAT求解器分支策略
被引量：1
- 5
-
-
作者
沈雪
陈树伟
艾森阳
-
机构
西南交通大学数学学院
系统可信性自动验证国家地方联合工程实验室
-
出处
《计算机科学》
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
[自动化与计算机技术—控制理论与控制工程]
-
-
题名基于回跳层数的SAT求解器学习子句删除策略
- 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
[自动化与计算机技术—计算机应用技术]
-
-
题名基于近期文字极性分配的学习子句评估算法
- 7
-
-
作者
冯心妍
吴贯锋
张丁荣
王恪铭
-
机构
西南交通大学信息科学与技术学院
西南交通大学系统可信性自动验证国家地方联合工程实验室
西南交通大学数学学院
西南交通大学计算机与人工智能学院
-
出处
《计算机工程与科学》
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
[自动化与计算机技术—计算机科学与技术]
-
