CODEWITHSUNDEEP
z3smtz3py
Xiao Xiao
Xiao Xiao

Reputation: 1

How to let z3 python existential proposition simplified to True/False?

I would like the z3 solver to determine if an added vector (b) is in the span of a list (a) of vectors or not. I don't want to enforce it to be True or not but just want to to be stored as a True or False.

I used the existential proposition Exists() and here are some examples:

import numpy as np
from z3 import *
solver = Solver()
a=np.array([[0,1,1],[0,0,1]])
b=np.array([1,1,1])
Coefficient=[Int('c_%s' %i) for i in range(2)]
linear_combination = np.dot(Coefficient,a)
answer = Bool('answer')
solver.add(answer == Exists(Coefficient,And([linear_combination[i]==b[i] for i in range(len(b))])))
solver.check()
solver.model().evaluate(answer)

ouput: Out[4]: False

However, for some list and added vector, the result is still in the Exists() format without being reduced to True/False:

import numpy as np
from z3 import *
solver = Solver()
a=np.array([[1,1,1],[1,1,1]])
b=np.array([1,1,1])
Coefficient=[Int('c_%s' %i) for i in range(2)]
linear_combination = np.dot(Coefficient,a)
answer = Bool('answer')
solver.add(answer == Exists(Coefficient,And([linear_combination[i]==b[i] for i in range(len(b))])))
solver.check()
solver.model().evaluate(answer)

output:

Out[6]: Exists([c_0, c_1], c_0 + c_1 == 1)

Is there a way to always let it output True/False, which should be doable since the condition statement involves only the coefficients?

Upvotes: 0

Views: 88

Answers (1)

alias
alias

Reputation: 30418

I'm not sure how you're even getting any results with your program. When I run it, I get:

z3.z3types.Z3Exception: Python value cannot be used as a Z3 integer

And this makes perfect sense: You cannot mix/match numpy/Python data-structures with z3 at will. These live in their own worlds, and any interaction between them has to be carefully programmed. (And may not always be possible.)

There are three main points regarding your problem:

  1. Do not mix numpy/Python/z3 values arbitrarily. In fact, avoid numpy completely if you can, since the more complicated routines of numpy you use, the less likely it'll be supported by z3.

  2. A linear combination can have real-coefficients on vectors, so make sure to use reals on the coefficients.

  3. z3 will only provide values of top-level variables. An Exist at the outermost layer is equivalent to a top-level variable; so pull them up. (There are good reasons why z3 won't give you values for explicitly quantified variables, as it would be impossible to uniquely refer to them. But that's a tangential discussion.)

Based on this, I'd code your problem as follows:

from z3 import *

def isLinearComb(vs, v):
    slv  = Solver()
    cs   = [Real('c_%s' % i) for i in range(len(vs))]

    sums = [sum(es) for es in zip(*[[c * e for e in v] for (c, v) in zip(cs, vs)])]

    for (e, s) in zip(v, sums):
        slv.add(e == s)

    if slv.check() == unsat:
        print("Not a linear combination.")
    else:
        m = slv.model()
        for c in cs:
            print(c, "=", m[c])

With this, you can try:

>>> isLinearComb([[0,1,1], [0,0,1]], [1,1,1])
Not a linear combination.
>>> isLinearComb([[1,1,1], [1,1,1]], [1,1,1])
c_0 = 0
c_1 = 1
>>> isLinearComb([[0,1,1], [0,0,1], [1,1,1]], [2,3.5,9])
c_0 = 3/2
c_1 = 11/2
c_2 = 2

Upvotes: 0

Related Questions