Z3 支持指数

Question

我是 Z3 的新手，我试图了解它是如何工作的，以及它可以做什么和不能做什么。我知道 Z3 至少通过幂 (^) 运算符对指数有一些支持(请参阅 Z3py returns unknown for equation using pow() function 、 How to represent logarithmic formula in z3py 和 Use Z3 and SMT-LIB to define sqrt function with a real number )。我不清楚的是这种支持有多广泛，以及 z3 可以对指数做出什么样的推断。

这是一个简单的例子，涉及 z3 可以分析的指数。我们定义一个指数函数，然后要求它验证 exp(0) == 1:

(define-fun exp ((x Real)) Real
  (^ 2.718281828459045 x))
(declare-fun x1 () Real)
(declare-fun y1 () Real)
(assert (= y1 (exp x1)))
(assert (not (=> (= x1 0.0) (= y1 1.0))))
(check-sat)
(exit)

正如预期的那样，Z3 返回 unsat。另一方面，这是一个 Z3 无法分析的简单示例:

(define-fun exp ((x Real)) Real
  (^ 2.718281828459045 x))
(declare-fun x1 () Real)
(declare-fun y1 () Real)
(assert (= y1 (exp x1)))
(assert (not (< y1 0.0)))
(check-sat)
(exit)

这应该是可满足的，因为实际上 x1 的任何值都会使 y1 > 0。但是，Z3 返回未知。鉴于 Z3 可以分析第一个示例，我可能天真地期望 Z3 能够对此进行分析。

我意识到这个问题有点宽泛，但是:谁能让我深入了解 Z3 如何处理指数，以及(更具体地说)为什么它可以解决我给出的第一个例子而不是第二个例子？

Answer 1

一般很难说，因为非线性求解具有挑战性，但是您提出的案例实际上并不那么神秘。你写了:

(assert (= y (exp x)))
(assert (not (=> (= x 0) (= y 1))))

Z3 将简化第二个断言，产生:

(assert (= y (exp x)))
(assert (= x 0))
(assert (not (= y 1)))

然后它将传播第一个相等，产生:

(assert (= y (exp 0)))
(assert (not (= y 1)))

现在当 exp被扩展，您有一个常量^常量的情况，Z3 可以处理(对于整数指数等)。

对于第二种情况，您是在问一个关于变量指数的非常基本的问题，而 Z3 立即发出警告。这并不太奇怪，因为关于变量指数的许多问题要么是已知的不可计算的，要么是未知的但很难。