滨州学院学报
濱州學院學報
빈주학원학보
JOURNAL OF BINZHOU UNIVERSITY
2011年
6期
82-85
,共4页
改名%极小不可满足公式%子类%多项式时间
改名%極小不可滿足公式%子類%多項式時間
개명%겁소불가만족공식%자류%다항식시간
renaming%minimal unsatisfiable formulas%subclass%polynomial time
改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用，对于一些具有对称结构的难例公式，可以通过改名来降低其证明的复杂性．研究了一个极小不可满足公式子类，给出了该子类的改名算法，并证明了对该子类中改名问题可以在多项式时间内判定．
改名規則在創建有效的滿足性算法和簡化某些消解難例的證明中起到瞭重要作用，對于一些具有對稱結構的難例公式，可以通過改名來降低其證明的複雜性．研究瞭一箇極小不可滿足公式子類，給齣瞭該子類的改名算法，併證明瞭對該子類中改名問題可以在多項式時間內判定．
개명규칙재창건유효적만족성산법화간화모사소해난례적증명중기도료중요작용，대우일사구유대칭결구적난례공식，가이통과개명래강저기증명적복잡성．연구료일개겁소불가만족공식자류，급출료해자류적개명산법，병증명료대해자류중개명문제가이재다항식시간내판정．
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.
