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

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 a simple algorithm for constructing a set of points that is stable with respect to a given set of clauses. Constructing 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 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 linear size set of points that can be constructed in quadratic time.

• Type: Conference
• Year: 2002
• Where: CADE
• Authors: Eugene Goldberg
• Keywords: Automated Reasoning, CADE 2002, Linear Size Set, Search Space Traversal, Stable Set