# DeepSAT - An Often Polynomial-Time Program for Solving the Satisfiability Problem

##
ABSTRACT

DeepSAT is a program which solves the well-known satisfiability problem.

The algorithm generalizes the traditional conflict-driven clause learning by introducing new variables during the run. The superior performance of DeepSAT results from the greater power of the extended-resolution proof language (used by DeepSAT) vs the resolution proof language (used by traditional solvers).

Discussion includes benchmark data showing polynomial growth of runtime and comparison to traditional solvers, description of the algorithm, and theoretical discussion (including comments on the P ?= NP question).

##
VIEW THE FULL WRITEUP

To view the full DeepSAT writeup, click here.

##
COMMENTS FROM THE AUTHOR

I self-publish this writeup because I think it could be of interest to both the practical SAT-solving
community and the theoretical computer science community,
even though the writeup is in a pretty rough state,
not yet suitable for a journal. I would also like to get feedback on the ideas in the writeup and
suggestions for improving the algorithm. DeepSAT is currently being used commercially for formal
verification, and even though it shows polynomial-time behavior on hard problems
such as ALU verification and XOR-heavy verification,
the runtimes are often too slow to be useful commercially. Theory suggests that much
faster runtimes should be possible (for example, O(N*log(N)) proofs exist,
but DeepSAT generates O(N^2.5) or worse proofs). I am hoping people smarter than me can help me
improve these poor results.
Please contact me with your comments and suggestions by clicking here.

Some ideas in this writeup are controversial. But some points are beyond dispute: the refutations
DeepSAT generates have been verified by the well-respected proof-checking program DRAT-TRIM. The
runtime and proof sizes in the benchmarks are as stated.

I apologize for the rough state of this writeup. In particular, the proof of Theorem 1 in the appendix
is incomplete - I have not yet added the lemma which strengthens the result to length-2 clause proofs.
In addition, section 5 was written when I was not aware of the existence of O(N*log(N)) size proofs
for XOR and ALU problems, so this section needs revision to include these facts.
Finally, the appearance is rough, the equations are in a crude form, some of the charts and tables
are untidy, and the old name for DeepSAT which was "Tortoise" still appears in some of the
figures.