具有未解释函数乘积的方程在 Z3 中是否不可解

Question

代码如下

(declare-fun f (Int) Real)
(declare-fun g (Int) Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-model)

returns "unknown"，尽管有一个明显的解决方案。消除 f 和 g 的参数（有效地使它们成为常量？）导致 "sat" 具有预期的分配。我想，我的问题是：具有未解释函数的算术有什么特别之处？

顺便说一句，用 + 替换 * 也会导致 "sat"，所以问题不在于未解释的函数本身，而在于它们如何组合。

补充想法

使域（非常）有限无济于事，例如，

(declare-fun f (Bool) Real)
(declare-fun g (Bool) Real)
(declare-const x Bool)
(declare-const y Bool)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-model)

returns"unknown"。这很奇怪，因为 f:Bool->Real 本质上只是两个变量 f(False) 和 f(True)（当然，求解器必须识别这一点）。

无法处理实值未解释函数的非线性算术是一个非常严重的限制，因为数组是作为未解释函数实现的。所以，例如，

(declare-const a (Array Int Real))
(assert (= (* (select a 1) (select a 1)) 1))
(check-sat)
(get-model)

returns"unknown"。换句话说，涉及乘法的实数数组元素上的任何非线性代数表达式都是无解的：'(

Answer 1

是乘法引入的非线性导致问题难以解决，而不是未解释的函数。事实上，您可以使用 get-info 命令询问求解器原因：

(set-logic QF_UFNIRA)
(declare-fun f (Int) Real)
(declare-fun g (Int) Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-info :reason-unknown)

以下是我从各种求解器那里得到的一些回复：

Z3:

(:reason-unknown smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic)))

CVC4:

(:reason-unknown incomplete)

MathSAT：

(error "sat, but with non-linear terms")

因此，随着求解器本身的改进并开始处理更多非线性算法，您最终可能会得到模型。但是，一般来说，非线性问题总是有问题的，因为当涉及整数时它们是不可判定的。（因为您可以使用非线性项对丢番图方程进行编码。）

有关 2012 年的相关讨论，另请参阅 How does Z3 handle non-linear integer arithmetic?。

删除未解释的函数

即使你摆脱了未解释的功能，你仍然在 unknown 土地，只要你混合 Int 和 Real 类型和非线性条款：

(set-logic QF_NIRA)
(declare-const f Real)
(declare-const g Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (+ (* f g) (to_real (+ x y))) 1.0))
(check-sat)
(get-info :reason-unknown)

Z3 说：

(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))")

因此，混合类型和非线性项会出现问题。

具有未解释函数乘积的方程在 Z3 中是否不可解

Are equations with products of uninterpreted functions unsolvable in Z3

z3

删除未解释的函数