Skip to content

Comment on A dumb introduction to z3parent

Comments

is this kind of like “if the answer to your minimization problem is negative infinity, the answer is undefined behavior”?

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...

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.