This approach is unworkable because:
* propagation needs modification of the watchlist (or it needs to have all literals of all clauses attached, which is incredibly slow and also unworkable)
* propagation is actually only about 50-60% of what a solver is doing: conflict resolution, clause database management and inprocessing takes a lot of time
* propagation is hard to parallelize as you need to update a global data structure of propagated literals and then act on that
This proposal will not work (and I sure it did not, if it was ever tried) and I don't understand how it got this high at ycombinator. If you want to look at good SAT solvers, look at lingeling, COPMinisat, MiniSat, or CryptoMiniSat. You may learn a lot from them. Easy starting is MiniSat. Good luck :)
Oh that's easy: because most of us know nothing about SAT solvers other than (maybe) what they are and that they're cool. We need people like you to teach us, so I'm glad you showed up! (A great example of https://meta.wikimedia.org/wiki/Cunningham's_Law.)
If you want to look at good SAT
solvers, look ... CryptoMiniSat.
PicoSAT is also small and easy to embed, however in CryptoMiniSat we trust, thank you very much!
One of its variants won the Main track of the SAT Competition of 2016, see
For all the solvers' source codes, see
The annual SAT competition http://www.satcompetition.org has a track for parallel solving.
See [2, 3, 4] for an overview of the field.
 M. J. H. Heule, O. Kullmann, S. Wieringa, A. Biere, Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.
 S. Hölldobler, N. Manthey, V. H. Nguyen, J. Stecklina, P. Steinke, A Short Overview on Modern Parallel SAT-Solvers.
 S. Wieringa, K. Heljanko, Asynchronous Multi-Core Incremental SAT Solving.
 Y. Hamadi, C. M. Wintersteiger, Seven Challenges in Parallel SAT Solving.
Wow, that's interesting! Are there any other examples where a sequential algorithm beats a parallel one?
This article by Moshe Vardi and this one by Dick Lipton are a nice introduction to the mystery of SAT solvers.
If I had to guess, I would think implementing a SAT solver on a GPU is quite hard. Many branches etc.
It seems Mr Costa has graduated, but the link to his thesis points to an empty pdf.
from May 2014 [pdf]