Complexity of finding a solution to SMT system with quantifier

Question

I need to find a solution to a problem by generating by using z3py. The formulas are generated depending on input of the user. During the generation of the formulas temporary SMT variables are created that can take on only a limited amount of values, eg is its an integer only even values are allowed. For this case let the temporary variables be a and b and their relation with global variables x and y are defined by the predicate P(a,b,x,y).

An example generated using SMT-LIB like syntax:

(set-info :status unknown)
(declare-fun y () Int)
(declare-fun x () Int)
(assert
(forall (
    (a Int) (b Int) (z Int) )
    (let 
      (($x22 (exists ((z Int))(and (< x z) (> z y)))))
      (=> 
          P(a, b, x, y) 
          $x22))))
(check-sat)

where

z is a variable of which all possible values must be considered
a and b represent variables who's allowed values are restricted by the predicate P
the variable 'x' and 'y' need to be computed for which the formula is satisfied.

Questions:

Does the predicate P reduce the time needed by z3 to find a solution?
Alternatively: viewing that z3 perform search over all possible values for z and a will the predicate P reduce the size of the search space?

Note: The question was updated after remarks from Levent Erkok.

alias alias · Accepted Answer · 2019-01-11T17:09:19

The SMTLib example you gave (generated or hand-written) doesn't make much sense to me. You have universal quantification over x and z, and inside of that you existentially quantify z again, and the whole formula seems meaningless. But perhaps that's not your point and this is just a toy. So, I'll simply ignore that.

Typically, "redundant equations" (as you put it), should not impact performance. (By redundant, I assume you mean things that are derivable from other facts you presented?) Aside: a=z in your above formula is not redundant at all.

This should be true as long as you remain in the decidable subset of the logics; which typically means linear and quantifier-free.

The issue here is that you have quantifier and in particular you have nested quantifiers. SMT-solvers do not deal well with them. (Search stack-overflow for many questions regarding quantifiers and z3.) So, if you have performance issues, the best strategy is to see if you really need them. Just by looking at the example you posted, it is impossible to tell as it doesn't seem to be stating a legitimate fact. So, see if you can express your property without quantifiers.

If you have to have quantifiers, then you are at the mercy of the e-matcher and the heuristics, and all bets are off. I've seen wild performance characteristics in that case. And if reasoning with quantifiers is your goal, then I'd argue that SMT solvers are just not the right tool for you, and you should instead use theorem provers like HOL/Isabelle/Coq etc., that have built-in support for quantifiers and higher-order logic.

If you were to post an actual example of what you're trying to have z3 prove for you, we might be able to see if there's another way to formulate it that might make it easier for z3 to handle. Without a specific goal and an example, it's impossible to opine any further on performance.

Complexity of finding a solution to SMT system with quantifier

1 Answers