8

非常に単純な制約を想定しましょうsolve(x > 0 && x < 5)。

Z3（または他のSMTソルバー、または他の自動手法）xは、指定された制約を満たす（整数）変数の最小値と最大値を計算できますか？

この場合、最小値は1、最大値は4です。

4

3 に答える 3

11

Z3は、目的関数または変数の最適化（最大化/最小化）をサポートしていません。このような機能を追加する予定ですが、今年は追加されません。現在のバージョンでは、各反復で追加の制約を追加するいくつかの問題を解決することにより、目的関数を「最適化」できます。問題が満たされない場合に最適なものを見つけたことがわかっています。これは、アイデアを説明する小さなPythonスクリプトです。スクリプトは、変数の値を最大化しますX。最小化するには、に置き換える必要s.add(X > last_model[X])がありs.add(X < last_model[X])ます。このスクリプトは非常に単純で、「線形検索」を実行します。それは多くの方法で改善することができますが、それは基本的な考え方を示しています。

オンラインでスクリプトを試すこともできます：http：//rise4fun.com/Z3Py/KI1

次の関連する質問を参照してください。任意の命題式の変数の上限/下限を決定する

from z3 import *

# Given formula F, find the model the maximizes the value of X 
# using at-most M iterations.
def max(F, X, M):
    s = Solver()
    s.add(F)
    last_model  = None
    i = 0
    while True:
        r = s.check()
        if r == unsat:
            if last_model != None:
                return last_model
            else:
                return unsat
        if r == unknown:
            raise Z3Exception("failed")
        last_model = s.model()
        s.add(X > last_model[X])
        i = i + 1
        if (i > M):
            raise Z3Exception("maximum not found, maximum number of iterations was reached")

x, y = Ints('x y')
F = [x > 0, x < 10, x == 2*y]
print max(F, x, 10000)
于 2012-08-13T14:49:32.890 に答える
6

レオナルドが指摘したように、これは前に詳細に議論されました：任意の命題式の変数の上限/下限を決定します。参照：Z3でコードを最適化する方法は？（PI_NON_NESTED_ARITH_WEIGHT関連）。

要約すると、定量化された式を使用するか、繰り返し実行することができます。残念ながら、これらの手法は同等ではありません。

  • 定量化されたアプローチは反復を必要とせず、ソルバーへの1回の呼び出しでグローバルな最小/最大を見つけることができます。少なくとも理論的には。しかし、それはより難しい公式を生み出します。したがって、バックエンドソルバーはタイムアウトするか、単に「不明」を返す可能性があります。

  • 反復アプローチでは、バックエンドソルバーが処理する簡単な式が作成されますが、最適な値がない場合は永久ループになる可能性があります。Int最も単純な例は、最大の値を見つけようとすることです。定量化されたバージョンは、そのような値がないことをすばやく通知することでこの問題をうまく解決できますが、反復バージョンは無期限に続行されます。制約に最適なソリューションがあるかどうかを事前に知らない場合、これは問題になる可能性があります。（言うまでもなく、「十分な」反復回数は通常、推測が難しく、ソルバーで使用されるシードなどのランダムな要因に依存する可能性があります。）

また、手元にある問題ドメインのカスタム最適化アルゴリズムがある場合、汎用SMTソルバーがそれを上回る可能性は低いことにも注意してください。

于 2012-08-14T06:46:52.990 に答える
2

z3は最適化をサポートするようになりました。

from z3 import *

o = Optimize()
x = Int( 'x' )
o.add(And(x > 0, x < 5))
o.maximize(x)
print(o.check())  # prints sat
print(o.model())  # prints [x = 4]

この特定の問題は整数計画です。

于 2021-04-12T15:01:02.570 に答える