5

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()
4

1 に答える 1

7

解の数が有限である場合は、割り当てられたモデル値と等しくない定数（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
于 2013-03-06T20:47:42.107 に答える