5

如何使用 z3 计算解决方案的数量？例如，我想证明对于 any n，方程组有 2 个解{x^2 == 1, y_1 == 1, ..., y_n == 1}。以下代码显示了给定的可满足性n，这不是我想要的（我想要任意的解决方案数量n）。

#!/usr/bin/env python

from z3 import *

# Add the equations { x_1^2 == 1, x_2 == 1, ... x_n == 1 } to s and return it.
def add_constraints(s, n):
    assert n > 1
    X = IntVector('x', n)
    s.add(X[0]*X[0] == 1)
    for i in xrange(1, n):
        s.add(X[i] == 1)
    return s

s = Solver()
add_constraints(s, 3)
s.check()
s.model()
4

1 回答 1

7

如果有有限数量的解决方案，您可以使用不等于其分配的模型值的常量（您的 x_i）的析取来枚举所有这些。如果有无限的解决方案（如果你想证明所有自然数 n 的情况就是这种情况），你可以使用相同的技术，但当然不能枚举它们，但可以使用它来生成许多解决方案一些绑定你选择。如果要对所有 n > 1 证明这一点，则需要使用量词。我在下面添加了对此的讨论。

虽然您没有完全提出这个问题，但您也应该看到这个问题/答案：Z3：找到所有令人满意的模型

这是您执行此操作的示例（此处的 z3py 链接：http ://rise4fun.com/Z3Py/643M ）：

    # Add the equations { x_1^2 == 1, x_2 == 1, ... x_n == 1 } to s and return it.
def add_constraints(s, n, model):
    assert n > 1
    X = IntVector('x', n)
    s.add(X[0]*X[0] == 1)
    for i in xrange(1, n):
        s.add(X[i] == 1)

    notAgain = []
    i = 0
    for val in model:
      notAgain.append(X[i] != model[val])
      i = i + 1
    if len(notAgain) > 0:
      s.add(Or(notAgain))
      print Or(notAgain)
    return s

for n in range(2,5):
  s = Solver()
  i = 0
  add_constraints(s, n, [])
  while s.check() == sat:
    print s.model()
    i = i + 1
    add_constraints(s, n, s.model())
  print i # solutions

如果你想证明对于 n 的任何选择都没有其他解决方案，你需要使用量词，因为前面的方法只适用于有限的 n（并且它很快变得非常昂贵）。这是显示此证明的编码。您可以对此进行概括，以结合上一部分中的模型生成功能，以提出更通用的公式的 +/- 1 解决方案。如果方程有多个独立于 n 的解（如您的示例中），这将允许您证明方程具有一些有限数量的解。如果解决方案的数量是 n 的函数，则您必须弄清楚该函数。z3py 链接：http ://rise4fun.com/Z3Py/W9En

x = Function('x', IntSort(), IntSort())
s = Solver()
n = Int('n')
# theorem says that x(1)^2 == 1 and that x(1) != +/- 1, and forall n >= 2, x(n) == 1
# try removing the x(1) != +/- constraints
theorem = ForAll([n], And(Implies(n == 1, And(x(n) * x(n) == 1, x(n) != 1, x(n) != -1) ), Implies(n > 1, x(n) == 1)))
#s.add(Not(theorem))
s.add(theorem)
print s.check()
#print s.model() # unsat, no model available, no other solutions
于 2013-03-06T20:47:42.107 回答