2

'x<10およびx>=11またはx>20'のような式が与えられ、また、使用可能な式の解析ツリーがすでに存在すると仮定します（たとえば、[または[[および[<[var：x] [10]] [> = [var：x] [11]]]]] [> [var：x] [20]]]）、この式がtrueと評価される原因となるxの範囲/セットを見つけるにはどうすればよいですか？

文法に関するいくつかの制限は次のとおりです。

  1. 式には1つの変数（例ではx）のみが含まれるため、x +2<yのような式はありません。
  2. 比較演算子のみですが、空のようなものである可能性がありますか？式中の[文字列式]
  3. 算術式や関数呼び出しはありません-したがって、x + 2 <3、またはx <someFunc（）のようなものは不可能です
4

2 に答える 2

1

SMTソルバーの簡単な代替手段は次のとおりです。

  1. 式で使用されているすべての数値を抽出します
  2. 番号のリストを並べ替える
  3. リストxの各ポイントについて、x-eps、x、およびx + eps（epsは少数）で式を評価します。

式の値はこれらのポイントでのみ変更できます。これらはソートされた順序であるため、結果を結合するだけで、xに許可される値の完全なリストを見つけることができます。

于 2013-02-25T21:48:56.840 に答える
0

YicesやZ3のようなSMTソルバーが役立つようです。彼らはあなたの問題のための一種の「大きな銃」ですが、トリックを行う必要があります。SMTソルバーは、ステロイドのSATソルバーのようなものであり、非ブール変数を使用した充足可能性問題が事実上あります。

于 2013-02-25T21:34:24.520 に答える