导　　师： 陈建二

授予学位： 硕士

作　　者： ;

机构地区： 广州大学

摘　　要： 可满足性问题(SAT)是计算机科学中最重要的问题之一,此问题在计算机科学上许多的领域有着十分重要的地位,也在工业界有着非常广泛的应用,很多实际问题都可以被转化成为可满足性问题的一个实例来进行求解。可满足性问题是第一个被证明为NP完全的问题。除非=,否则很可能不存在多项式时间的算法可以求得其精确解。在实际应用中,人们考虑寻找一个更简单的NP完全问题,使得人们最终设计完成的算法的时间复杂度更小。本文研究的单文字可满足性问题(XSAT)就是这种问题,XSAT是SAT的一种特殊情况,人们对于XSAT的主要研究集中在关于变量数9)的参数算法之上。在以往的算法中,消解操作后的表达式长度可能会出现增长,这使得在XSAT文章中进行消解存在着一定的风险,不一定可以保证有效率地解决问题。本文的主要内容如下:(1)对于目前XSAT的最佳算法,本文以待定参数的角度进行了详细的分析,重现了加权分治中先设置待定参数,再进行分支分析,最后确定权值的情况。(2)本文证明了在XSAT算法中使用消解的安全性。本文证明了XSAT问题中表达式的长度不会无限增长,这使得人们可以在XSAT问题的分析中无后顾之忧地使用消解。另外,本文对在所有变量出现次数均小于等于2的情况下的XSAT问题给出了多项式时间算法,并给出详细证明。在以前的研究中并没有给出过这种情况的证明。(3)本文对在传统算法的复杂度分析中观察到一些特定的情况可以被有效率地解决。如果同一变量出现在两个长度为三的子句中,又或者两个子句中有超过三个共同变量,那么可以直接对其进行分支来消除它。对于线性单文字可满足性问题,本文证明了如果存在变量在所有子句中出现次数大于等于4,那么可以直接对其进行分支来消除它。

关 键 词： 参数算法 单文字可满足性问题 布尔变量 完全问题

领　　域： [自动化与计算机技术—计算机系统结构] [自动化与计算机技术—计算机科学与技术]