Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points
- 287 Downloads
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.
KeywordsEquivalence Class Transport Function Proof System Conjunctive Normal Form Satisfying Assignment
Unable to display preview. Download preview PDF.
- 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.V. Chvatal, E. Szmeredi. Many hard examples for resolution. J. of the ACM,vol. 35, No 4, pp. 759–568.Google Scholar
- 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
- 6.E. Goldberg. Proving unsatisfiability of CNFs locally. Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability Testing.Google Scholar
- 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.M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver. Proceedings of DAC-2001.Google Scholar
- 11.C. Papadimitriou. On selecting a satisfying truth assignment. Proceedings of FOC-91.Google Scholar
- 12.A. Roy. Symmetry breaking and fault tolerance in Boolean satisfiability. PhD thesis. Downloadable from http://www.cs.uoregon.edu/~aroy/
- 13.B. Selman, H. Kautz, B. Cohen. Noise strategies for improving local search. Proceedings of AAAI-94.Google Scholar
- 14.I. Shlyakhter. Generating effective symmetry breaking predicates for search problems. Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability TestingGoogle Scholar
- 16.H. Wong-Toi. Private communication.Google Scholar