0

与えられた非負の実数tSS, tLS, tIS, tBS。（つまり、tSS>=0かつtLS>=0かつtIS>=0かつtBS>=0かつtSS>=0の実数型です）

次の制約C1は、12の結合を含むCNF形式です。

(tSS+tLS<=tIS)And(tIS<=tBS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tBS)And(tBS<=tIS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tBS)And(tSS<=tIS)And(tIS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS<=tIS)And(tIS<=tBS)And(tBS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tIS)And(tSS<=tBS)And(tBS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS<=tBS)And(tBS<=tIS)And(tIS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tBS)And(tIS<=tSS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS<=tBS)And(tIS<=tBS)And(tBS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tIS<=tBS)And(tBS<=tSS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tIS)And(tBS<=tSS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS<=tIS)And(tBS<=tSS)And(tIS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tIS<=tSS)And(tBS<=tIS)And(tSS+tLS+tIS+tBS<=3)

制約C2を次の形式で取得したい

tSS<=a and tLS<=b and tIS<=c and tBS <=d and tSS<=e

制約C2はC1に含める必要があるだけです。つまり、C2を満たす評価はC1を満たす必要がありますが、その逆はできません。aeの値は、0から無限大までの範囲の値です。無限大とは、0より大きい任意の値を取ることができることを意味します。

Z3を使用してaeの値を推測することは可能ですか？（満足できない場合があります）

4

1 に答える 1

2

それを行うためのより効率的な手法があるかもしれませんが、少なくとも数量詞を使用して問題を解決することができます。

CNFC1(tSS, tLS, tIS, tBS)の公式を示し、C2(SS, tLS, tIS, tBS, a, b, c, d)満たす制約です。次の定量化された式の充足可能性を確認できます。

forall tSS tLS tIS tBS. C2(SS, tLS, tIS, tBS, a, b, c, d) => C1(tSS, tLS, tIS, tBS)

a, b, c, d自由変数はどこにありますか。

Z3SMTをオンラインで使用して具体的な例をエンコードしました。この場合、クエリは満足のいくものではありません。

于 2012-09-01T14:40:14.277 に答える