非布尔可满足性问题求解算法的研究.pdf

上海交通大学硕士学位论文非布尔可满足性问题求解算法的研究姓名：邱敏申请学位级别：硕士专业：计算机软件与理论指导教师：徐良贤20040101非布尔可满足性问题求解算法的研究 1非布尔可满足性问题求解算法的研究 摘 要 可满足性问题(satisfiability problems)是组合数学中的一类比较热门的话题 它对很多工程领域中的研究起着工具性的作用 在工程实践中它与计算机科学 电子科学以及规划学中许多具体问题密切相关 特别是在人工智能领域中 搜索问题和计划问题更是以其作为理论基础 由于可满足性问题的工具性作用科研人员投入了大量的热情和精力对其进行研究 在很短的时间内可满足性问题得到了巨大的发展 在可满足性问题中人们遇到较多的是非布尔类型的问题 围绕着求解非布尔可满足性问题 人们提出了两种不同的求解思路系统求解思路和随机搜索思路作为完备性算法 系统求解思路对于需要确切解的情况有一定优势 但是高确切性带来的负作用是较长的求解时间 目前已经有许多优秀的算法被广为接受它们大都采用了一定的启发策略 对搜索过程也进行了优化但是对于求解公式规模较大的情况 系统算法已不能满足响应时间短的要求 于是人们提出了随机局部搜索算法局部算法是一种不完备算法它也基于一定的启发策略但由于随机性它不能保证一定找到问题的解在本文中作者在对已有两种算法进行研究和分析的基础上 提出了一些新的建议本文的工作大致可以归纳如下 在系统算法中给出一种新的启发策略并实现了修改后的算法同时用部分实例进行了仿真并将仿真结果与其它算法进行比较根据比较结果分析并总结出了新算法的优势和不足 非布尔可满足性问题求解算法的研究 2研究了随机搜索思路分析了系统算法中的噪声水平参数的特性以及它对算法性能的影响本文提出了动态变化的噪声参数这一思想并将该思路用于最新的非布尔随机搜索算法中同样通过几个测例比较了修改后的算法与多种不同算法的性能并对仿真结果进行了分析 作为对算法的补充本文还提出了一种优化策略其目的是对待求解的合取范式公式进行预处理删去冗余变量压缩冗余的变量取值集合使得公式得到简化在本文中作者先给出了理论分析对可能执行的简化过程做了可行性分析然后给出相应的处理流程并以一个实例演示了简化的整个过程最后测试了不用简化过程与使用简化过程在求解同类问题时所花费的时间依此证实了简化过程在绝大多数情况下具有优越性能 最后本文对所做的工作做了总结 同时展望了在该领域中未来可能继续的工作 关键词 可满足性问题非布尔问题系统求解随机搜索启发策略噪声参数简化过程 非布尔可满足性问题求解算法的研究 3THE RESEARCH ON SOLVER ALGORITHMS FOR NON-BOOLEAN SATISFIABILITY PROBLEMS ABSTRACT Satisfiability Problems (SAT) are one kind of the hottest topics in propositional logic. In the practical fields, it is relevant to some issues involving such areas as computer science and electrical science. It even acts as the basis for both the planning and searching in the area of artificial intelligence. For its important role, researchers paid a great deal of energy for the researches on it so that the SAT has had a rapid growth in a short time. Researches put more emphases on Non-Boolean problems just because of its more popularity in the SAT. There are two different solver for Non-Boolean SAT-Systematic algorithm and stochastic local search (SLS). While systematic algorithm, a complete one, is superior when the exact results of SAT are required, it has to cost more time than others in finding results. By now there have been a lot of well known excellent systematic algorithms which are based on some heuristics used to optimize the process of search. For the problems with large size, systematic algorithms can not fit for the requirement of short responding time, so people then brought out SLS. SLS algorithms are also based on heuristics but incomplete, in some case they can not find the final results of certain problems even if they actually are resolvable. In this thesis, the author provides some suggestions on the two 非布尔可满足性问题求解算法的研究 4solvers according to research and analysis on them. The main contributes given by the thesis are as follow: A new heuristic strategy to systematic algorithm is given and a new version of algorithm is realized. According to simulations on several examples, the comparison between new algorithm and old ones is provided. At last, a summary about the advantages and disadvantages about new algorithm is made. Researches on SLS and analysis on a parameter of noise level, a key factor in SLS, are given. A new strategy of dynamic noise is issued depending on the quality of noise and its effect on SLS when changed. Also, a simulation experiment and analysis on the quality of new algorithm are made. As a supplement, an optimization strategy is provided whose aim is to pre-treat the CNF by means of purging redundant variables and value sets. Author first gives theoretical demonstration, and then analyzes the feasibility of this strategy and illustrates the simplification process by an example. Finally present the flow graph of simplifier. Some tests are made and used to compare the resolving performance using simplifier with those without using simplifier. In the last charter, the author makes a summary for the whole thesis and at the same time provides some prospective topics that are worthy in researching in the future. KEY WORDS satisfiability problems, Non-Boolean problems, systematic algorithm, stochastic local search, heuristic strategy, noise parameter, simplifier 上海交通大学 学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果。

除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的作品成果 对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明本人完全意识到本声明的法律结果由本人承担 学位论文作者签名：邱敏 日期： 2004 年 3 月 8 日 上海交通大学 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅 本人授权上海交通大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文 保密□，在 年解密后适用本授权书 本学位论文属于 不保密□ （请在以上方框内打“√” ） 学位论文作者签名：邱敏 指导教师签名：徐良贤 日期： 2 0 0 4 年 3 月 8 日 日期： 2 0 0 4 年 3 月 8 日 非布尔可满足性问题求解算法的研究 1符 号 说 明 {a, b, c} 集合符号 ST 集合变量 |S| 集合中元素的个数 S∪T 集合 S和 T 的并集 S∩T 集合 S和 T 的交集 ST 集合 S和 T 的差 a∈S a 是集合 S中的一个元素 a∉S a 不是集合 S中的一个元素 TRUE FALSE 布尔值 ¬ 取非 ∨ 析取∧ 。