Насколько нелинейность может обрабатываться z3 на практике?

Question

Приносим извинения, если этот вопрос плохо сформулирован, но я пытаюсь использовать z3 (в python с привязкой языка) для решения некоторых нелинейных уравнений, но, к сожалению, ни qfnra-nlsat, ни общий решатель не могут решить следующую систему, если только а, б и все дано:

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 в основном застревает (дольше, чем я пытался), в обоих случаях.

Я новичок в CSP и теоретический фон, извините, если это глупый вопрос, но мне интересно, не существует ли такая нелинейность вне (эмпирически) разрешима z3 или я не использую ее правильно? Благодаря!

Edit:

Вот питон код, который не работает на моей машине:

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 ] 

Edit:

Казалось что последний код из z3 git repo некорректно нарушен. Я пробовал с выпуском 4.4.1, и все получилось.

Следить за вопрос, хотя, если я просто добавить еще одно ограничение ниже:

a == 16.0 

и Z3 застревает, который я не мог понять ... Кажется, что дополнительное ограничение выше довольно тривиально, первоначальное предположение о том, что b и c являются как 1s, должны решить систему, но я думаю, что это не так, как работает z3? Любая идея о том, как решить систему с помощью этого нового ограничения?

Answer 1

Предполагая, что я не совершил ошибку перевода, я пробовал это в чистом интерфейсе SMT-LIB и, похоже, работал нормально.

Если у вас все еще есть проблемы после просмотра, пожалуйста, закодируйте весь ваш пример, который терпит неудачу, поскольку, возможно, у вас есть некоторые ограничения, которые вы не включили, что приводит к сбою. Или, возможно, перегруженные операторы Python (например, **) не интерпретируются должным образом (хотя, похоже, это правильное использование для питания), поэтому вы можете использовать функции API Z3 Python для различных выражений.

Я включил эту 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)))) 
)