4 ms·
This 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 complexi
by mohsen1 1y ago
This 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
- mzl 1y agoAny tool that can solver hard problems will also have non-trivial runtime behavior. That is an unfortunate fact. But you are also correct in that combinatorial optimizaton solvers (CP, SAT, SMT, MIP, ...) often have quite sharp edges that are non-intuitive. For the iOS AutoLayout, what kind of issues have you seen, and how complex were the problems?
- mohsen1 1y agoIt’s a familiar error for iOS developers: “constraints are too complex to solve”
- hwayne 1y agoEven 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")