3 ms·
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 SA
by dgreensp 3y ago
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.
- _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