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).
To view the full DeepSAT writeup, click here.
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.