2

我遇到了一个之前提到的问题，我并没有完全得到解决方案（将替代与简化相结合）。在我的编码中，我有严格的不等式，我需要将 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。）非常感谢！

4

1 回答 1

2

前提：

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

  2. 在这个答案NB 状态（重点是我的）

epsilon 指的是非标准数（无穷小）。您可以将其设置为任意小。同样，模型只使用标准数字，因此它选择了一些数字，在本例中为 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()

Whereinstantiate(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)) )
于 2016-06-21T13:26:46.257 回答