GPU accelerated SMT constraint solving (2021) | Hacker News Reader

GPU accelerated SMT constraint solving (2021)

blog.osiris.cyber.nyu.edu

64 pointszdw15 comments

Open articleView on HN

SMT here refers to

https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

not

https://en.wikipedia.org/wiki/Simultaneous_multithreading

and not

https://en.wikipedia.org/wiki/Surface-mount_technology

in case anyone else was sitting there wondering for too long like I was.

I know a little about SAT solvers. I wrote a SAT library, based on MiniSAT, used in production in the Meteor package manager, and more recently I’ve used my SAT solver as part of a sudoku solver that can solve standard Sodukos and also exotic variants, quite efficiently.

While technically, SAT has exponential algorithmic complexity, in practice, SAT solvers can solve problems with thousands of boolean variables quite quickly. “Guess and check” on these same problems would take the lifetime of the universe. CPU vs GPU does not remotely cover the difference.

Basically, I have no idea what this author is going on about, this could be a joke for all I know.

If a SAT solver is so efficient, distinctly not taking the lifetime of the universe to produce an answer, what exactly is it about these things that makes them so efficient; what is it that guides them? How do they work at a high level, that they seem so good at solving stuff?

Google or YouTube could probably give you a good nutshell answer to that.

The Communications of the ACM article "The Silent (R)evolution of SAT" [1] gives an overview of some of the techniques used in SAT solvers. I believe it was posted on HN fairly recently.

[1] https://cacm.acm.org/magazines/2023/6/273222-the-silent-revo...

From what I learned from covering this in my Master's degree, the efficiency comes from the DPLL algorithm, which can efficiently solve many real world inputs, but still takes exponential time in the worst case.

I’d recommend reading about DPLL and CDCL. These are relatively simple concepts that you can code up yourself

This appears.. naive at best.

But it appears to get distracted by the performance of the random number generation approach it's going to use - which, for the quality of random numbers they would need for this, shouldn't be a problem at all as far as I can tell.

Is unguided random sampling more likely to find a solution than in-order enumeration?

In order enumeration of parameters / candidates?

If so, then I'd argue that yes random search is more likely. When we do hyper parameter tuning in ML, random search beats grid search in efficiency. The higher the dimensionality of the problem, the worst grid search is going to be because you will spend a lot of time at the boundaries.

If you are doing Grid Search, then you might as well use a space filling curve, find a promising block, and increase the resolution. This is how GeoHash [1] works more or less.

On the other hand, if a single solution exists, then it is improbable that you will find it via random search.

There are more complex solutions to exact constraint solving, but perhaps they don't scale particularly well.

[1] https://en.wikipedia.org/wiki/Geohash

Would have been nice to see how their approach (GPU based fuzzing of SMT formulas) compares to traditional CPU solvers, did I miss it?

Was this a one-off or is there a follow up?

They should compare with other multithreading and GPU approaches for SAT/SMT solving (like https://www.win.tue.nl/~awijs/articles/parafrost_gpu.pdf from Armin Biere, or other works from Mate Soos). There has been a lot of research in this direction.

Other old HN thread (2017) with relevant comments https://news.ycombinator.com/item?id=13667380 from actual experts.

Another related thread from last month: https://news.ycombinator.com/item?id=36084461

Since this is evaluating large boolean expressions, wouldn't it make more sense to use an FPGA for this?

How does its performance compare to CP-SAT, included in OR-TOOLS?

Reply on news.ycombinator.com