Wrote an article on solving my favorite number logic puzzle using a mixture of and Microsoft Research's Z3: ahf.me/articles/2020/05/01/sol

@ahf Z3 is cool. First came across it during adventofcode.com/2018/day/23 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.

· · Web · 0 · 0 · 1
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!