Z3はどのように非線形整数計算を処理しますか？

Question

私は、乗算を伴う整数の理論は一般的に決めることができないことを知っています。それにもかかわらず、特定の例では、Z3はモデルを返す。私はこれがどのように行われているのか知りたいと思っています。それは実数に対する非線形算術の新しい決定手続きと関係がありますか？特定のインスタンス（例：有限モジュラスなどの整数）が認識されていますが、Z3はそれを乗算クエリのモデルとして返します。どんな助けでも大歓迎です。

Answer 1

はい、非線形整数計算の決定の問題は決めることができません。 チューリングマシンのHalting問題を非線形整数計算でエンコードすることができます。 この問題に関心を持つ人には、美しい本Hilbert's tenth problemを強くお勧めします。

数式に解がある場合は、常にブルートフォースで見つけることができます。つまり、可能なすべての割り当てを列挙し、それらが式を満たすかどうかをテストします。これは、プログラムを実行するだけでHaltingの問題を解決し、与えられたステップ数の後に終了するかどうかを確認することとは異なることではありません。

Z3は素朴な列挙を実行しません。数字kが与えられると、kビットを使用してすべての整数変数を符号化し、すべてを命題論理に還元する。次に、SATソルバーを使用して解を見つける。解が見つかった場合は、それを元の公式の整数解に変換し直します。命題形式の解がない場合は、kを増やそうとするか、別の戦略に切り替える。命題論理へのこの減少は、本質的にモデル/解探索法である。問題が解決策を持たないことを示すことはできません。実際には、すべての整数変数が下限と上限を持つ問題については、それを行うことができます。したがって、Z3は解決策がないことを示すために他の戦略を使用しなければなりません。

また、命題論理への縮小は、非常に小さな解（符号化するビット数が少ない解決策）がある場合にのみ機能します。

• Need help understanding the equation

Z3は、非線形整数演算のための良いサポートを持っていない：私は次のポストにいることを議論します。上記のアプローチは非常に単純です。

http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems

最後に、非線形本当の算術（NLSat）ソルバーが非線形整数問題に対してデフォルトで使用されていません。私の意見では、Mathematicaは技術の最も包括的なポートフォリオを持っているようです。通常、整数問題には非常に効果がありません。 それにもかかわらず、整数問題にもZ3にNLSatを使用させることができます。

(check-sat) 

(check-sat-using qfnra-nlsat) 

では、このコマンドを使用すると、Z3は、現実の問題として問題を解決します：私達はちょうど交換する必要があります。実際の解が見つからない場合は、整数解が存在しないことがわかります。解が見つかった場合、Z3は解が整数変数に実際に整数値を割り当てるかどうかをチェックします。そうでない場合は、 unknownを返して、問題の解決に失敗したことを示します。