基于cdcl的sat问题求解算法研究

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

1、ｆ駐ｔＥ輪１議議目，Ｓ牛团馳Ｔ耐旧■脯＾键．１密级国内图书分类号：０１４１：公开１国际图书分类号：５０．６西南交通大学研究生学位论文基于ＣＤ化的ＳＡＴ问题求解算法研究年级二零一兰级姓名易念申请学位级别理学硕±专业应用数学指导老师徐扬教授二零一六年五月ＣｌａｓｓｉｆｉｅｄＩｎｄｅｘ：０１４１．１Ｕ．６．Ｄ．Ｃ：５１０ＳｏｕｔｈｗｅｓｔＪｉａｏｉｘｍｇＵｎｉｖｅｒｓｉｔｙＭａｓｔｅｒＤｅｇｒｅｅＴｈｅｓｉｓＳＴＵＤＹＯＮＳＡ

2、ＴＳＬＯＶＩＮＧＡＬＧＯＲＩＴＨＭＢＡＳＥＤＯＮＣＤＣＬＧｒａｄｅ：２０１３Ｃａｎｄｉｄａｔｅ：ＮｉａｎＹｉＡｃａｄｅｍｉｃＤｅｒｅｅＡｌｉｅｄｆｏｒ；ＭａｓｔｅｒｇｐｐＳｅｃｉａｌｉｔ：ＡｌｉｅｄＭａｔｈｅｍａｔｉｃｓｐｙｐｐＳｕｅｒｖｉｓｏｒ：Ｐｒｏｆ．ＹａｎＸｕｐｇＭａｙ，２０１６西南交通大学学位论文版权使用授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家有关部口或机构送交论文的复印件和电子版，允许论文被查阅和

3、借阅。本人授权西南交通大学可Ｗ将本论文的全部或部分内容编入有关数据库进行检索，可ｙ？采用影印、缩印或扫描等复印手段保存和汇编本学位论文。本学位论文属于１□．保密，在年解密后适用本授权书；２．不保密？吏用本授权书。＂＂请在上方框内打Ｖ（）学位论文作者签名：指导老师签名：＾．曰期曰期：ｙ／／／：ｆ：／厂。／西南交通大学硕±学位论文主要工作（贡献）声明本文针对求解ＳＡＴ问题所做的主要工作和贡献如下；一１、本文提出种启发式策略，根据所给子句、文字数量和出现次数，定义文字相关系数，

4、进而对初始变量决策过程提供依据、子句相关系数；２，、基于定义的相关系数给定冲突状态定义，根据冲突状态下的总的冲突数不断减少的原则，，根据冲突稳定状态制定回溯回退机制策略进而定义冲突稳定状态；［ＷＤＣＬ－３、基于上两种策略，结合Ｃ求解器形成求解ＳＡＴ问题新算法Ｃｏｎｆｌｉｃｔ（ＳＡＴ），并采用ＳＡＴ竞赛中的问题及ＴＰＴＰ问题库中旅行商问题进巧实例测试，发现Ｃｏｎｆｌｔ－ｉｃＳＡＴ算法具有较高的求解效率，对于成功求解的ＳＡＴ问题使用的平均时间较短。本人郑重声明，：所呈交的学位论文是在导师指导下独立进行研

5、究工作所得的成果。除文中己经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的研究成果。对本文的研究做出贡献的个人和集体，均己在文中作了明确说明。本人完全了解违反上述声明所引起的一切法律责任将由本人承担。学位论文作者签名：．Ｌ瓜曰期：西南交通大学硕±研究生学位论文第Ｉ页摘要人工智能领域中，研究命题逻辑公式的可满足性巧ＡＴ问题具有十分重耍的作用。）随着科学、技术、社会等领域的发展，需要解决的ＳＡＴ问题的规模变得越来越大，而传统单一的算法无法适应这些大规模的一些针对大规

6、模的ＳＡＴ问题的ＳＡＴ问题。因此求解器应运而生，如Ｃｈａｆ、ｚＣｈａｆ、Ｍｉｎｉｓａｔ、Ｌｉｎｇｅｌｉｎｇ等诸多著名求解器。这些求解一器都并非由单的算法构建一，而是在传统的ＤＰＬＬ等算法的基础上构建的套系统，如ＣＤＣＬ求解器，其包含多个决策过程，在算法过程中不断的改进学习和调整，Ｗ更为高效的解大规模的ＳＡＴ问题。送些求解器主要分为如下几个部分，分别是变量决策、冲突分析、子句学习和回溯机制。而其中的变量决策过程在整个算法构架中占有十分一重要的地位，个好的变量决策策略可Ｗ减少冲突的产生，大量节省求解时间，因

7、此研究变量决策过程的策略具有较为重耍的意文。本文主要结合ＣＤＣＬ求解器构架，做了如下几个方面的研究工作：一１、本文提出种启发式策略，根据所给子句、文字数量和出现次数，定义文字相关系数，、子句相关系数进而对初始变量决策过程提供依据；２、基于定义的相关系数，给定冲突状态定义，根据冲突状态下的总的冲突数不断，减少的原则，进而定义冲突稳定状态根据冲突稳定状态制定回溯回退机制策略；３Ｌ－、基于Ｗ上两种策略，结合ＣＤＣ求解器形成求解ＳＡＴ问题新算法ＣｏｎｆｌｉｃｔＳＡＴ，（）并采用ＳＡＴ竞赛中的问题Ｗ及ＴＰ

8、ＴＰ问题库中旅行商问题进行实例测试，并对测试结果进行分析比较。：－命题逻辑，可满足性问题，，ｔ关键字，ＤＰＩＸ算法ＣＤＣＬＣｏｎｆｌｉｃＳＡＴ西南交通大学硕±硏究生学位论文第ＩＩ页ＡｂｓｔｒａｃｔＴｈｅｓａｔｉｓｆｉａｂｉｌｉｔｙＳＡＴｐｒｏｂｌｅｍ