摘要
改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用,对于一些具有对称结构的难例公式,可以通过改名来降低其证明的复杂性.研究了一个极小不可满足公式子类,给出了该子类的改名算法,并证明了对该子类中改名问题可以在多项式时间内判定.
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.
出处
《滨州学院学报》
2011年第6期82-85,共4页
Journal of Binzhou University
基金
滨州学院青年人才创新工程科研基金项目(BZXYQNLG200611)
关键词
改名
极小不可满足公式
子类
多项式时间
renaming
minimal unsatisfiable formulas
subclass
polynomial time
