5

いくつかの項の絶対値を含む小さな問題を解決しようとしています。z3 では、abs() 関数はサポートされていません。Pythonにはありますが、最終的にはz3pyに渡す必要があります。Pythonからz3に絶対演算子を使用して用語を渡す方法はありますか、それとも他の方法はありますか? 以下は、小さな例のコードです。

`
x = Int('x')
y = Int('y')

x= abs(2-y)
s=Solver()
s.add(x>0)
s.add(y>0)
s.check()
m=s.model()
print m`

abs() を削除した場合、答えは y=1 になるはずです。この問題を絶対値関数で解決する方法はありますか? abs()。または、Pythonで解決してz3に渡す方法はありますか。sympy も試しましたが、うまくいきません。

4

3 に答える 3

12

1 つのアプローチを次に示します。

x = Int('x')
y = Int('y')

def abs(x):
    return If(x >= 0,x,-x)

s=Solver()
s.add(x == abs(y-2))
s.add(x>0)
s.add(y>0)
s.check()
m=s.model()
print m
于 2014-03-21T02:27:38.360 に答える
1

必要がないように問題を変換できますabs。

あなたの特定の問題では、「x = abs(2-y), x > 0」なので、「abs(2-y) > 0」です。絶対値を負にすることはできず、y != 2 だけで終了しました。

したがって、x 定義と x 関連の制約を削除して、'y != 2' を追加するだけで、同等の問題が発生します。

x の値が必要な場合は、後で Python で y の値から取得します。

于 2014-03-21T00:47:22.537 に答える
0

絶対値の考え方は非常に単純です。ゼロからの距離を知りたい。これを行う 1 つの方法は、すべての負の項の符号をオンにすることです。

if x<0:
    x=-x
于 2014-03-21T00:46:16.243 に答える