Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

CADE

2002

Springer

2002

Springer

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.

Added |
03 Dec 2009 |

Updated |
03 Dec 2009 |

Type |
Conference |

Year |
2002 |

Where |
CADE |

Authors |
Eugene Goldberg |

Comments (0)