3 ms·
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
by _a_a_a_ 3y ago
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?
- 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