Z3 Оптимизация, строгие неравенства

Предпосылка:

1. Я предполагаю, что вам просто нужна модель, в которой p приближается к 1 с фиксированной точностью.

2. В этом ответе N.B. состояния (выделено мной)

эпсилон относится к нестандартному числу (бесконечно малому). Вы можете установить его произвольно маленьким. Опять же, модель использует только стандартные числа, поэтому она выбирает некоторое число, в данном случае 9.

При условии..

• Я не смог найти ни одного параметра для установки epsilon ни в Python API, ни среди параметров smt2

• Изменяя размер интервала x, значение x в возвращенной модели находится на другом расстоянии от оптимального значения (например, интервал 0, 10 дает x=9, тогда как 0, 1 дает x=0.5)

..мой взгляд на предыдущую цитату заключается в том, что z3 выбирает какое-то случайное удовлетворяющее значение, вот и все.

Поэтому:

Я бы сделал это следующим образом:

from z3 import *

epsilon = 0.0000001

p = Real('p')
q = Real('q')
s = Optimize()

s.add(p > 0, p < 1)
s.add(q > 0, q < 1)

s.push()
h = s.maximize(p)

print s.check() # Here I assume SAT

opt_value = h.value()

if epsilon in opt_value: # TODO: refine
    s.pop()
    opt_term = instantiate(opt_value, epsilon) # TODO: encode this function

    s.add(p > opt_value)

    s.check()

    print s.model()
else:
    print s.model()
    s.pop()

Где instantiate(str, eps) – это специальная функция, которая анализирует строки в форме ToReal(1) + ToReal(-1)*epsilon и возвращает результат очевидной интерпретации такой строки.

----

Я хотел бы упомянуть, что альтернативный подход состоит в том, чтобы закодировать проблему как формулу smt2 и передать ее в качестве входных данных для OptiMathSAT:

(set-option:produce-models true)

(declare-fun p () Real)
(declare-fun q () Real)

(assert (and (< 0 p) (< p 1)))
(assert (and (< 0 q) (< q 1)))

(maximize p)

(check-sat)
(set-model 0)
(get-model)

OptiMathSAT имеет параметр командной строки -optimization.theory.la.epsilon=N для управления значением epsilon в возвращаемой модели формулы. По умолчанию N=6 и epsilon равно 10^-6. Вот результат:

### MAXIMIZATION STATS ###
# objective:      p (index: 0)
# interval:     [ -INF , +INF ]
#
# Search terminated!
# Exact strict optimum found!
# Optimum: <1
# Search steps: 1 (sat: 1)
#  - binary: 0 (sat: 0)
#  - linear: 1 (sat: 1)
# Restarts: 1 [session: 1]
# Decisions: 3 (0 random) [session: 3 (0 random)]
# Propagations: 6 (0 theory) [session: 13 (0 theory)]
# Watched clauses visited: 1 (0 binary) [session: 2 (1 binary)]
# Conflicts: 3 (3 theory) [session: 3 (3 theory)]
# Error:
#  - absolute: 0
#  - relative: 0
# Total time: 0.000 s
#  - first solution: 0.000 s
#  - optimization: 0.000 s
#  - certification: 0.000 s
# Memory used: 8.977 MB
sat
( (p (/ 1999999 2000000))
  (q (/ 1 2000000)) )