A Dumb Introduction to Z3

https://www.hakank.org/

Think about it purely in the set-theoretic sense "what is the minimal set containing 37 elements?" the answer is "the set containing 37 elements."

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 internally, so to speak)

It now wants to give goal the lowest possible value it can assign it, even if not satisfiable, to start the process. It looks at the bounds of c1, c2 and c3 to determine this, and they're all -infinity.

The lowest possible value of goal is -infinity, which the optimizer has no idea what to do with, and just basically gives up. When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal:

(+ c1 c2 c3) |-> (* (- 1) oo)

A different optimization algorithm, like one that works "top-down" (find the first satisfiable assignment, then make it better) would actually be able to converge. I think OptiMathSAT would be able to handle it because it also does top-down reasoning for this.

CP solvers and MIP solvers all enforce variable bounds so they don't have this issue.

Yes, it picked a valid result and gave up.

I got a similar nonsensical result in my run-ins[1] in with SAT solvers too, until I added a lowerbound=0.

The "real life" follow-up question in interviews was how to minimize the total number of intermediate rows for a series of joins within in a cost-based optimizer.

[1] - https://gist.github.com/t3rmin4t0r/44d8e09e17495d1c24908fc0f...

In general, for modeling layers embedded in programming languages, having operator overloading makes the code so much better to work with. Modeling layers where one has to use functions or strings that are evaluated are much harder to work with.

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 it is more flexible, and then move to SMT style models like Z3 if or when it is needed. One of the reasons I think CP is a better initial choice is the focus on higher-level concepts and global constraints.

For the iOS AutoLayout, what kind of issues have you seen, and how complex were the problems?

    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")