Search code examples
z3z3pyquantifierssatisfiability

What does a model mean in a universally quantified formula? Is it a function?

Consider these two formulae:

  • Exists y. Forall x. (y>x), which is unsat.
  • Forall x. Exists y. (y>x), which is sat.

Note that we cannot find “models” for the sat formula, e.g., using Z3 it outputs Z3Exception: model is not available for the following code:

phi = ForAll([x],Exists([y], lit))

s_def = Solver()
s_def.add(phi)
print(s_def.model())

Also, quantifier elimination does not output an elimination, but a satisfiability result [[]] (i.e., True):

x, y = Reals('x, y')

t = Tactic("qe")

lit = (y>x)

ae = Goal()
ae.add(ForAll([x],Exists([y], lit)))
ae_qe = t(ae)

print(ae_qe)

I think this happens because the value of y fully depends on x (e.g., if x is 5 then y can be 6). Thus, I have some questions:

  • Am I right with this interpretation?
  • What would be the meaning of “a model of a universally quantified formula”?
  • Do we say a formula accepts quantifier elimination even if it never eliminates the quantifier but "only: evaluate to True or False?
  • Is there a way to synthetise or construct a model/function that represents a y that holds the constraint (y>x); e.g. f(x)=x+1. In other words, does it make sense that the quantifier elimination of a Forall x. Exists y. Phi(x,y) like the example would be Forall x. Phi(x,f(x))?
Solution

  • You get a model-not-available, because you didn't call check. A model is only available after a call to check. Try this:

    from z3 import *

x, y = Ints('x y')

phi = ForAll([x], Exists([y], y > x))

s = Solver()
s.add(phi)
print(s.check())
print(s.model())

    This prints:

    sat
[]

    Now, you're correct that you won't get a meaningful/helpful model when you have a universal-quantifier; because the model will depend on the choice of x in each case. (You only get values for top-level existentials.) This is why the model is printed as the empty-list.

    Side Note In certain cases, you can use the skolemization trick (https://en.wikipedia.org/wiki/Skolem_normal_form) to get rid of the nested existential and get a mapping function, but this doesn't always work with SMT solvers as they can only build "finite" skolem functions. (For your example, there isn't such a finite function; i.e., a function that can be written as a case-analysis on the inputs, or an if-then-else chain.) For your specific questions:

    • Yes; value of y depends on x and thus cannot be displayed as is. Sometimes skolemization will let you work around this, but SMT solvers can only build finite skolem-functions.

    • Model of a universally quantified formula is more or less meaningless. It's true for all values of the universally quantified variables. Only top-level existentials are meaningful in a model.

    • Quantifier elimination did work here; it got rid of the whole formula. Note that QE preserves satisfiability; so it has done its job.

    • This is the skolem function. As you noted, this skolem function is not finite (can't be written as a chain of finite if-then-elses on concrete values), and thus existing SMT solvers cannot find/print them for you. If you try, you'll see that the solver simply loops:

    from z3 import *

x = Int('x')

skolem = Function('skolem', IntSort(), IntSort())
phi = ForAll([x], skolem(x) > x)

s = Solver()
s.add(phi)
print(s)
print(s.check())
print(s.model())

    The above never terminates, unfortunately. This sort of problem is simply too complicated for the push-button approach of SMT solving.