z3 - 整数变量的最小值和最大值

Question

让我们假设一个非常简单的约束：solve(x > 0 && x < 5).

xZ3（或任何其他 SMT 求解器，或任何其他自动技术）能否计算满足给定约束的（整数）变量的最小值和最大值？

在我们的例子中，最小值为 1，最大值为 4。

Answer 1

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)

Answer 2

正如莱昂纳多指出的那样，这在之前已详细讨论过：确定任意命题公式中变量的上限/下限。另请参阅：如何优化 Z3 中的一段代码？（PI_NON_NESTED_ARITH_WEIGHT 相关）。

总而言之，可以使用量化公式，也可以迭代。不幸的是，这些技术并不等同：

• 量化方法不需要迭代，并且可以在一次调用求解器中找到全局最小值/最大值；至少在理论上。但是，它确实会产生更难的公式。因此，后端求解器可能会超时，或者只是返回“未知”。

• 迭代方法为后端求解器创建了简单的公式来处理，但如果没有最优值，它可以永远循环；最简单的例子是试图找到Int最大值。量化版本可以很好地解决这个问题，快速告诉你没有这样的价值，而迭代版本会无限期地继续下去。如果您不提前知道您的约束确实有最佳解决方案，这可能是一个问题。（不用说，“足够”的迭代次数通常很难猜测，并且可能取决于随机因素，例如求解器使用的种子。）

还要记住，如果手头有针对问题域的自定义优化算法，通用 SMT 求解器不太可能胜过它。

Answer 3

z3 现在支持优化。

from z3 import *

o = Optimize()
x = Int( 'x' )
o.add(And(x > 0, x < 5))
o.maximize(x)
print(o.check())  # prints sat
print(o.model())  # prints [x = 4]

这个特殊的问题是一个整数程序。