z3py中一组变量的最大值和最小值答案

【问题标题】：Max and Min of a set of variables in z3pyz3py中一组变量的最大值和最小值
【发布时间】：2021-07-06 15:43:47
【问题描述】：

我有一个问题，我想将一个实变量的范围限制在另一组实变量的最大值和最小值之间。

s = Solver()
y = Real('y')
Z = RealVector('z', 10)
s.add(And(y >= min(Z), y <= max(Z)))

有没有办法在 z3py 中做到这一点？

【问题讨论】：

Z 和 y 还依赖于许多其他约束。这里没有包括它们。

标签： z3 smt z3py

【解决方案1】：

您可以使用 Axel 的解决方案；尽管那需要您创建一个额外的变量并且还断言比需要更多的约束。此外，它不允许您将min 和max 用作简单的函数。以函数式的方式对其进行编程可能会更容易，如下所示：

# Return minimum of a vector; error if empty
def min(vs):
  m = vs[0]
  for v in vs[1:]:
    m = If(v < m, v, m)
  return m

# Return maximum of a vector; error if empty
def max(vs):
  m = vs[0]
  for v in vs[1:]:
    m = If(v > m, v, m)
  return m

另一个区别是，在函数式风格中，如果向量为空，我们会抛出错误。在另一种风格中，结果基本上是不受约束的。（即 min/max 可以取任何值。）您应该考虑哪种语义适合您的应用程序，以防您传递的向量可能为空。（至少，你应该改变它，让它打印出更好的错误信息。目前，如果给定一个空向量，它会抛出一个IndexError: list index out of range 错误。）

现在你可以说：

s = Solver()
y = Real('y')
Z = RealVector('z', 10)
s.add(And(y >= min(Z), y <= max(Z)))
print (s.check())
print (s.model())

打印出来：

sat
[z__7 = -1,
 z__0 = -7/2,
 z__4 = -5/2,
 z__5 = -2,
 z__3 = -9/2,
 z__2 = -4,
 z__8 = -1/2,
 y = 0,
 z__9 = 0,
 z__6 = -3/2,
 z__1 = -3]

【讨论】：

感谢您的回答。这种方法的一个问题是 Z 是我的应用程序中的 IF() 条件列表： Z = [IF(a, v1, 0), IF(b, v2, 0), ...IF(b, v3 , 0)]。使用您提到的函数形式，结果始终是默认值（在最小值/最大值的情况下为 0/1）。
一点也不。它应该一切正常，因为函数使用z3的If；不是 Python 的if。如果您发现其他情况，请发布一些代码以显示此效果。

【解决方案2】：

您可以从 Hakan Kjellerstrand 的 collection of useful z3py definitions 中受益：

from z3 import *

#  Functions written by Hakan Kjellerstrand 
#  http://hakank.org/z3/
#  The following can be used by importing http://www.hakank.org/z3/z3_utils_hakank.py

# v is the maximum value of x
def maximum(sol, v, x):
  sol.add(Or([v == x[i] for i in range(len(x))])) # v is an element in x)
  for i in range(len(x)):
    sol.add(v >= x[i]) # and it's the greatest

# v is the minimum value of x
def minimum(sol, v, x):
  sol.add(Or([v == x[i] for i in range(len(x))])) # v is an element in x)
  for i in range(len(x)):
    sol.add(v <= x[i]) # and it's the smallest

s = Solver()
y = Real('y')
zMin = Real('zMin')
zMax = Real('zMax')
Z = RealVector('z', 10)

maximum(s, zMin, Z)
minimum(s, zMax, Z)

s.add(And(y >= zMin, y <= zMax))

print(s.check())
print(s.model())

【讨论】：