Wrote an article on solving my favorite number logic puzzle using a mixture of and Microsoft Research's 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.

@ahf Z3 is cool. First came across it during when its optimization methods beat all other approaches.

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.

Sign in to participate in the conversation

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!