points by mate_soos 9 years ago

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 :)

dang 9 years ago

> I don't understand how it got this high at ycombinator

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.)

mafribe 9 years ago
 
   If you want to look at good SAT 
   solvers, look ... CryptoMiniSat.

Any personal relationship with CryptoMiniSat? ;)

  • mate_soos 9 years ago

    Considering that CryptoMiniSat got 3rd place (after 1st and 2nd both being lingeling) in Parallel SAT solving the last competition, I think it was fair to include it. Sure, it's mine, but I also put it at the end :) Other solvers that are good to look at: glucose and riss. Note that a lot of solvers are variations of MiniSat. riss, ligeling, PrecoSat and CryptoMiniSat are the only ones that substantially differ from MiniSat.

    • dlo 9 years ago

      Thanks for the recommendations. I love SAT solvers and have been looking for a way to get into them.

mtve 9 years ago

Google does not know "COPMinisat", would you please clarify?

PicoSAT is also small and easy to embed, however in CryptoMiniSat we trust, thank you very much!

pettou 9 years ago

Please, do you have any recommendations for books about SAT solving for beginners?