-1

特定の線形方程式/不等式のセット (A) が別の線形方程式/不等式のセット (B) を伴うかどうかを判断するためのツールを探しています。戻り値は「true」または「false」のいずれかです。

説明のために、A と B の可能なインスタンスと、アルゴリズムの期待される戻り値を見てみましょう。

A: {Z=3,Y=Z+2, X < Y} ;
B: {X<5} ; 
Expected result: true

A: {Z=3,Y=Z+2, X < Y} ;
B: {X<10} ;
Expected result: true

A: {Z=3,Y=Z+2, X < Y} ;
B: {X=3} ; 
Expected result: false

A: {X<=Y,X>=Y} ;
B: {X=Y} ; 
Expected result: true

A: {X<=Y,X>=Y} ;
B: {X=Y, X>Z+2} ; 
Expected result: false

通常、A には最大 10 の方程式/不等式が含まれ、B には 1 つまたは 2 つのものが含まれます。それらはすべて線形で比較的単純です。すべての変数が整数であると仮定することさえできます。

AがBを伴うかどうかを判断するこのタスクは、より大きなシステムの一部であるため、そのようなものをすでに実装していて使用できるツール/ソースコード/パッケージを探しています。

私が見始めたもの：

  1. 代数による定理証明 - Otter、EQP、Z3 (Vampire は現在ダウンロードできません)。
  2. Coq 形式証明管理システム。
  3. 線形計画。

ただし、これらのツールに関する私の経験は非常に限られており、これまでのところ有望な方向性は見つかりませんでした。私よりも経験豊富な人々からのガイドラインやアイデアは、高く評価されます。

お時間をいただきありがとうございます！

4

1 に答える 1