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

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:February 12,2004
  • Revised:July 08,2005
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063