Advertisement

Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points

  • Eugene Goldberg
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

We show that a conjunctive normal form (CNF) formula F is unsatisfiable iff there is a set of points of the Boolean space that is stable with respect to F. So testing the satisfiability of a CNF formula reduces to looking for a stable set of points (SSP). We give some properties of SSPs and describe a simple algorithm for constructing an SSP for a CNF formula. Building an SSP can be viewed as a “natural” way of search space traversal. This naturalness of search space examination allows one to make use of the regularity of CNF formulas to be checked for satisfiability. We illustrate this point by showing that if a CNF F formula is symmetric with respect to a group of permutations, it is very easy to make use of this symmetry when constructing an SSP. As an example, we show that the unsatisfiability of pigeon-hole CNF formulas can be proven by examining only a set of points whose size is quadratic in the number of holes.

Keywords

Equivalence Class Transport Function Proof System Conjunctive Normal Form Satisfying Assignment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    C.A. Brown, L. Finkelstein, P.W. Purdom. Backtrack searching in the presence of symmetry. In “Applied algebra, algebraic algorithms and error correcting codes”. Sixth international conference, P. 99–110. Springer-Verlag, 1988.Google Scholar
  2. 2.
    V. Chvatal, E. Szmeredi. Many hard examples for resolution. J. of the ACM,vol. 35, No 4, pp. 759–568.Google Scholar
  3. 3.
    W. Cook, C.R. Coullard, G. Turan. On the complexity of cutting planes proofs. Discrete Applied Mathematics, 18, 1987, 25–38.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    J. Crawford, M. Ginsberg, E. Luks, A. Roy. Symmetry breaking predicates for search problems. Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR’96).Google Scholar
  5. 5.
    M. Davis, G. Logemann, D. Loveland. A Machine program for theorem proving. Communications of the ACM.-1962.-V. 5.-P. 394–397.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    E. Goldberg. Proving unsatisfiability of CNFs locally. Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability Testing.Google Scholar
  7. 7.
    A. Haken. The intractability of resolution. Theor. Comput. Sci. 39 (1985), 297–308.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    B. Krishnamurthy. Short proofs for tricky formulas. Acta Informatica 22 (1985) 253–275.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    D. Mitchell, B. Selman, and H.J. Levesque. Hard and easy distributions of SAT problems. Proceedings AAAI-92, San Jose,CA, 459–465.Google Scholar
  10. 10.
    M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver. Proceedings of DAC-2001.Google Scholar
  11. 11.
    C. Papadimitriou. On selecting a satisfying truth assignment. Proceedings of FOC-91.Google Scholar
  12. 12.
    A. Roy. Symmetry breaking and fault tolerance in Boolean satisfiability. PhD thesis. Downloadable from http://www.cs.uoregon.edu/~aroy/
  13. 13.
    B. Selman, H. Kautz, B. Cohen. Noise strategies for improving local search. Proceedings of AAAI-94.Google Scholar
  14. 14.
    I. Shlyakhter. Generating effective symmetry breaking predicates for search problems. Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability TestingGoogle Scholar
  15. 15.
    A. Urquhart. The symmetry rule in propositional logic. Discrete Applied Mathematics 96–97(1999):177–193,1999.CrossRefMathSciNetGoogle Scholar
  16. 16.
    H. Wong-Toi. Private communication.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Eugene Goldberg
    • 1
  1. 1.Cadence Berkeley LabsBerkeley

Personalised recommendations