Would a SQL optimizer use a generic solver as described here or are there special algorithms for such problems?
A dumb introduction to z3
31–40 of 42 posts
Re: A dumb introduction to z3
#32Those of you wondering about how to use z3, please consider coding in static python (not z3py) and then transpile to smt2. You'll be able to solve bigger problems with familiar/legible syntax and even use the code in production.
Can you expand on that? What you mean by static python?
Re: A dumb introduction to z3
#33Does someone, with some experience on this subject, has an opinion on the best solver with binding in Python for a begginer? The OP use Z3 but also mentionned MiniZinc and I heard about Google OR-Tools.
If you want to work in Python, I would either use OR-Tools which has a Python library or CPMpy which is a solver agnostic Python library using numpy style for modeling combinatorial optimization problems. There is a Python package for MiniZinc, but it is aimed at structuring calls to MiniZinc, not as a modeling layer for MiniZinc. Personally, I think it is better to start with constraint programming style modeling as…
If you do want to start with SMT though, z3 has quite good bindings. I found it intuitive to use, and its ability to give you answers to very hard problems is like owning a magic wand.
Re: A dumb introduction to z3
#34Those of you wondering about how to use z3, please consider coding in static python (not z3py) and then transpile to smt2. You'll be able to solve bigger problems with familiar/legible syntax and even use the code in production.
Can you expand on that? What you mean by static python?
z3py is going through python’s interpreter to talk to the c++ core of z3; this creates a performance bottleneck as the system size grows. The native input language of z3 is smt2, so coding in plain old python with type hints and then transpile to smt2 would, ideally, help with the bottleneck enabling solving of increasingly complex systems.
That’s how I understand it at least! Someone please correct me if I’m off base.
Re: A dumb introduction to z3
#35I’d be curious if someone here could explain the initial nonsensical answer for the coin change problem. I understand that not giving the lower bounds effectively lets it find an arbitrarily low (generally very negative) number of coins that satisfy the problem (so the minimization would basically go to negative infinity). But why would it respond with “to get 37 in the lowest number of coins I’ll give you 37 ones”?…
It has to do with the algorithm Z3 uses to do optimization I think (there are different ones). It works in a "bottom-up" manner, first giving the minimization goal its lowest possible value and then it tries to "work its way up" to something satisfiable. So in this case there's something like: goal = c1 + c2 + c3 minimize goal (even if you write minimize (c1 + c2 + c3), it's still creating that goal variable internal…
Thanks for the explanation!
> When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal: (+ c1 c2 c3) |-> (* (- 1) oo)
This part is what I was looking for. I was surprised that the behavior wasn’t accompanied by any warnings in the article.
Re: A dumb introduction to z3
#36I also was inspired to play around with Z3 after reading a Hillel Wayne article. I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips
I guess z3 is fine with it, but it confuses me that they decided pips wouldn't have unique solutions
I actually wasn't aware of this either.
Z3 is fine with it--its job is to find any satisfying model. The possible outcomes are "the puzzle is solvable and here's a solution" or "the puzzle isn't solvable."
Re: A dumb introduction to z3
#37Does someone, with some experience on this subject, has an opinion on the best solver with binding in Python for a begginer? The OP use Z3 but also mentionned MiniZinc and I heard about Google OR-Tools.
It really depends on the kind of solving you want to do. Mathematical optimization, as in finding the cheapest/smallest/whatever solution that fits a problem? OR-Tools. Satisfaction problems, like finding counterexamples in rulesets or reverse engineering code? Z3.
Re: A dumb introduction to z3
#38This was such a pleasure to read! Thank you for sharing! My understanding is that solvers are like regexes. They can easily get out of hand in runtime complexity. At least this is what I have experienced from iOS's AutoLayout solver
Even worse than that, SMT can encode things like Goldbach's conjecture:
from z3 import \*
a, b, c = Ints('a b c')
x, y = Ints('x y')
s = Solver()
s.add(a > 5)
s.add(a % 2 == 0)
theorem = Exists([b, c],
And(
a == b + c,
And(
Not(Exists([x, y], And(x > 1, y > 1, x \* y == b))),
Not(Exists([x, y], And(x > 1, y > 1, x \* y == c))),
)
)
)
if s.check(Not(theorem)) == sat:
print(f"Counterexample: {s.model()}")
else:
print("Theorem true")Re: A dumb introduction to z3
#39I also was inspired to play around with Z3 after reading a Hillel Wayne article. I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips
I love how you create dataclasses to abstract over constraints!
Re: A dumb introduction to z3
#40[deleted]