python - Z3 优化，严格的不等式

Question

我遇到了一个之前提到的问题，我没有完全得到解决方案(将替代与简化相结合)。在我的编码中，我有严格的不等式，我需要将 epsilon 设置为 0 或一个非常小的值。例如，我有以下简化的 Python 代码:

from z3 import *

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

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

print s.check()
print s.upper(h)
print s.model()

如何让 p 被赋予最大值 1？ (现在它被分配了 1/2。)非常感谢!

Answer 1

前提:

1. 我假设您只是想要一个模型，其中p以固定精度接近 1。

2. 在this answer注意状态(重点是我的)

epsilon refers to a non-standard number (infinitesimal). You can set it arbitrarily small. Again the model uses only standard numbers, so it picks some number, in this case 9.

鉴于..

• 我在 Python API 和 smt2 选项中都找不到设置 epsilon 的选项

• 通过改变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)) )