论文摘要
一个CNF公式F称为极小不可满足的（MU），如果F是不可满足，并且在F中删去任意一个子句后所得到的公式是可满足的。一个MU中的公式F称为最大的，如果对于任意一个子句f∈F且对于任意一个文字L，-L，L（?）f，将L添加到子句f中，公式F变为可满足的。最大的极小不可满足公式类记作MAX，MAX（k）=MU（k）∩MAX。公式F的一个改名是一个定义在var（F）上的函数φ，使得对每个变元x，φ（x）∈{x，-x}；公式F的一个变元改名是var（F）上的一个置换；公式F的一个文字改名是一个变元改名和一个改名的组合。以上这三种改名不改变公式的可满足性。改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用。许道云教授已经证明：MU（k）中的变元和文字改名都等价于图同构的判定问题，而图同构的判定问题是NP问题。最近，许道云教授找到了一个极小不可满足公式的子类——MAX+公式，该类公式的变元和文字改名的判定问题可以在多项式时间内完成，并指出MAX+（1）公式的改名判定时间是O（n2）。本文基于上述结论，利用Hans.Kleine Büning教授提出的分裂技术，先对一些满足特殊条件的MAX+公式的结构进行了分析，发现了一些规律。之后，利用这些规律，再对MAX+（2）公式的结构进行了分析，发现任何一个MAX+（2）公式的结构必然具有如下情况之一：（1）有两个全出现变元，且每个变元在公式F的正负出现次数至少为2；（2）有唯一的全出现变元；（3）没有全出现变元，但有1到3个准全出现变元，且每个变元在公式F的正负出现次数至少为2；（4）没有全出现变元和准全出现变元，但有唯一的一对匹配变元对，并且在这对变元中至少有一个变元在公式F中的正负出现次数至少为2。这些结构特点保证了两个MAX+（2）公式是否有改名函数的问题可以在O（n2）时间内完成。本文给出了相应的算法，并进行了证明。