z3 解数

如何使用 z3 来计算解的数量？例如，我想证明对于任何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()

如果解的数量有限，您可以使用不等于指定模型值的常量（您的 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