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.

For a brief description of the algorithm.