2

以前に言及された問題があり、解決策がまったく得られません (代替と単純化の組み合わせ)。私のエンコーディングでは、厳密な不等式があり、イプシロンを 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. 固定精度で 1にp 近づくモデルが必要なだけだと思います。

  2. この回答では、 NBは述べています（強調は私のものです）

イプシロンは非標準数 (無限小) を表します。任意に小さく設定できます。繰り返しますが、モデルは標準的な数値のみを使用するため、この場合は 9 という数値が選択されます。

とすれば..

  • epsilonPython 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=NepsilonN=6epsilon10^-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 に答える