z3py: What is a correct way of asserting a constraint of "something does not exist"

Question

I want to assert a constraint of "something must not exist" in z3py. I tried using "Not(Exists(...))". A simple example is as follows. I want to find a assignment for a and b, so that such c does not exist.

from z3 import *

s = Solver()
a = Int('a')
b = Int('b')
c = Int('c')

s.add(a+b==5)
s.add(Not(Exists(c,And(c>0,c<5,a*b+c==10))))
print s.check()
print s.model()

The output is

sat
[b = 5, a = 0]

Which seems to be correct. But when I write "Not(Exists(...))" constraint in a more complex problem, it would take hours without generating a solution. I wonder if this is the correct and the most efficient way to assert "not exist" constraint? Or such problems with quantifiers are intrinsically hard to solve by any solver?

Answer 1

The way you wrote that constraint is just fine. And it is not surprising that Z3 (or any other solver) would have a hard time solving such problems as you have both quantifiers and non-linear arithmetic. Such problems are intrinsically hard to solve.

You might look into Z3's nlsat tactic, which might provide some relief here: How does Z3 handle non-linear integer arithmetic?

Or, you can try reals instead of integers, or bit-vectors (i.e., machine integers). Of course, whether you can actually use these types would depend on your problem domain. (Reals will have "fractional" values obviously, and bitvectors are subject to modular-arithmetic.)