Research on the Renaming of a Subclass of Minimal Unsatisfiable Formulas
Qingyan Chen · Journal of Binzhou University · 2011
The rule of renamings has played a significant role in the construction of efficient satisfiability algorithms and simplifying resolution proofs of some hard formulas.The complexity proving hard formulas is reduced by renaming for some hard formulas with symmetrical structure.By investigating the formulas in a subclass of minimal unsatisfiable formulas we give an algorithm and prove that the complexity of renaming of formulas in the subclass is polynomial time.