Some Properties of Pigeon-Hole Formulas
Author:
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [16]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    The pigeon-hole formula PHnn+1, defined from the pigeon hole principles, is one of the hardest examples on resolution. The research of the formula’s constructions and properties is helpful for constructing other hard examples. It is shown that PHnn+1 is a minimal unsatisfiable formula. The two normal forms of maximal satisfiable truth assignments for PHnn+1 are presented by the minimal unsatisfiability of PHnn+1, which one of normal forms is used in Haken’s proof of hardness for PHnn+1. The formula PHnn+1 has well isomorphics properties on substructures. For the modified DPLL algorithm introduced by the isomorphism rule, the complexity of refutation proof of PHnn+1 can be reduced to O(n3).

    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:177-193. [doi: 10.1016/S0166-218X(99)00039-6]
    [3] Chvátal V, Szemerédi T. Many hard examples for resolution. Journal of the Association for Computing Machinery, 1988,35(4): 759-768. [doi: 10.1145/48014.48016]
    [4] Haken A. The intractability of resolution. Theoretical Computer Science, 1985,39:297-308. [doi: 10.1016/0304-3975(85)90144-6]
    [5] Urquhart A. Hard examples for resolution. Journal of the ACM, 1987,34(1):209-219. [doi: 10.1145/7531.8928]
    [6] Roberts FS, Tesman B, Wrote; Feng S, Trans. Applied combinatorics (2nd ed.). Beijing: China Machine Press, 2005 (in Chinese).
    [7] Atserias A, Galesi N, GavaldàR. Monotone proofs of the pigeon hole principle. In: Montanari U, Rolin J, Welzl E, eds. Proc. of the ICALP 2000. LNCS 1853, Berlin, Heideberg: Springer-Verlag, 2000. 151-162.
    [8] Xu DY, Liu CY. DPLL algorithm with literal renaming strategy. Journal of Frontiers of Computer Science and Technology, 2007, 1(1):116-125 (in Chinese with English abstract).
    [9] Büning HK, Lettman T. Propositional Logic: Deduction and Algorithms. Cambridge: Cambridge University Press, 1999.
    [10] Büning HK, Xu DY. The complexity of homomorphisms and renamings for minimal unsatisfiable formulas. Annals of Mathematics and Artificial Intelligence, 2005,43(1-4):113-127. [doi: 10.1007/s10472-005-0422-8]
    [11] Büning HK, Zhao XS. Minimal unsatisfiability: Results and open questions. In: Proc. of the Conf. on SAT 2002. Cincinati, 2002. 1-66.
    [12] Xu DY. Applications of minimal unsatisfiable formulas to polynomially reduction for formulas. Journal of Software, 2006,17(5): 1204-1212 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/1204.htm [doi: 10.1360/jos171204]
    [13] Xu DY, Deng TY, Zhang QS. k-LSAT(k≥3) is NP-complete. Journal of Software, 2008,19(3):511-521 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/19/511.htm [doi: 10.3724/SP.J.1001.2008.00511]
    [14] Davis M, Logemann G, Loveland D. A machine program for theorem proving. Communications of the ACM, 1962,5(7):394-397. [doi: 10.1145/368273.368557]
    [15] Davis M, Putnam H. A computing procedure for quantification theory. Journal of the ACM, 1960,7(3):201-215. [doi: 10.1145/321033.321034]
    [16] Nerode A, Shore RA. Logic for Applications. 2nd ed., New York: Springer-Verlag, 1993.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

许道云,韦立,王晓峰.鸽巢公式的一些性质.软件学报,2011,22(11):2553-2563

Copy
Share
Article Metrics
  • Abstract:5326
  • PDF: 6390
  • HTML: 0
  • Cited by: 0
History
  • Received:July 07,2010
  • Revised:November 03,2010
You are the first2044654Visitors
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