P = NP

A Polynomial Time Algorithm for 3-SAT

This website provides a deterministic polynomial time algorithm that decides satisfiability for 3-SAT. Also provided is code for a serial version with no non-trivial efficiencies. We tried to be as informal as possible for general consumption while maintaining the necessary mathematical rigour. The algorithm has been released so that researchers, companies and governments can use it for whatever purpose they may have.

Regarding the paper, observe that lemma 4.1 establishes that the algorithm will not claim that a 3-SAT G, is unsatisfiable if G has at least one solution. Additionally, lemma 4.3 establishes that the algorithm is polynomial and the theorem establishes that the algorithm always detects unsatisfiability, specifically with respect to any three literals of G. Lemma 4.2 offers a special case for linear time.

The example 3-SAT from the paper is depicted above before and after processing if pre-processing were to be bypassed. The literal associated with the endpoint having all red edges belongs to no solution, determined after the first two red edges were removed. ie. evaluated to be zero.

Paper

The complexity analysis ignores all efficiencies.

Proof

Github

A serial C++ version with trivial efficiencies is available at GitHub which determines satisfiability only. We fairly call this version naive, although it does provide the most insight for study.

An optimized C code version exists, that will construct a solution for a satisfiable 3-SAT. It has the same polynomial bound.

Code

Generalization

The deterministic polynomial time algorithm that determines satisfiability of 3-SAT can be generalized for SAT.

SAT

The Team

Ortho Flint

Ortho Flint

Asanka Wickramasinghe

Asanka Wickramasinghe

Jason Brasse

Jason Brasse

Special thanks and acknowledgements to: Ge Baolai of SHARCNET and Steven Beauchemin from the University of Western Ontario.