6 ms·
GPU accelerated SMT constraint solving (2021)
- drdrey 3y agoWould 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?
- jfmc 3y agoThey should compare with other multithreading and GPU approaches for SAT/SMT solving (like https://www.win.tue.nl/~awijs/articles/parafrost_gpu.pdf 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 https://news.ycombinator.com/item?id=13667380 from actual experts.
- bmc7505 3y agoAnother related thread from last month: https://news.ycombinator.com/item?id=36084461 https://news.ycombinator.com/item?id=36084461
- mk_stjames 3y agoSMT here refers to https://en.wikipedia.org/wiki/Satisfiability_modulo_theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories not https://en.wikipedia.org/wiki/Simultaneous_multithreading https://en.wikipedia.org/wiki/Simultaneous_multithreading and not https://en.wikipedia.org/wiki/Surface-mount_technology https://en.wikipedia.org/wiki/Surface-mount_technology in case anyone else was sitting there wondering for too long like I was.
- ris 3y agoThis 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.
- DougBTX 3y agoIs unguided random sampling more likely to find a solution than in-order enumeration?
- PartiallyTyped 3y agoIn 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 https://en.wikipedia.org/wiki/Geohash
- tesdinger 3y agoHow does its performance compare to CP-SAT, included in OR-TOOLS?
- amelius 3y agoSince this is evaluating large boolean expressions, wouldn't it make more sense to use an FPGA for this?
- dgreensp 3y agoI 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.
- _a_a_a_ 3y agoIf 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?
- dgreensp 3y agoGoogle or YouTube could probably give you a good nutshell answer to that.
- rotifer 3y agoThe 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-revolution-of-sat/fulltext https://cacm.acm.org/magazines/2023/6/273222-the-silent-revo...
- calebh 3y agoFrom 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.
- sesuximo 3y agoI’d recommend reading about DPLL and CDCL. These are relatively simple concepts that you can code up yourself