z3 解数 [英] z3 number of solutions

问题描述

如何使用 z3 计算解的数量?例如，我想证明对于任何 n，方程组有 2 个解 {x^2 == 1, y_1 == 1, ..., y_n == 1}.以下代码显示了给定 n 的可满足性，这不是我想要的(我想要任意 n 的解决方案的数量).

How do I use z3 to count the number of solutions? For example, I want to prove that for any n, there are 2 solutions to the set of equations {x^2 == 1, y_1 == 1, ..., y_n == 1}. The following code shows satisfiability for a given n, which isn't quite what I want (I want number of solutions for an arbitrary 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()

推荐答案

如果有有限数量的解决方案，您可以使用不等于其指定模型值的常量(您的 x_i 的)的析取来枚举所有这些.如果有无限解(如果你想为所有自然数 n 证明这一点就是这种情况)，你可以使用相同的技术，但当然不能枚举它们，但可以使用它来生成许多解一些绑定你选择.如果要对所有 n > 1 证明这一点，则需要使用量词.我在下面添加了对此的讨论.

If there are a finite number of solutions, you can use the disjunct of the constants (your x_i's) not equal to their assigned model values to enumerate all of them. If there are infinite solutions (which is the case if you want to prove this for all natural numbers n), you can use the same technique, but of course couldn't enumerate them all, but could use this to generate many solutions up to some bound you pick. If you want to prove this for all n > 1, you will need to use quantifiers. I've added a discussion of this below.

虽然你没有问这个问题，但你也应该看到这个问题/答案:Z3:找到所有满意的模型

While you didn't quite ask this question, you should see this question/answer as well: Z3: finding all satisfying models

这是您执行此操作的示例(z3py 链接在此:http://rise4fun.com/Z3Py/643M ):

Here's your example doing this (z3py link here: 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

If you want to prove there are no other solutions for any choice of n, you need to use quantifiers, since the previous approach will only work for finite n (and it gets very expensive quickly). Here is an encoding showing this proof. You could generalize this to incorporate the model generation capability in the previous part to come up with the +/- 1 solution for a more general formula. If the equation has a number of solutions independent of n (like in your example), this would allow you to prove equations have some finite number of solutions. If the number of solutions is a function of n, you'd have to figure that function out. z3py link: 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

这篇关于z3 解数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！