SYMPOSIUM MINISYMPOSIA

ABSTRACT

A 3-CNF expression is a Boolean expression in conjunctive normal form with 3 literals per clause. Satisfiability is the problem of determining whether a Boolean expression has an assignment to its variables that will make the value of the expression true. Satisfiability is a well-known NP-complete problem [1]. All known deterministic algorithms for solving problems in this class require exponential time in the worst-case, and it remains unknown whether polynomial-time algorithms exist. The class is important because many of the problems occur in practical computing. When confronted with NP-complete problems, it is common for practitioners to apply polynomial-time approximation algorithms instead of seeking exact solutions. Research on better algorithms continues, with goals both of speeding up practical applications and of improving our understanding of the combinatorial nature of the problems. Efforts to reduce upper bounds on the complexity of deterministic algorithms for various NP-complete problems will eventually lead to the discovery of a lower bound for all problems in the class.

CCG is a recently defined algorithm for determining the satisfiability of 3-CNF expressions [3]. It can easily be generalized from 3CNF to k-CNF expressions [4] and shown to have a worst-case time complexity equal to that of the branching algorithm of Monien and Speckenmeyer [2], which remains a standard among deterministic satisfiability algorithms. CCG determines satisfiability by searching for a clique in a graph made from an expression~Rs complement. The clauses in the expression become nodes in the graph, where two nodes are adjacent if the clauses they represent are consistent, i.e., no literal in one clause is the negation of a literal in the other. The original expression is satisfiable if and only if the graph has a clique of (n choose 3) nodes, where n is the number of variables in the expression. The search for a clique is simplified by reduction and pruning operations. Reduction removes from consideration nodes that can surely be used to extend a partially discovered clique, and pruning removes nodes that cannot be a part of a partially discovered clique. The reduction operation figures prominently in establishing the worst-case complexity of the algorithm. The effects of pruning have not yet been analyzed mathematically, but an empirical study shows that it can dramatically reduce the number of steps in a potentially exponential search. This paper summarizes the previous results and presents the results of a new empirical study that contrasts the algorithm's performance on satisfiable expressions with its performance on unsatisfiable expressions. In general, the number of pruning steps required to identify an unsatisfiable expression is much smaller than the number of steps needed to identify a satisfiable expression. This provides a rationale for using the CCG method in a polynomial-time approximation algorithm that predicts the satisfiability of an expression after a small, fixed number of steps.

References

1. Cook, S. 1971. The Complexity of Theorem-Proving Procedures. Proceedings of the Third ACM Symposium on Theory of Computing, 151-158. ACM, New York.

2. Monien, B., and E. Speckenmeyer. 1985. Solving Satisfiability in Less Than 2^n Steps. Discrete Applied Mathematics 10:287-295.

3. O~RNeil, T. E. 1996. A Complement-Based Algorithm for 3CNF Satisfiability. Journal of Computing and Information 2(1):170-184.

4. O~RNeil, T. E. 1998. The Generalized CCG Algorithm for K-CNF Satisfiability. In preparation.

Getting More Information

To obtain more information about the meeting send e-mail to: fscc98@pax.st.usm.edu.

Return to PAX
Return to USM

USM
inquire@delphi.st.usm.edu
Updated
http://pax.st.usm.edu