z3 在实践中可以处理多少非线性？

Question

如果这个问题措辞不当，我深表歉意，但我正在尝试使用 z3（在带有语言绑定的 python 中）求解一些非线性方程，但不幸的是，qfnra-nlsat 和通用求解器都无法求解以下系统除非 a、b 和 c 都给出：

    y == 0.001 * (a ** 2.07) * (b ** 0.9) * (c ** 0.7) + 0.002 
    y > 0.0

我尝试了以下策略：

    t = z3.Then('simplify', 'qfnra-nlsat')

我还尝试用一些中间名称替换非线性部分，然后使用 push() 使用增量求解器将指数部分添加回来。但在这两种情况下，z3 基本上都会卡住（据我尝试超过 1 小时）。

我是 CSP 的新手和所涉及的理论背景，很抱歉，如果这是一个愚蠢的问题，但我想知道这种非线性是否超出了 z3 （经验上）可以解决的问题，或者我没有正确使用它？谢谢！

编辑：

这是在我的机器上失败的 python 代码：

    import z3
    a = z3.Real('a')
    b = z3.Real('b')
    c = z3.Real('c') 
    y = z3.Real('y')

    eq = [ 
        y == 0.001 * (a ** 2.07) * (b ** 0.9) * (c ** 0.7) + 0.002,
        y >= 0.0 
    ]

    t = z3.Then('simplify', 'qfnra-nlsat')
    s = t.solver()
    s.add(eq)
    r = s.check()
    print r
    m = s.model()
    print m

这是输出：

    unknown
    [y = 1/500 ]

编辑：

z3 git repo 的最新代码似乎有点坏了。我尝试了 4.4.1 版本，一切顺利。

不过，如果我在下面再添加一个约束条件，请提出一个后续问题：

    a == 16.0

z3 卡住了，我无法理解...似乎上面的附加约束非常微不足道，b 和 c 都是 1 的初始猜测应该可以解决系统问题，但我想这不是 z3 的工作方式?关于如何用这个新约束解决系统的任何想法？

Answer 1

假设我没有犯一些翻译错误，我在纯 SMT-LIB 界面中尝试了这个，它似乎工作正常。

如果您在查看此内容后仍有一些问题，请对您失败的整个示例进行编码，因为您可能有一些未包含的约束导致它失败。或者，重载的 Python 运算符（例如，**）可能没有被正确解释（尽管这似乎是正确的使用方式），因此您可能希望将 Z3 Python API 的函数用于各种表达式。

我包含了这个 x 变量，这是为了仔细检查我是否正确使用了 ^ 作为电源，它看起来是正确的（rise4fun 链接：http://rise4fun.com/Z3/plLQJ）：

(declare-const x Real)
(declare-const y Real)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)

; y == 0.001 * (a ** 2.07) * (b ** 0.9) * (c ** 0.7) + 0.002
(assert (= y (+ (* 0.001 (^ a 2.07) (^ b 0.9) (^ c 0.7)) 0.002)))
(assert (> y 0.0))

(check-sat-using qfnra-nlsat)
(get-model)

(assert (> x 1.0))
(assert (= x (^ 5.0 2.5))) ; check ^ means pow
(check-sat-using qfnra-nlsat)
(get-model)

这会产生：

sat
(model 
  (define-fun a () Real
    (- 1.0))
  (define-fun b () Real
    (- 1.0))
  (define-fun c () Real
    (- 1.0))
  (define-fun y () Real
    (+ (/ 1.0 500.0)
   (* (- (/ 69617318994479297159441705182250977318952641791835914067365099344218850343780027694073822279020999411953209540560859156221731465694293028234177768119402105034869871366755227547291324996387.0
            4000.0))
      (^ (/ 1.0 8.0) 207.0))))
)
sat
(model 
  (define-fun a () Real
    (- 1.0))
  (define-fun b () Real
    (- 1.0))
  (define-fun c () Real
    (- 1.0))
  (define-fun x () Real
    (root-obj (+ (^ x 2) (- 3125)) 2))
  (define-fun y () Real
    (+ (/ 1.0 500.0)
   (* (- (/ 69617318994479297159441705182250977318952641791835914067365099344218850343780027694073822279020999411953209540560859156221731465694293028234177768119402105034869871366755227547291324996387.0
            4000.0))
      (^ (/ 1.0 8.0) 207.0))))
)