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

Question

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

Z3(或任何其他SMT求解器,或任何其他自动技术)可以计算x满足给定约束的(整数)变量的最小值和最大值吗？

在我们的例子中,最小值为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求解器不可能胜过它.