用Z3或Z3py部分描述函数

2条回答

网友

1楼 · 编辑于 2024-09-19 23:32:30

在下面，您可以找到问题的直接SMT编码，除了求和要求的

(set-option :smt.mbqi true) ; also try false (e-matching instead of MBQI)

(declare-fun A (Int) Int)

(assert 
  (=
    10000
    (+ 
      (A 1)
      (A 2)
      (A 3)
      ; ...
      (A 99))))

; A(x) > 10 where 0<x<100
(assert (forall ((x Int))
  (implies
    (and (< 0 x) (< x 100))
    (> (A x) 10))))

; A(x) = 0 where x>= 100
(assert (forall ((x Int))
  (implies
    (>= x 100)
    (> (A x) 10))))

; A(3) = 190
(assert (= (A 3) 190))

; A(12) = 1200
(assert (= (A 12) 1200))

(check-sat)

几句话：

所有SMT功能都是合计的；如果要对部分函数进行编码，必须显式地对函数的域进行建模，并使定义公理以参数是否在域中为条件。不过，Z3仍将为您提供该功能的总体模型
在SMT中，由于没有求和理解运算符，所以任意求和编码是非常重要的。不过，您的情况更简单，因为您的总和覆盖静态已知数量的元素（0<；x<；100）
如果Z3py提供了一种方便的源代码语法，可以在静态已知的许多元素上生成和，我不会感到惊讶

网友

2楼 · 编辑于 2024-09-19 23:32:30

在z3py中可以有多种方法来编写这个示例。对于列出的约束，您可以使用符号数组、未解释的函数或为100个元素中的每个元素使用单独的变量

使用数组

这种情况下最简单的方法是使用数组：即将Int -> Int函数建模为数组：

from z3 import *

A = Array('A', IntSort(), IntSort())

s = Solver()

total = 0
for i in range(100):
    s.add(A[i] > 10)
    total = total + A[i]

s.add(total == 10000)

s.add(A[ 3] ==  190)
s.add(A[12] == 1200)

k = Int('k')
s.add(ForAll(k, (Implies(Or(k < 0, k >= 100),  A[k] == 0))))

if s.check() == sat:
    m = s.model()
    for i in range(100):
        v = m.evaluate(A[i]).as_long()
        print("%3d: %d" % (i, v))

运行时，此选项将打印：

您可以汇总打印的值，以确保它确实为您提供10000

使用未解释的函数

您还可以将A建模为未解释的函数。对上述内容而言，所需的更改实际上微不足道：

from z3 import *

A = Function('A', IntSort(), IntSort())

s = Solver()

total = 0
for i in range(100):
    s.add(A(i) > 10)
    total = total + A(i)

s.add(total == 10000)

s.add(A( 3) ==  190)
s.add(A(12) == 1200)

k = Int('k')
s.add(ForAll(k, (Implies(Or(k < 0, k >= 100),  A(k) == 0))))

if s.check() == sat:
    m = s.model()
    for i in range(100):
        v = m.evaluate(A(i)).as_long()
        print("%3d: %d" % (i, v))

这张照片是：

在这种情况下，模型非常不同，但很容易看到它有A(3) = 190、A(12) = 1200、A(74) = 7543，所有其他条目都设置为11；总共给你190 + 1200 + 7543 + 11 * 97 = 10000

使用独立变量

第三种方法是在python数组中分配100个整数元素，并分别对单个元素声明约束。这将导致最简单的模型，因为它不会使用任何量化。当然，这将模拟范围0..99之外的元素隐式为0的事实，因此仅当不需要显式提及此约束时才使用此选项。同样，编码几乎相同：

from z3 import *

A = [Int('A_%d' % i) for i in range(100)]

s = Solver()

total = 0
for i in range(100):
    s.add(A[i] > 10)
    total = total + A[i]

s.add(total == 10000)

s.add(A[ 3] ==  190)
s.add(A[12] == 1200)

if s.check() == sat:
    m = s.model()
    for i in range(100):
        v = m.evaluate(A[i]).as_long()
        print("%3d: %d" % (i, v))

为了简洁起见，我省略了这个输出。请注意，在本例中，我们如何使用A作为python列表，而不是z3py本身直接支持的符号数组

总结

最后，您描述的约束非常简单，可以使用这三种技术。哪一个是最好的取决于您想要建模的其他约束。（特别是，您希望避免大量使用量词，如上面的ForAll，因为SMT解算器通常不能很好地处理量词。这个问题足够简单，所以不会造成问题，但当约束变得复杂时，它会增加解算时间或导致解算器回答unknown。）

希望这能让你开始。祝你好运

使用数组

使用未解释的函数

使用独立变量

总结

相关问题更多 >

编程相关推荐

热门问题

热门文章