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

Research on the Renaming of a Subclass of Minimal Unsatisfiable Formulas

作　　者：陈庆燕[1] 

机构地区：[1]滨州学院计算机科学技术系,山东滨州256603

出　　处：《滨州学院学报》2011年第6期82-85,共4页Journal of Binzhou University

基　　金：滨州学院青年人才创新工程科研基金项目(BZXYQNLG200611)

摘　　要：改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用,对于一些具有对称结构的难例公式,可以通过改名来降低其证明的复杂性.研究了一个极小不可满足公式子类,给出了该子类的改名算法,并证明了对该子类中改名问题可以在多项式时间内判定.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.

关 键 词：改名 极小不可满足公式 子类 多项式时间 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]