z3解决方案的数量

Question

如何使用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()

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