z3 - Z3：设置起始值

Question

我可以要求 Z3 从某些起始值搜索以满足约束吗？

说，如果我有两个RealExprs xand y，并且我有x==y作为约束。我可以要求 Z3 搜索x=-9999, y=-9997这样 Z3 可能会返回给我的模型x=-9998 and y=-9998并说“SAT”吗？

Answer 1

据我了解您的问题，您正在寻找最大化/最小化问题的解决方案，即以下函数

f(x, y) = |x + 9999| + |y + 9997|

与约束一起x = y。如该问题的答案所述，Z3 目前不直接支持此功能。但是，如前所述，您可以尝试通过在 Python 循环中查询 Z3 来解决此类问题，该循环将先前找到的解决方案添加为下一个查询的新约束。