试论max'+（2）公式改名的复杂性

《试论max'+（2）公式改名的复杂性》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、贵州大学硕士学位论文MAX<'+>（2）公式改名的复杂性姓名：姚雷博申请学位级别：硕士专业：计算机应用技术指导教师：许道云20070501原创·眭声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的科研成果。对本文的研究在做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律责任由本人承担。论文作者签名：型量鱼擅日期．呈QQ盈皇旦关于学位论文使用授权的声明本人完全了解贵州大学有关保留、使用学位论文的规定，同意学校保留或向国家有关部

2、门或机构送交论文的复印件和电子版，允许论文被查阅舜口借阅；本人授权贵州大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，．-j-以采用影印、缩印或其他复制手段保存论文和汇编本学位论文。(保密论文在解密后应遵守此规定)论文作者签名：巡鲎擅导师签名：泌．，q摘要一个CNF公式，称为极小不可满足的(^彤)，如果F是不可满足，并且在，中删去任意一个子句后所得到的公式是可满足的．一个MU中的公式F称为最大的，如果对于任意一个子旬feF且对于任意一个文字L，—正，工仨，，将L添加到子句f中，公式F变为可满足的．最大的极小不可满足公式类记作MAX，MAX(k)=M

3、U(k)c、MaX．公式F的一个改名是一个定义在vat(F)上的函数妒，使得对每个变元x，认x)∈{x’，x}；公式F的一个变元改名是vaKF)上的一个置换；公式，的一个文字改名是一个变元改名和一个改名的组合。以上这三种改名不改变公式的可满足性。改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用。许道云教授已经证明：MU(k)中的变元和文字改名都等价于图同构的判定问题，而图同构的判定问题是NP问题。最近，许道云教授找到了一个极小不可满足公式的子类——MAX+公式，该类公式的变元和文字改名的判定问题可以在多项式时间内完成，并指出MAX+O)公

4、式的改名判定时间是O(n2)．本文基于上述结论，利用Hans．KleineBrining教授提出的分裂技术，先对一些满足特殊条件的MAX+公式的结构进行了分析，发现了一些规律。之后，利用这些规律，再对MAX+(2)公式的结构进行了分析，发现任何一个MAX+(2)公式的结构必然具有如下情况之一：(1)有两个全出现变元，且每个变元在公式F的正负出现次数至少为2：(2)有唯一的全出现变元；(3)没有全出现变元，但有1到3个准全出现变元，且每个变元在公式F的正负出现次数至少为2：(4)没有全出现变元和准全出现变元，但有唯一的一对匹配变元对，并且在这对变元中至少有一个变

5、元在公式F中的正负出现次数至少为2。这些结构特点保证了两个MAX+(2)公式是否有改名函数的问题可以在O(n2)时间内完成。本文给出了相应的算法，并进行了证明。关键词：MAX+(2)公式、改名，复杂性中图分类号：0141．1文献标识码：AAbstractACNFformulaFisminimalunsatisfiable(MV)，iftheformulaFisunsatisfiableanddeletingallarbitraryclauseresultsasatisfiableformula．AformulaFin删iscalledmaximal。iffor

6、anyclausefEF，anyliteral‘and也，上tf，addingLtofyieldsasatisfiableformula．ThesetofmaximalminimalunsatisfiableisdenotedasMAX．ArenamingofformulaFisamapping妒overW们suchthat氟对e“q}foreveryvariablex．Avariablerenamingisapermutationofvariables．Aliteralrenamingisacombinationofavariablerenaminganda

7、renaming．Therenamingsofformulasdon’tchangethesatisfiabilityofformulas．Therenamingshasplayedasignificantroleinsimplifyingresolutionproofsofsomehardformulasandconstructingtheefficientsatisfiabilityalgorithms．ProfessorDanyun．Xuhasprovedthatthevariableandliteralrenamingproblemsoftheform

8、ulasinMU(k)areequiv