MAX(1)和MARG(1)中公式改名的复杂性(英文)

作者：许道云; 董改芳; 王健

来源：软件学报, 2006, (07): 1517-1526.

• 计算复杂性
• 改名
• 极小不可满足公式 complexity
• renaming
• minimal unsatisfiable formula

改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合.研究CNF公式的改名有助于改进DPLL算法.考虑判定问题“对于给定的CNF公式H和F是否存在一个变元(或文字)改名,使得(H)=F?”的计算复杂性.MAX(1)和MARG(1)是极小不可满足公式的两个子类,这两个子类中的公式可以用树表示.树同构的判定问题在线性时间内是可解的.证明了对于MAX(1)和MARG(1)中的公式,文字改名问题在线性时间内可解,变元改名问题在平方次时间内可解.

• 单位
  软件工程国家重点实验室; 武汉大学; 贵州大学; 内蒙古农业大学