This approach is unworkable, it has been demonstrated many times. I have not only been developing a SAT solver for >7 years (with >9000 commits) but also have participated in the SAT competition in all these years. I used to get a proposal like this a lot (thankfully, they dried up). None of them made it work. I used to work on programming GPGPUs in a professional setting, (rainbow table generators&lookup systems), so I'm not unfamiliar with their advantages and restrictions.
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
* etc
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 :)
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 * etc
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 :)