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. 在这个答案，注:各州，(强调是我的)

epsilon是指一个非标准数(无限小).你可以把它设得很小。同样，模型只使用标准数字，因此它选择一些数字，在本例中是9。

既然如此..。

• 我找不到在Python或smt2选项中设置smt2的任何选项。
• 通过改变x区间的大小，返回模型中的x值与最优值的距离不同(例如，区间0, 10给出x=9，而0, 1给出x=0.5)。

..my引用了前面的话，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)) )