4 ms·
How do your project and Z3 compare to (1) Logic programming tools like Prolog and (2) optimizers like scipy.optimize? All of these seem to find solutions to us
by pbronez 2y ago
How do your project and Z3 compare to (1) Logic programming tools like Prolog and (2) optimizers like scipy.optimize?
All of these seem to find solutions to user-provided constraint sets. They must be appropriate for different classes of problems, but it’s not obvious to me how that breaks out.
It’s, uh, been a long time since I last hand-rolled an optimization algorithm…
- philzook 2y agoThis is a tough comparison. They are very similar in some respects but also very distinct. Prolog has some operational flavor to it. You can predict what it'll do. It can be used as "just" a programming language akin to python with fairly little logical/mathemtical content. Declarative Prolog as in constraint logic programming is in the realm of attacking similar logical problems to z3. scipy.optimize is a grab bag of stuff. Some of it is pretty heuristic. It's all subject to floating point error, which is the devil we live with. The milp and lp solvers are relatives of how z3 handles linear inequality constraints. scipy.optimize doesn't treat logic at all really. It takes in mathematical multivariate functions and finds roots or minima. Z3 is intended to be mathematically rigorous. It is less operational than prolog. On big combinatorial problems (SAT, bitvector problems), it is probably a superior tool. It does have an optimization interface, I haven't used it much.