Deterministic Propositional Satisfiability


The SAT problem is an NP-Complete problem. An efficient algorithm for the solution of SAT would provide efficient algorithms for every problem in the complexity class. An efficient algorithm for the solution of any NP-Complete problem would have many important consequences. No algorithm is currently known for the efficient solution of any NP-Complete problem.

Many very bright people have spent a number of years trying to show that $P \ne NP$, without success. Many other very bright people have spent as many years trying to find an efficient algorithm for SAT.  Most of those efforts have been expended in trying to improve model-elimination theorem provers, to search the Herbrand universe more efficiently

This dissertation is based on a preliminary hypotheses that and efficient, or less inefficient, algorithm for SAT exists. However, the approach to the problem will be  different from previous approaches.  The key idea is to construct a logic that admits short proofs/refutations, or at least that is not known to require exponentially long proofs/refutations.  Then, using this logic, to investigate a variety of deduction algorithms that may be useful.

A construction giving a complete and efficient (polynomially bounded) algorithm for SAT would provide  proof that P=NP.  Progress toward a solution may yeild a complete algorithm with more efficient average-case behavior, or an efficient algorithm for a larger subset of the cases, than was previously known.

The Satisfiability Problem

The statement of the $SAT$ problem is hideously simple: Given a propositional term in conjunctive normal form, decide whether or not there exists any satisfying interpretation. The answer to an instance of the problem is a single propositional constant.

\citeA{Gary:intractability} states the $SAT$ problem as follows:

It is important to notice that the $SAT$ problem is not a semantic problem. Once a particular notation is chosen as the propositional term algebra, an instance of the $SAT$ problem is given as a conjunctive normal form term in that propositional algebra, and the answer is a single constant in that algebra. As an algebra problem, it is amenable to algebraic solution. The algebraic computation required to solve the problem may be performed by a computer according to an algorithm. An algorithm for solving arbitrary instances of $SAT$ problems is an algorithm for manipulating the symbols of the algebra.

A variety of related problems are equivalent to $SAT$. A problem named $3SAT$ includes an additional restriction that every clause have exactly three literals. The proof that every $SAT$ problem has an equivalent $3SAT$ problem due to \citeA{Karp:reducibility}. A similar proof is presented by \citeA{Gary:intractability}. Given an instance of $SAT$, an algorithm can construct an equivalent instance of $3SAT$, and given the solution to that $3SAT$ problem, another algorithm can construct the solution of the original $SAT$ problem. Both construction algorithms have polynomial complexity.

A large variety of other $NP$-complete problems are each equivalent to $SAT$ in the same sense. Every problem in $NP$ can be algorithmically \emph{reduced} to one or more instances of $SAT$ problems, such that the the solution to the original $NP$ problem can be algorithmically extracted from the solutions to those $SAT$ problems. In every case, both the reduction of the problem and the extraction of the solution can be performed in polynomial time. A variety of such algorithms are reported in \citeA[chapter 3]{Gary:intractability}.