对于极小不可满足公式和它的子类的研究是近年来兴起的一个热门方向。我们对极小不可满足公式集感兴趣主要基于两方面的原因：一是大多数的消解难例公式都是极小不可满足的；二是对于极小不可满足公式的深入理解，有助于我们构造新的难例公式以及新的满足性算法。 一个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+={F∈MAX|(E)x∈var(F)(A)splittings(Fx，F(_)x)：Fx，F(_)x∈MAX+∪{(□)}}，其中□代表空子句。MAX+(k)=MAX+∩MAX(k)。显然，MAX+是MAX中分裂公式的闭包，即公式的分裂在MAX+中是封闭的。而且证明了这种递归构造方法具有可靠性和完备性。 另一方面，我们将研究关于MAX+(k)中公式改名的判定问题的复杂性。基于分裂技术并通过证明MAX(1)中公式改名问题在多项式时间内可以判定。我们证明了：MAX+(k)中公式的改名问题在多项式时间内可以判定，并给出相应的算法。最后，我们给出了一个文字改名的应用，以此来说明改名问题在证明系统中起到的重要作用。