真实理论中 z3 中的“根对象”是什么？

Question

我在 z3 中尝试了 QF_NRA，它给了我一个关于 root-obj 的抽象值。

(set-logic QF_NRA)
(declare-const x Real)
(assert (= 2 (* x x)))
(check-sat)
sat
(get-model)
(
  (define-fun x () Real
    (root-obj (+ (^ x 2) (- 2)) 1))
)

我不太明白它的意思。

此外，x 似乎是在递归中定义的，而不是由 define-fun-rec 定义的。

谢谢。

Answer 1

代数实数

Z3 的真实理论支持所谓的algebraic reals。也就是说，它可以用具有有理（等效地，整数）值系数的多项式的根来表示解。请注意，这样的多项式可以有复数根。 Z3 仅支持实数根，即虚部为 0 的根。代数实数本质上是具有整数系数的单变量多项式的实数根。

处理root-obj的

在您发布的示例中，您要求 z3 为 x*x == 2 找到一个令人满意的模型。它告诉你解决方案是多项式的“零”(+ (^ x 2) (- 2))，或者用更熟悉的符号P(x) = x^2 -2 编写。你得到的索引是1（root-obj 的第二个参数），它表示它是这个多项式的“第一个”实根。如果你要求 z3 给你另一个解决方案，它会给你下一个：

(set-logic QF_NRA)
(declare-const x Real)
(assert (= 2 (* x x)))
(assert (distinct x (root-obj (+ (^ x 2) (- 2)) 1)))
(check-sat)
(get-model)

打印出来：

sat
(
  (define-fun x () Real
    (root-obj (+ (^ x 2) (- 2)) 2))
)

如您所见，“下一个”解决方案是第二个根。如果我们断言我们想要另一个解决方案怎么办？

(set-logic QF_NRA)
(declare-const x Real)
(assert (= 2 (* x x)))
(assert (distinct x (root-obj (+ (^ x 2) (- 2)) 1)))
(assert (distinct x (root-obj (+ (^ x 2) (- 2)) 2)))
(check-sat)

打印出来：

unsat

正如预期的那样。

请注意，代数实数不包括 pi、e 等数字，即它们不包括超越数。只有那些可以表示为具有整数系数的多项式的根的实数。 Leonardo 2012 年的paper 对此进行了详细解释。

获得近似值

z3 还允许您以任意精度获得此类 root-obj 解决方案的近似值。为此，请使用咒语：

(set-option :pp.decimal true)
(set-option :pp.decimal_precision 20)

第二行中的20 是您想要的精度位数，您可以根据需要进行更改。如果将这两行添加到原始脚本中，z3 将响应：

sat
(
  (define-fun x () Real
    (- 1.4142135623730950?))
)

注意号码末尾的?。这是 z3 告诉您它打印的数字是该值的“近似值”的方式，即它不是精确的结果。

关于“递归”的说明

您的问题表明x 可能是递归定义的。事实并非如此。碰巧您选择的变量名是x，z3 也总是使用字母x 作为多项式。如果您选择y 作为变量，您仍然会得到完全相同的答案；多项式的参数与程序中的变量无关。