让我们假设一种非常简单的约束： solve(x > 0 && x < 5)
Z3（或任何其他SMT求解器，或任何其他自动技术）可以计算（整数）变量的最小值和最大值x满足给定约束条件？
在我们的例子中，最小为1，最大值为4。
Answer 1:
正如莱昂纳多指出的，对此进行了详细讨论之前： 确定上/对任意命题公式中的变量下界 。 另请参阅： 如何在Z3优化的代码？ （PI_NON_NESTED_ARITH_WEIGHT相关） 。
总之，一个可以使用一个量化的公式，或者去重复。 不幸的是，这些技术是不相等的：
量化方法不需要迭代，并且可以找到该解算器的单一调用全球最小/最大; 至少在理论上。 但是，它不会产生更难公式。 因此，后端求解器超时，或简单地返回“未知”。
迭代方法创造了后端解算器来处理简单的公式，但它可以永远循环下去，如果没有最优值; 最简单的例子正在试图找到最大的
Int值。 量化版本可以快速地告诉你，有没有这样的价值很好地解决这个问题，而迭代版本将无限期地继续下去。 这可能是一个问题，如果你不提前知道时间，你的约束也有一个最佳的解决方案。 （不用说，有“足够的”迭代次数通常是难以猜测，并可能取决于随机因素，如求解器使用的种子。）
也请记住，如果有一个问题域手头定制的优化算法，这是不可能的通用SMT求解器可以超越它。
Answer 2:
Z3还没有优化（最大化/最小化）目标函数或变量支持。 我们计划增加这种能力，但它不会发生在今年。 在当前版本中，我们可以“优化”通过解决每个迭代我们添加额外的约束若干问题的目标函数。 我们知道，我们找到了最佳的时候问题就变得不可满足。 下面是描述了一个思路一小Python脚本。 该脚本最大化变量的值X 。 为最小化，我们只需要替换s.add(X > last_model[X])与s.add(X < last_model[X]) 这个脚本是非常幼稚的，它执行了“线性搜索”。 它可以在许多方面得到改善，但它展现了基本思路。
您也可以在线试用这个脚本在： http://rise4fun.com/Z3Py/KI1
请参阅以下有关的问题： 确定上/任意的命题公式在下界变量
from z3 import *
# Given formula F, find the model the maximizes the value of X
# using at-most M iterations.
def max(F, X, M):
s = Solver()
s.add(F)
last_model = None
i = 0
while True:
r = s.check()
if r == unsat:
if last_model != None:
return last_model
else:
return unsat
if r == unknown:
raise Z3Exception("failed")
last_model = s.model()
s.add(X > last_model[X])
i = i + 1
if (i > M):
raise Z3Exception("maximum not found, maximum number of iterations was reached")
x, y = Ints('x y')
F = [x > 0, x < 10, x == 2*y]
print max(F, x, 10000)
文章来源: Minimum and maximum values of integer variable
