乗算を伴う整数の理論は一般的に決定不能であることを認識しています。ただし、場合によっては、Z3 はモデルを返します。これがどのように行われるか知りたいです。実数に対する非線形演算の新しい決定手順と何か関係がありますか? Z3 が乗算クエリのモデルを返す特定のインスタンス (例: 有限モジュラス下の整数など) が認識されていますか? どんな助けでも大歓迎です。
5847 次
1 に答える
36
はい、非線形整数演算の決定問題は決定不能です。チューリング マシンのホールティング問題は、非線形整数演算でエンコードできます。この問題に興味のある人には、ヒルベルトの 10 番目の問題という美しい本を強くお勧めします。
式に解がある場合、力ずくでいつでも見つけることができることに注意してください。つまり、すべての可能な割り当てを列挙し、それらが式を満たすかどうかをテストし続けます。これは、プログラムを実行し、所定のステップ数後にプログラムが終了するかどうかを確認するだけで停止問題を解決しようとするのとそれほど違いはありません。
Z3 は単純な列挙を実行しません。numberkを指定すると、ビットを使用してすべての整数変数をエンコードし、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、問題の解決に失敗したことを示すために戻ります。
于 2012-12-16T04:07:33.623 に答える