Z3 能否通过最大运算有效解决约束？答案

【问题标题】：Can Z3 effectively solve constraints with a max operation?Z3 能否通过最大运算有效解决约束？
【发布时间】：2016-11-16 07:54:54
【问题描述】：

假设我想解决以下约束：y == max(x, 0)。我能想到的是对以下内容进行编码（在 z3py 接口中）：If(x > 0, y == x, y == 0)。我的问题是：

Z3 是否会在内部将上述表达式转换为两个约束：x > 0 /\ y == x 和 x <= 0 /\ y == 0，然后在两个约束中的任何一个满足时对它们进行 OR 并返回 sat？
如果是这样，约束的数量似乎会随着max 操作的数量呈指数增长。我的系统有超过 100 个max。在 Z3 或任何其他求解器中是否有有效的解决方法？

谢谢！

【问题讨论】：

【解决方案1】：

使用python接口可以定义：

def mymax(x,y):
    return If(x > y, x, y)

这不会产生指数级的约束。

在许多情况下，只执行 max 规定的不等式的一侧就足够了。在这些情况下，引入一个新的变量 max_x_y 并断言

   max_x_y >= x, max_x_y >= y

当您还要求 max_x_y

【讨论】：

用mymax，如果我想表达y是x和0之间的最大值，我可以做solve(y==mymax(x, 0))，这很酷。但是 Z3 是否会在内部将 mymax 转换为两个约束，然后将它们 OR 放在一起，并在任一可满足时返回 sat？如果是这样，尽管If 使它看起来只是一个约束，但 Z3 是否将其视为两个约束，从而使复杂性呈指数级增长？
@queeten 根据问题的结构，运行时可能会或可能不会呈指数增长。请参阅我的答案中的 cmets。如果我在这里错了，请纠正我 Nikolaj。此外，关于可能仅使用不等式的一侧的有趣点。

【解决方案2】：

如果您的所有最大操作都出现在 y > max(x, 0) 形式的上下文中，我会将它们编码为 (and (> y x) (> y 0)) (SMT-LIB)，它没有分支。我不确定使用 Python 接口的语法是什么。

【讨论】：

这是个好技巧！但是你会怎么做y == max(x, 0)呢？有没有一种通用的方法可以在没有分支的情况下有效地表达max？
最简洁的方法是 Nikolaj 所说的，If(x > y, x, y)。我怀疑您是否可以笼统地说通过引入这样的约束是否会使搜索空间翻倍。这取决于问题和求解器的内部结构。如果 x > y 是从问题的其他地方知道的，那么 Z3 将有效地将 If(x > y, x, y) 替换为 x 或 y 并且不会有分支。如果 x > y 不能从上下文中确定，那么它可能必须被分支。
在这种情况下，有关求解器和算法的知识可以帮助您假设对性能的影响。然而，像 Z3 这样的求解器的整体性能很复杂，并且取决于许多相互权衡的因素。一般来说，您必须使用相关基准测试您的假设，以确定它们是否在您感兴趣的特定问题上得到证实。