基于增量式的#sat求解算法研究

《基于增量式的#sat求解算法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、＂、．、；学校代码：２０１３１０２４８５：１０２００研究生学号聲分类号；ＩＭ密级：丞Ｉ：５、驚議蟲Ｉ芭：＇《批坤么夫多．ｔｆｉｉＰ硕±学位论文每心蒂－节：；；＾；？？．ａ？．－ｖ．；ｆ基于増？式的＃ＳＡＴ歌３？其法巧巧：京、＼、、一．＊？、＊＾ＲｅｓｅａｒｃｈｏｆｉＩＰｒｏｂｌｅｍａｓｅｄｏｎ、Ａｌｇ肿ｔｈ抑Ｓ化＃ＳＡＴ及站心、：ｒ．ＶＩ已一＇－、、、．＇．；节片ｉｎｃ班做ｅｎｔａｌｓｏｌｖｉｎｇ＊＇＇？．＊－

2、．ｊ．．？．＇—，，：＊＊ｒ■■，．．Ｔ＊■＿‘冉护转：．門请：．作者王ｇ巧．．．－、．，？．：：；’指导教师－；段明巧教巧，；；苦＾某＾一级学科：巧？机巧学与巧术．＼二级学科：竹》轨应巧技术？研究方向；智化规谢与規划识别．Ｉ…一．．学位类型．；学术硕±：片三子户Ｖ护＇’．＾若今－Ｉ－．？，？＊；、■＇．巧．ａ诗东北师范大学学位评定委员会＾？‘■ｖｖ＞＾ｔ芳２古＇、可０１６年６月、Ｗ巧在

3、妹：诘和装．．一．這巧．专，怎＊？－＞’？－：．Ｖ．Ｖ１Ｉ—＇＇．－＇．托二．驻．．批？Ｉ－，＇－、．一－可告苦坤１．’．一．■’－．可片．？＇＇＇ｔ—＇＇＇．－本Ｖ又’沪’＇、．＇：；：．．、＇－．；六短＇帘心谭瑪－？、一一一＾，Ａ一．．．－，Ｉ、Ｖ＇Ｖｒ次山祭银其．，、？．．－、Ｉ．■‘学校代码：10200研究生学号：2013102485分类号：TP39密级：无硕士学位论文基于增量式的#SAT

4、求解算法研究ResearchofAlgorithmsfor#SATProblemBasedonincrementalsolving作者：王惠贤指导教师：殷明浩教授一级学科：计算机科学与技术二级学科：计算机应用技术研究方向：智能规划与规划识别学位类型：学术硕士东北师范大学学位评定委员会2016年6月摘要可满足（SAT）问题是判定一个合取范式真假的决策性问题，计算复杂度为NP完全。人工智能领域的许多问题如约束模型检测、电路延迟故障测试等都可以转化为SAT问题进行求解，其中不乏相似的问题。早期的SAT求解器不能利用实例间的

5、相似性，每个问题都要从头开始求解。近年来，随着增量式SAT算法的出现和广泛应用，求解这一系列实例的效率有了非常明显的改善。作为SAT问题的扩展，模型计数（#SAT）问题需要计算合取范式所有可满足赋值的个数，计算复杂度为#P完全。该问题在一致性规划、概率推理等领域有着广泛的应用，其中也包含很多相似问题。由于该问题求解较为困难，因此在#SAT求解器中实现信息的重用显得尤为重要。为了更有效的将求解实际生活中相似的#SAT问题，本文在精确的cachet算法基础上加以改进，提出了增量式模型计数算法。首先对多个实例相互比较，找出

6、需要更新的子句，并按照规定的格式放入输入文件中。然后对初始公式进行求解，并在求解过程中对可重用信息及时加以缓存。紧接着，再次读取输入文件，并根据缓存信息对更新子句的可满足性进行相应的分析和处理。如此循环读取并求解，直至整个输入文件处理完毕。此外，本文还用类似的方法对加权#SAT算法进行了增量式的改进，为处理多个相似的加权#SAT问题提供了新思路。为了测试本文算法的求解效率，我们首先选用随机和图着色领域的实例将本文算法与cachet算法进行对比实验，随后又选用求解困难的概率推理领域的实例，将本文增量式权重#SAT算法与

7、普通权重算法进行比较。实验结果证实了本文算法在上述领域的有效性。关键词：增量式；#SAT；更新子句；加权算法IAbstractThesatisfiabilityproblem(SAT)isadecisionproblemofjudgingwhetherornotaconjunctivenormalformistrue,itscomputationalcomplexityisNP-complete.Manyproblemsinthefieldofartificialintelligencesuchasconstrain

8、tmodelchecking,circuitdelayfaulttestingandsoon,canbeconvertedintoSATproblemtosolve,andthereisnolackofaseriesofsimilarproblemsamongthem.EarlySATsolvercan’tuseinstancesimilari