乗算を伴う整数の理論は一般的に決定不可能であることは承知しています。しかし、特定の例では、Z3 はモデルを返します。これがどのように行われるのか知りたいです。これは、実数上の非線形演算の新しい決定手順と関係があるのでしょうか。Z3 が乗算クエリに対してモデルを返す特定の例 (例: 有限係数の整数など) はどれですか。どのような助言でも大歓迎です。
ベストアンサー1
はい、非線形整数演算の決定問題は決定不可能です。チューリングマシンの停止問題を非線形整数演算でエンコードできます。この素晴らしい本を強くお勧めします。ヒルベルトの第10問題この問題に関心のある人のために。
数式に解がある場合は、常に力ずくで解を見つけることができます。つまり、可能な割り当てをすべて列挙し、それらが数式を満たすかどうかをテストし続けます。これは、プログラムを実行し、指定された数のステップ後に終了するかどうかを確認するだけで停止問題を解決しようとすることとそれほど違いはありません。
Z3 は単純な列挙は行いません。数値 が与えられるとk、すべての整数変数をkビットを使用してエンコードし、すべてを命題論理に還元します。次に、SAT ソルバーを使用して解を見つけます。解が見つかった場合は、元の式の整数解に変換します。命題形式に解がない場合は、 を増やすkか、別の戦略に切り替えようとします。この命題論理への還元は、本質的にはモデル/解を見つける手順です。問題に解が存在しないことを示すことはできません。実際には、すべての整数変数に下限と上限がある問題の場合は、それを行うことができます。そのため、Z3 は解が存在しないことを示すために他の戦略を使用する必要があります。
さらに、命題論理への還元は、非常に小さなソリューション（エンコードするのに必要なビット数が少ないソリューション）がある場合にのみ機能します。これについては次の投稿で説明します。
Z3 は非線形整数演算を十分にサポートしていません。上記のアプローチは非常に単純です。私の意見では、Mathematica は最も包括的な技術ポートフォリオを備えているようです。
http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems
最後に、非線形実数演算 (NLSat) ソルバーは、非線形整数問題ではデフォルトでは使用されません。通常、整数問題では非常に効果がありません。ただし、整数問題でも Z3 に NLSat を使用するように強制することはできます。次のコードを置き換えるだけです。
(check-sat)
と
(check-sat-using qfnra-nlsat)
このコマンドを使用すると、Z3 は実際の問題として問題を解きます。実際の解が見つからない場合、整数解がないことがわかります。解が見つかった場合、Z3 は解が実際に整数値を整数変数に割り当てているかどうかを確認します。そうでない場合は、unknown問題を解決できなかったことを示すために戻ります。