一个极小不可满足公式子类改名的复杂性研究

摘要

改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用，对于一些具有对称结构的难例公式，可以通过改名来降低其证明的复杂性．研究了一个极小不可满足公式子类，给出了该子类的改名算法，并证明了对该子类中改名问题可以在多项式时间内判定．%The rule ability algorithms and formulas is reduced by formulas in a subclass plexity of renaming of of renamings has played a significant role in the construction of efficient satisfi- simplifying resolution proofs of some hard formulas. The complexity proving hard renaming for some hard formulas with symmetrical structure. By investigating the of minimal unsatisfiable formulas we give an algorithm and prove that the com- formulas in the subclass is polynomial time.