z3 解的数量

Question

我该如何使用z3来计算解的数量呢？举个例子，我想证明对于任何一个n，方程组{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()

Answer 1

如果解决方案的数量是有限的，你可以通过列出所有不等于它们指定模型值的常量（也就是你的 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