5

任意の命題式 PHI (いくつかの変数に対する線形制約) が与えられた場合、各変数の (近似) 上限と下限を決定する最良の方法は何ですか?

一部の変数は制限されていない場合があります。この場合、アルゴリズムは、これらの変数に上限/下限がないと結論付ける必要があります。

例えば、PHI = (x=3 AND y>=1)。x の上限と下限は両方とも 3 です。y の下限は 1 で、y には上限がありません。

これは非常に単純な例ですが、一般的な解決策はありますか (おそらく SMT ソルバーを使用)?

4

2 に答える 2

3

これは、各変数の SAT/UNSAT ドメインが連続していることを前提としています。

  1. SMT ソルバーを使用して、式の解を確認します。解決策がない場合は、上限/下限がないことを意味するため、停止します。
  2. 式の変数ごとに、変数のドメインに対して 2 つのバイナリ検索を実行します。1 つは下限を検索し、もう 1 つは上限を検索します。各変数の検索の開始値は、ステップ 1 で見つかった解の変数の値です。SMT ソルバーを使用して、各検索値の充足可能性を調べ、各変数の境界を体系的に囲みます。

整数ドメイン変数を想定した検索関数の擬似コード:

lower_bound(variable, start, formula)
{
    lo = -inf;
    hi = start;
    last_sat = start;
    incr = 1;
    do {
        variable = (lo + hi) / 2;
        if (SMT(formula) == UNSAT) {
            lo = variable + incr;
        } else {
            last_sat = variable;
            hi = variable - incr;
        }
    } while (lo <= hi);
    return last_sat;
}

と

upper_bound(variable, start, formula)
{
    lo = start;
    hi = +inf;
    last_sat = start;
    do {
        variable = (lo + hi) / 2;
        if (SMT(formula) == SAT) {
            last_sat = variable;
            lo = variable + incr;
        } else {
            hi = variable - incr;
        }
    } while (lo <= hi);
    return last_sat;
}

-inf/+inf は、各変数のドメインで表現可能な最小値/最大値です。lower_bound が -inf を返す場合、変数には下限がありません。upper_bound が +inf を返す場合、変数には上限がありません。

于 2012-01-26T02:24:00.953 に答える
2

実際には、このような最適化問題のほとんどは、SMT ソルバーに加えて、最大/最小の種類の外部ドライバーを反復する必要があります。SMT ソルバーの特定の機能を活用できる定量化されたアプローチも可能ですが、実際には、そのような制約は基礎となるソルバーにとっては難しすぎます。特にこの議論を参照してください: Z3 でコードを最適化する方法は? (PI_NON_NESTED_ARITH_WEIGHT 関連)

そうは言っても、ほとんどの高水準言語バインディングには、生活を簡素化するために必要な機構が含まれています。たとえば、Haskell SBV ライブラリを使用して z3 をスクリプト化する場合は、次のようになります。

Prelude> import Data.SBV
Prelude Data.SBV> maximize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]
Prelude Data.SBV> maximize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Nothing
Prelude Data.SBV> minimize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]
Prelude Data.SBV> minimize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]

最初の結果状態 x=3, y=1 は、述語 x==3 && y>=1 に関して x を最大化します。2 番目の結果は、同じ述語に関して y を最大化する値がないことを示しています。3 番目の呼び出しでは、x=3,y=1 が x に関する述語を最小化します。4 番目の呼び出しでは、x=3,y=1 が y に関して述語を最小化します。(詳細については、 http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34を参照してください。)

オプション "Iterative" (Quantified の代わりに) を使用して、量指定子を使用する代わりに、ライブラリに反復的に最適化を実行させることもできます。これら 2 つの手法は同等ではありません。後者は極小値/極大値にとらわれる可能性があるためです。ただし、定量化されたバージョンが SMT ソルバーで処理するには多すぎる場合、反復的なアプローチによって問題が解決される可能性があります。

于 2012-01-30T02:18:48.000 に答える