A polynomial time (heuristic) SAT algorithm
Charles Sauerbier · arXiv (Cornell University) · 2002
ABSTRACT — [Note: See addendum prefacing this paper, as a hole has been determined to exist in the algorithm as presented in this paper.] An algorithm of two parts is presented that determines existence of and instance of an assignment satisfying of instances of SAT. The algorithm employs an unconventional approach premised on set theory, which does not use search or resolution, to partition the set of all assignments into non-satisfying and satisfying assignments. The algorithm, correctness, and time and space complexity proofs are given. KEY TERMS — Algorithms, complexity, computation theory, satisfiability, set theory. ADDENDUM A hole has been found in the algorithm as presented, where an eleventh hour change admits a path inconsistency resulting in false affirmation of existence of a solution at the end of Part A of the algorithm. This results from cyclic closure of paths against a root other than that supporting the path as its origin. Existence of a path can still be established using the algorithm where Part B is used to search the reduced space represented in the results of Part A. However, to fully and completely effect this check is to nullify any benefit of having performed Part A in alternative to the motivating basis from which Part A was derived. A reversion back to the more primitive and computationally expensive in the worst case is being composed. For now the algorithm as presented can be said to be no better than a polynomial time heuristic SAT algorithm. The algorithm has not been found to give false negatives. The underlying mathematical premises motivating the algorithm do not support the algorithm giving false negatives. In making the change the impact to consistency was not given sufficient consideration. Reversion to the mechanism from which the version given here derives results in a increase in the exponent value of 3 for worst-case performance of the algorithm, though best-case performance is potentially improved by in reduction of the exponent value for some instances of SAT. S A polynomial time (heuristic) SAT algorithm