This website provides a deterministic polynomial time algorithm that decides satisfiability for 3-SAT. Also provided is code for a serial version with no 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. Lemma 4.2 offers a special case for linear time.


Algorithm

For a brief description of the algorithm.

The complexity analysis ignores all efficiencies.

A serial C++ version without non-trivial efficiencies is available at GitHub. 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, in polynomial time.

The Team: Ortho Flint, Asanka Wickramasinghe, Jay Brasse and Chris Fowler.

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