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

Question

我想在 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" 约束的正确且最有效的方法？或者这种量词问题本质上很难被任何求解器解决？

Answer 1

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

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

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

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

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

z3

exists

smt

z3py

quantifiers