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.
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.
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.
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?
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.
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.
15 comments
[ 3.5 ms ] story [ 44.6 ms ] threadWas this a one-off or is there a follow up?
Other old HN thread (2017) with relevant comments https://news.ycombinator.com/item?id=13667380 from actual experts.
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.
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.
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
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.
[1] https://cacm.acm.org/magazines/2023/6/273222-the-silent-revo...