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