• Article
  • | |
  • Metrics
  • |
  • Reference [13]
  • |
  • Related [20]
  • | | |
  • 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
    [1]Krishnamurthy B.Short proofs for tricky formulas.Acta Informatica,1985,22(3):253-275.
    [2]Urquhart A.The symmetry rule in propositional logic.Discrete Applied Mathematics,1999,96-97(1):177-193.
    [3]Xu DY.On the complexity of renamings and homomorphisms for minimal unsatisfiable formulas[Ph.D.Thesis].Nanjing:Nanjing University,2002.
    [4]Papadimitriou CH,Wolfe D.The complexity of facets resolved.Journal of Computer and System Sciences,1988,37(1):2-13.
    [5]Aharoni R.Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas.Journal of Combinatorial Theory,1996,43(A):196-204.
    [6]Davydov G,Davydova I,Kleine Büning H.An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF.Annals of Mathematics and Artificial Intelligence,1998,23(3-4):229-245.
    [7]Fleischner H,Kullmann O,Szeider S.Polynomial-Time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.Theoretical Computer Science,2002,289(1):503-516.
    [8]Kleine Büning H,Zhao XS.Polynomial time algorithms for computing a represent(a)tion for minimal unsatisfiable formulas with fixed deficiency.Information Processing Letters,2002,84(3):147-151.
    [9]K(o)bler J,Sch(o)ning U,Toran J.The Graph Isomorphism Problem:Its Structural Complexity.Birkh(a)user Verlag,1993.
    [10]Kleine Büning N,Xu DY.The complexity of homomorphisms and renamings for minimal unsatisfiable formulas.Annals of Mathematics and Artificial Intelligence,2005,43(1-4):113-127.
    [11]Kleine Büning H,Zhao XS.The complexity of some subclasses of minimal unsatisfiable formulas.Discrete Applied Mathematics,2005,130(2):185 -207.
    [12]Kleine Büning H.On subclasses of minimal unsatisfiable formulas.Discrete Applied Mathematics,2000,107(1-3):83-98.
    [13]Aho AV,Hopcropt JE,Ullman JD.The Design and Analysis of Computer Algorithms.Addison-Wesley Publishing Company,1976.84-86.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:4112
  • PDF: 5053
  • HTML: 0
  • Cited by: 0
History
  • Received:February 12,2004
  • Revised:July 08,2005
You are the first2034815Visitors
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