SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example.<p>Does anyone have good suggestions for what to use SAT solvers for?
Sudoku may be a poor example for illustrating some of the overarching points of this series of blog posts, which I take to be that modern SAT solvers are, as someone described them in a previous thread, "little diamonds of engineering", that they embody decades of research, that you can exploit their power cheaply and easily, and that it might take significant effort to beat them if you have a non-trivial problem.<p>Since specialized solvers <i>do</i> thrash SAT-based solvers for conventional Sudoku, the author focuses the example less on absolute performance and more on simplicity, rapid prototyping, and comparison to casual non-SAT implementations. But conventional Sudoku is a small problem, and in most cases the SAT-based solver makes so few decisions that it doesn't benefit much from CDCL. Consider here[1] the comparison to JCZSolve(ZSolver) that the author mentions in part 1 of the series:<p>For 17-clue puzzles (which are generally very easy), JCZSolve is 50x as fast as Minisat, and it makes on average ~1.9 decisions per puzzle compared to Minisat's ~3.0. But if you look at the hardest dataset JCZSolve is only 10x as fast as Minisat, and it makes on average ~365 decisions per puzzle compared to Minisat's ~121. I'm not aware of a highly specialized and optimized Solver for 16x16 clue or larger Sudoku, but given this trend my guess is that it would take a lot of effort to write one that's faster than what you get with Minisat for free.<p>[1] <a href="https://github.com/t-dillon/tdoku/blob/master/benchmarks/GCE-c2-standard-4_clang-8_O3_native" rel="nofollow">https://github.com/t-dillon/tdoku/blob/master/benchmarks/GCE...</a>
SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types[1], and Djinn uses one for suggesting functions given a type[2]. Similarly to Djinn, Edwin Brady gave a presentation on using an SMT solver to do live code suggestions/implementation inference in the successor to Idris[3].<p>[1] <a href="https://ucsd-progsys.github.io/liquidhaskell-blog/" rel="nofollow">https://ucsd-progsys.github.io/liquidhaskell-blog/</a><p>[2] <a href="http://lambda-the-ultimate.org/node/1178" rel="nofollow">http://lambda-the-ultimate.org/node/1178</a><p>[3] <a href="https://www.youtube.com/watch?v=mOtKD7ml0NU" rel="nofollow">https://www.youtube.com/watch?v=mOtKD7ml0NU</a>
Links to previous HN discussions of this article:<p><a href="https://news.ycombinator.com/item?id=19953213" rel="nofollow">https://news.ycombinator.com/item?id=19953213</a><p><a href="https://news.ycombinator.com/item?id=17684502" rel="nofollow">https://news.ycombinator.com/item?id=17684502</a><p><a href="https://news.ycombinator.com/item?id=17778770" rel="nofollow">https://news.ycombinator.com/item?id=17778770</a>
Previously posted 4 months ago and 1 year ago: <a href="https://hn.algolia.com/?dateRange=all&page=0&prefix=false&query=modern%20sat%20solvers%3A%20fast&sort=byPopularity&type=story" rel="nofollow">https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...</a>
If you’re looking for a higher-level interface to SAT, SMT, and general constraint solvers, I can recommend MiniZinc: <a href="https://www.minizinc.org/index.html" rel="nofollow">https://www.minizinc.org/index.html</a>
Whenever I read about SAT solvers I think of Prolog and Minikanren and friends. Is there a relationship there? Do they use similar algorithms? I know that backtracking (mentioned in the article) is a thing in Prolog at least.
The programming language Mercury which is a functional, predicate based, moded language uses something like a precursor to a sat solver to "run" the program. As in you can ask for the input of a function to make your program true.<p>I imagine all sorts of things can be done like this, and the sat solver is useful for verifying correctness.
This is an interesting read, but I'd be interested in a more large-scale benchmark. Right now it could be possible that the SAT solver is just better optimized for the particular platform, instead of the SAT solver being superior algorithm-wise.
You can also watch the talk from same author about the same subject here - <a href="https://www.youtube.com/watch?v=x2XtpCn0-bM" rel="nofollow">https://www.youtube.com/watch?v=x2XtpCn0-bM</a>