The Complexity Of The Max + (2) Formula Renamed

A CNF formula F is minimal unsatisfiable(MU), if the formula F is unsatisfiable and deleting an arbitrary clause results a satisfiable formula. A formula F in MU is called maximal, if for any clause f∈F, any literal L and-L, L(?)f, adding L to f yields a satisfiable formula.The set of maximal minimal unsatisfiable is denoted as MAX. A renaming of formula F is a mappingφover var(F) such thatφ(x)∈{x,-x} for every variablex. A variable renaming is a permutation of variables. A literal renaming is a combination of a variable renaming and a renaming. The renamings of formulas don't change the satisfiability of formulas.The renamings has played a significant role in simplifying resolution proofs of some hard formulas and constructing the efficient satisfiability algorithms. Professor Daoyun. Xu has proved that the variable and literal renaming problems of the formulas in MU(k) are equivalent to the graph isomorphism problem. As we known, the graph isomorphism problem is still in NP. Resently, Professor Daoyun. Xu and his student Qingyan. Chen found a new subclass in MU formulas, which is called MAX~+ formulas, and in which the variable and literal renaming problems of formulas is polynomial. And they point that the renaming problems in MAX~+(1) formulas is square.Based on above conclutions, we show some rules about MAX~+ formulas using the splitting technique brought by Professor H.Kleine Büning. With the help of these rules, we show a property about MAX~+(2). The property tells us that every formula F in MAX~+(2) have one of the following structures:(1)There are two full appearance variables in F, and every variable appears in F at least two times " + " and two times "-";(2)There is only one full appearance variable in F;(3) There are only one to three nearly full appearance variables, and every variable appears in F at least two times " + " and two times "-";(4)There is only a pair of matching variables, and at least one of them appears in F at least two times " + " and two times "-".According to this property, we proved that the variable and literal renaming problems in MAX~+(2) formulas is square too. We show and prove the algorihm about this question in this thesis.