5

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()
Alex Reece
  • 1,906
  • 22
  • 31

1 Answers1

7

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.

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

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

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
Community
  • 1
  • 1
Taylor T. Johnson
  • 2,834
  • 16
  • 17
  • Wow, this was a great response. Unfortunately, I can't quite use the first part: I'm getting the number solutions outside of the solver so I can't prove things like "the number of solutions <= f(n)". I'm going to play around with the second thing though (the function seems to be a good way to prove something about equations that are a function of n), but I still don't see how that gives me access to the number of solutions. Is there a way to express "the domain of this function is < f(n)"? – Alex Reece Mar 06 '13 at 23:54
  • I'm starting to develop the impression that this just can't be done in z3 :-/ – Alex Reece Mar 07 '13 at 15:28
  • Could you please provide an example of what you'd like to solve? You can use the first part of my answer to find the number of solutions for a particular n. You can then use the second part to show there are no other solutions for any choice of n. In your original example, the number of solutions is independent of n. Do you have a specific example you're interested in where this is not the case? I didn't understand the domain of function < f(n): in the example, I restrict the domain n >= 1. If you'd rather 1 <= n <= C for some C, you can add that in the antecedent of the implication. – Taylor T. Johnson Mar 07 '13 at 17:05
  • Sure thing. I want to prove a statement equivalent to: "In the real field, for any `n`, for any `t_1, ... t_n`, there are at most `2^n` solutions to the set of equations { `x_1^2 == t_1`, `x_2^2==t_2`, ... , `x_n^2==t_n` }." – Alex Reece Mar 08 '13 at 01:00