一次理論に関する事実を証明するために Z3 の使用を最適化する実験を行っています。現在、私は Python で 1 次理論を指定し、そこで量化子を接地し、すべての節を証明目標の否定とともに Z3 に送信します。私は、結果を最適化できることを望む次の考えを持っています:証明の目標に関連する理論の数式のみを Z3 に送りたいです。この概念について詳しくは説明しませんが、直感は単純だと思います。私の理論は数式の結合であり、証明目標の真理値に影響を与える可能性のある結合のみを送信したいのです。
私の質問は次のとおりです。これは効率の改善につながるのでしょうか、それとも Z3 はすでに同様の方法を使用していますか? Z3 は、最後のアサーションが証明の目標であると常に想定しているとは思わないため、これを最適化する方法がないため、そうではないと思います。
はい、無関係な事実を削除すると、大きな違いが生じる可能性があります. という形の満たされない式があるとしF_1 and F_2 and (not G)ます。F_1 and (not G)さらに、 は充足不可能であり、充足可能であるとしましょうF_2。F_2あなたが無関係と呼ぶものです。フォーミュラを Z3 に送信する前に削除する安価な方法があればF_2、大きな違いが生じる可能性があります。
Z3 には無関係な事実を「無視」するためのヒューリスティックがありますが、それらは単なるヒューリスティックです。この例では、最悪のシナリオは、F_2Z3 が満たすのが非常に難しいものです。Z3 は基本的に、入力式 (F_1 an F_2 and (not G)作業例の式) を満たす解釈/ソリューションを構築しようとしています。Z3 が解釈を構築することが不可能であることを示すことができる場合、式は充足不能です。実際には、式F_2が Z3 に適合することがすぐに示され、解釈/解決策F_2が競合しない場合にのみ、式は Z3 に無関係ですF_1 and (not G)。そうでない場合、Z3 は で多くのリソースを浪費する可能性がありF_2ます。