%0 Journal Article
%T max(1)和marg(1)中公式改名的复杂性
%A 许道云？
%A 董改芳？
%A 王健？
%J 软件学报
%P 1517-1526
%D 2006
%X 改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合.研究cnf公式的改名有助于改进dpll算法.考虑判定问题"对于给定的cnf公式h和f是否存在一个变元(或文字)改名ψ使得ψ(h)=f?"的计算复杂性.max(1)和marg(1)是极小不可满足公式的两个子类,这两个子类中的公式可以用树表示.树同构的判定问题在线性时间内是可解的.证明了对于max(1)和marg(1)中的公式,文字改名问题在线性时间内可解,变元改名问题在平方次时间内可解.
%K 计算复杂性
%K 改名
%K 极小不可满足公式
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20060705&flag=1