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 使用固定精度。。

2. 在此答案中状态（强调是我的）

epsilon是指非标准数（无穷小）。您可以任意将其设置为小。同样，模型仅使用标准号码，因此它选择某些数字，在这种情况下为9。

给定..

• 我找不到任何选项来设置python API中的epsilon

• 通过更改x间隔的大小，返回模型中x的值与最佳值不同（例如Interval 0, 10给出x=9，而0, 1给出CC_7）

..我对上一句话的看法是， 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，可以控制公式的返回 model 中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)) )