使用 Z3 和 SMT-LIB 定义带实数的 sqrt 函数

Question

如何以 smt-libv2 格式编写 sqrt 函数。

注意： 为了获得最多两个值，我在这里找到了一个有用的链接：Use Z3 and SMT-LIB to get a maximum of two values。

Answer 1

假设您的公式没有量词，那么您可以通过引入新变量和添加约束来隐式定义平方根。 例如你可以写：

  (define-fun is_sqrt ((x Real) (y Real)) Bool (= y (* x x)))

那么'x'是'y'的平方根；如果你只想要非负平方根，那么：

  (define-fun is_sqrt ((x Real) (y Real)) Bool (and (>= x 0) (= y (* x x))))

对于您的断言中出现平方根的每个事件，引入一个新变量并将新变量插入该位置。然后添加断言

   (assert (is_sqrt fresh-variable sub-term))

Z3 还提供了一个内置运算符，用于将术语提升为幂。 您可以使用它来获得平方根。所以要写出'x'的平方根， 你可以写这个词：

   (^ x 0.5)

在 Z3 中使用幂的推理是有限的，所以这真的取决于你的公式所说的这个公式是否会以与关系编码相同的方式处理。

Answer 2

如果您实际上不需要函数，那么将 y 定义为 x 的平方根的最简单方法是断言 y * y = x，即：

; This will cause Z3 to return a decimal answer instead of a root-obj
(set-option :pp.decimal true)

; Option 1: inverse of multiplication. This works fine if you don't actually
; need to define a custom function. This will find y = 1.414... or y = -1.414...
(declare-fun y () Real)
(assert (= 2.0 (* y y)))

; Do this if you want to find the positive root y = 1.414...
(assert (>= y 0.0))

(check-sat)
(get-value (y))
(reset)

我尝试使用未解释函数的另一种方法是这样的：

; Option 2: uninterpreted functions. Unfortunately Z3 seems to always return
; 'unknown' when sqrt is defined this way. Here we ignore the possibility that
; x < 0.0; fixing this doesn't help the situation, though.
(declare-fun sqrt (Real) Real)
(assert (forall ((x Real)) (= x (* (sqrt x) (sqrt x)))))
(declare-fun y () Real)
(assert (= y (sqrt 2.0)))
(check-sat)
(reset)

最后，到目前为止，如果您使用的是 Z3，最简单的方法是使用 Nikolaj 建议的内置幂运算符。你可以基于这个想法创建一个函数：

; Option 3: built-in power operator. This is not standard SMT-LIB, but works
; well with Z3.
(define-fun sqrt ((x Real)) Real (^ x 0.5))
(declare-fun y () Real)
(assert (= y (sqrt 2.0)))
(check-sat)
(get-value (y))
(reset)

Nikolaj 定义函数is_sqrt 的想法也是一个有趣的想法，并且它的优点是无需量词，因此可以与 nlsat（Z3 中最强大的非线性求解器）一起使用。