MAX(1)和MARG(1)中公式改名的复杂性
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

Supported by the National Natural Science Foundation of China under Grant Nos.60463001, 10410638 (国家自然科学基金); the Special Foundation for Improving Scientific Research Condition of Guizhou Province of China (贵州省高层次人才科研条件特助经费);the Government Foundation of Gu


Complexities of Renaming for Formulas in MAX(1) and MARG(1)
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    A renaming is a function mapping propositional variable to itself or its complement, a variable renaming is a permutation over the set of propositional variables of a formula, and a literal renaming is a combination of a renaming and a variable renaming. Renaming for CNF formulas may help to improve DPLL algorithm. This paper investigates the complexity of decision problem: for propositional CNF formulas H and F,does there exist a variable (or literal) renaming ψ such that ψ(H)=F? Both MAX(1) and MARG(1) are subclasses of the minimal unsatisfiable formulas, and formulas in these subclasses can be represented by trees. The decision problem of isomorphism for trees is solvable in linear time. Formulas in the MAX(1) and MARG(1), it is shown that the literal renaming problems are solvable in linear time, and the variable renaming problems are solvable in quadratic time.

    参考文献
    相似文献
    引证文献
引用本文

许道云,董改芳,王健.MAX(1)和MARG(1)中公式改名的复杂性.软件学报,2006,17(7):1517-1526

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2004-02-12
  • 最后修改日期:2005-07-08
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号