The article series Modern SAT Solvers: Fast, Neat, and Underused[1] argues that we don't use generic problem solvers enough in our daily engineering work.
A generic solution won't beat a hand-optimised specific solution, but if you're good at phrasing your problem in the right way, you can get 80 % of the way there with 20 % of the effort by using a generic solver.
Z3, being an even more generic SMT solver rather than "just" a SAT solver, should allow you to do even more with less.
I've long wanted to integrate this type of solver into my workflow more, because I think that if I can make it into more of a habit, it would provide insane leverage for prototyping. Does anyone have experience using these techniques for that?
A generic solution won't beat a hand-optimised specific solution, but if you're good at phrasing your problem in the right way, you can get 80 % of the way there with 20 % of the effort by using a generic solver.
Z3, being an even more generic SMT solver rather than "just" a SAT solver, should allow you to do even more with less.
I've long wanted to integrate this type of solver into my workflow more, because I think that if I can make it into more of a habit, it would provide insane leverage for prototyping. Does anyone have experience using these techniques for that?
[1]: https://codingnest.com/modern-sat-solvers-fast-neat-underuse...