2

元のシステムを線形不等式で近似することにより、Z3 に 2 つの異なる変数 (または一般的なケース) を持つ整数多項式不等式のシステムの充足可能性を証明するように依頼することは可能ですか?

4

1 に答える 1

1

デフォルトでは、Z3 は非線形整数問題を線形問題として解こうとします。x*y基本的なトリックは、新しい「変数」などの非線形項を扱うことです。非線形整数演算は Z3 では十分にサポートされていません。次の投稿に、Z3 が非線形整数演算を処理する方法の概要があります。

于 2012-12-27T16:40:49.750 に答える