z3解决方案的数量

Question

如何使用z3来计算解决方案的数量？例如，我想证明对于任何n，方程组{x^2 == 1, y_1 == 1, ..., y_n == 1}有2个解。下面的代码显示了给定的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: finding all satisfying models

这里是你的榜样做这个（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