z3py:声明 "something does not exist" 约束的正确方法是什么

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

我想在 z3py 中声明 "something must not exist" 的约束。我尝试使用 "Not(Exists(...))"。一个简单的例子如下。我想给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(...))" 约束时,需要几个小时才能生成解决方案。 我想知道这是否是断言 "not exist" 约束的正确且最有效的方法?或者这种量词问题本质上很难被任何求解器解决?

你写约束的方式很好。毫不奇怪,Z3(或任何其他求解器)很难解决此类问题,因为您同时拥有量词和非线性算术。这样的问题本质上是很难解决的。

您可能会研究 Z3 的 nlsat 策略,这可能会在此处提供一些缓解:How does Z3 handle non-linear integer arithmetic?

或者,您可以尝试使用 reals 而不是整数或位向量(即机器整数)。当然,您是否可以实际使用这些类型取决于您的问题领域。 (显然,实数将具有 "fractional" 值,而位向量则受制于模运算。)