"Is progress in SAT solving the sole result of hardware advancement? Time Leap Challenge compared 20-year-old SAT solvers on new computer hardware and modern SAT solvers on 20-year-old computer hardware. Although hardware improvements make old solvers faster, algorithmic progress dominates and drives today's SAT solving."*

Pretty cool given computing progress over the last 20 years:

  1. CPUs sped up 40-60x
  2. GPU FLOPS/$ increased ~10,000x

  1. https://www.cpubenchmark.net/year-on-year.html
  2. https://en.wikipedia.org/wiki/FLOPS#Hardware_costs

And yet, despite tremendous progress accelerating continuous optimization workloads, there are still no competitive GPU-based SAT solvers. I wonder why?

It's not just GPU. There are not even good multicore SAT solvers. State of the art SAT algorithms are serial and they don't parallelize.

It shares short conflict clauses between parallel solvers and achieves superlinear speedup in some cases, e.g., 4 parallel solvers solve faster than one forth of the single solver soolution time.

Short conflict clauses are rare so there is little communication between solvers required.

CryptoMiniSAT: https://github.com/msoos/cryptominisat

Author's goal to have solver that is good in computing range from single CPU up to cluster. Judging from CryptoMiniSAT successes, he has mostly reached the goal.