Wrote an article on solving my favorite number logic puzzle using a mixture of #Python and Microsoft Research's Z3: https://ahf.me/articles/2020/05/01/solving-binary-puzzles-using-python-and-z3/
@ahf Only had time to skim for the moment, but looks like fun :-D. I used STP for static analysis in grad school but it seems like Z3 has become more popular since. Wonder how they compare...
@sporksmith Cool! I haven't had a look at STP before. I got very curious about Z3 after I read an article about using Z3 together with a C fuzzer to eliminate branches in code paths to reach higher coverage. I'm very impressed with how easy it is to program it.
Since then, played around with its optimizer a bit and found the API UX pretty lackluster: You can put in problems it doesn't support and rather than blow up, it will often just return non-optimal results.
As a makeshift CP solver, it does seem excellent though!
@fuglede Cool! I stopped playing AoC way too early in 2018, but that puzzle looks fun. Have you used other similar libraries?
@ahf Probably not per se. As in, can't say SMT is something I've encountered regularly.
But as I'm sure you know, there's a huge market for optimization libraries in general, which Z3 ends up being a competitor in with its functionality (the AoC puzzle could also be solved with one of a billion LP solvers, but Z3 was way better; my own AoC solution used scipy.optimize and took 6 hours to run).
In the direction of theorem proving, I get the feel that Lean (also MS) is picking up a lot of speed.
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!