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

如何解决z3py中一组变量的最大值和最小值

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

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

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

解决方法

可以使用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,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]

,

您可以从 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,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,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())