z3 实数存在论 [英] z3 existential theory of the reals

问题描述

Z3 是否决定非线性实数算术的存在片段?也就是说，我可以用它作为一个决策程序来测试一个带有 + 和 x 的无量词公式对实数有解吗?

Does Z3 decide the existential fragment of nonlinear real arithmetic? That is, can I use it as a decision procedure for testing whether a quantifier-free formula with + and x has a solution over the reals?

推荐答案

是的，Z3 有一个用于非线性多项式实数算法的存在片段的决策过程.当然，该程序是完整的模可用资源.该程序相当昂贵.本文描述了在 Z3 中实现的过程.

Yes, Z3 has a decision procedure for the existential fragment of nonlinear polynomial real arithmetic. Of course, the procedure is complete modulo available resources. The procedure is quite expensive. This article describes the procedure implemented in Z3.

这是一个小例子(也可以在线这里获得):

Here is a small example (also available online here):

(declare-const a Real)
(declare-const b Real)
(assert (= (^ a 5) (+ a 1)))
(assert (= (^ b 3) (+ (^ a 2) 1)))
(check-sat)
(get-model) 
(set-option :pp-decimal true) ;; force Z3 to display the result in decimal notation
(get-model)

这是一个相关的问题:

• Z3 支持非线性算术

这篇关于z3 实数存在论的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！