z3py：断言"something does not exist"约束的正确方法是什么

Question

我想在z3py中断言"某些东西必须不存在"的约束。我尝试使用"不(存在(…))"。下面是一个简单的例子。我想为a和b找到一个赋值，使得这样的c不存在。

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()

输出为

sat
[b = 5, a = 0]

这似乎是正确的。但是，当我在一个更复杂的问题中编写"Not(Exists(…))"约束时，可能需要几个小时才能生成解决方案。我想知道这是否是断言"不存在"约束的正确和最有效的方法?或者这样的量词问题本质上很难被任何求解器解决?

Answer 1

您写约束的方式很好。这并不奇怪，Z3(或任何其他求解器)将很难解决这样的问题，因为你有量词和非线性算法。这些问题本质上是难以解决的。

你可以看看Z3的nlsat策略，这可能会让你松一口气:Z3是如何处理非线性整数运算的?

或者，您可以尝试使用real s代替整数或位向量(即机器整数)。当然，是否可以实际使用这些类型取决于您的问题域。(实数显然会有"小数"值，而位向量受制于模运算。)