Z3 支持平方根

Question

我一直在搜索 z3 提供的平方根功能。例如，要添加关于实数 x 的约束，即 x*x = 2，最好的编码方式是什么？

我试过：

(declare-const x Real)
(assert (= 2 (* x x))) 
(check-sat)

结果未知。该模型也无法获得。

不过，我相信应该有办法满足这个要求。我指的是 smt-lib 2.0 语言的扩展版本，而不是 python api.

Answer 1

您需要使用非线性求解器。你的例子没有自动检测和使用它的原因是因为常量2：它被解析为一个整数而不是一个实数，所以它在技术上是整数和实数的组合理论，而非线性求解器可能只涉及实数，除非你强迫它。要强制使用它，您可以使用 check-sat-using 和非线性求解器 qfnra-nlsat (rise4fun link: http://rise4fun.com/Z3/fXDp ):

(declare-const x Real)

(push)
(assert (= 2 (* x x)))
(check-sat-using qfnra-nlsat) ; sat
(get-model)
; may have to play with printing options as this is irrational (or this may be a bug)
; (model 
;  (define-fun x () Real
;    (/ 5.0 4.0))
;)
(pop)

; the reason you need to use check-sat-using is because the 2 gets parsed into an integer; to force it to be a real, use a decimal:
(push)
(assert (= 2.0 (* x x)))

(check-sat) ; sat
(get-model) 
;(model 
;  (define-fun x () Real
;    (root-obj (+ (^ x 2) (- 2)) 1))
;)
(pop)

对于一般的指数（平方根等），可以用^求幂：

; you can also use ^ for exponentiation    
(push)
(assert (= 2.0 (^ x 2.0)))
(check-sat) ; sat
(get-model)
; (model 
;  (define-fun x () Real
;    (root-obj (+ (^ x 2) (- 2)) 1))
;)
(pop)

; to represent square root, etc., you may use fractional or decimal exponents
(push)
(assert (= 25.0 (^ x 0.5))) ; square root: 2 = sqrt(x)
(check-sat) ; sat
(get-model)
; maybe a bug or have to tune the model printer
;(model 
;  (define-fun x () Real
;    (- 1.0))
;)
(pop)

(push)
(assert (= 2.0 (^ x (/ 1.0 3.0))))
(check-sat) ; sat
(get-model)
;(model 
;  (define-fun x () Real
;    8.0)
;)
(pop)

(push)
(assert (= 10.0 (^ x 0.2)))
(check-sat) ; sat
(get-model)
;(model 
;  (define-fun x () Real
;    100000.0)
;)
(pop)

这是一个古老但相关的post：z3/python reals

一些打印问题，例如，如果您需要十进制近似值，可以使用以下方法解决：

(set-option :pp.decimal true)

Z3 支持平方根

Z3 support for square root

z3