Complexity Of Renamings For MAX～+(k)

Research on minimal unsatisfiable formula and its subclasses is an active topic that begins to surface in recent years. We are interested in subclasses of MU mainly for two reasons. one is that almost all hard formulas for resolution are minimal unsatisfiable formulas, the other is that a deeper understanding of MU-formulas may help to develop new hard formulas and new satisfiability algorithms.A CNF formula F is minimal unsatisfiable (MU) if 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 and 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 variable x. 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. The variable and literal renaming problems of formulas in MU(k) is equivalent to the graph isomorphism problem. As we known, the graph isomorphism problem is still in NP. So computer scientists are trying to seek some polynomially solvable subclasses of minimal unsatisfiable formulas all the while.In this thesis, We seek a subclass MAX⁺ of maximal minimal unsatisfiable formulas and the formulas in it can be constructed recursively. MAX⁺ = {F∈ MAX| (?)x ∈ var(F)(?)splittings(F_x, F_(?)x) : F_X,F_(?)x ∈ MAX⁺ U{?}} , where (?) is empty clause. Denote MAX⁺(k) = MAX⁺ ∩MAX(k). Obviously, the subclass MAX⁺ is closure on the splitting of formulas in MAX. Moreover, we show that the method constructing recursively the formulas in MAX⁺ is provided with completeness and soundness.On the other hand, we will investigate the complexity of decision problems for renaming problems (literal renaming; variable renaming) of the formulas in MAX⁺(k). We will present algorithms solving the above mentioned problems in polynomial time for fixed k. The proof is based on the splitting technology and the fact that the complexities of renamings of formulas in MAX(1) are polynomial time. Finally, we quote application of the literal renaming to illuminate the power of the renamings for prepositional proof systems .