z3ソルバーに直接節を追加する

Question

私は、私が変更を続け、Z3を使って増分的にチェックする必要があるAIG（およびインバーターグラフ）を持っています。私はAIGのCNF表現を生成することができ、理想的にはこれらの節を直接ソルバに供給し、コードから繰り返し呼び出すことが望ましいでしょう。 C/C++ APIを使用してZ3ソルバーに句（またはAIG）を直接追加できる方法はありますか？

Answer 1

はい、内部的に句に変換される新しいアサーションをアサートするだけで済みます。

多くの漸進的な解決問題では、Z3は市販の専用SATソルバーを使用していませんが、SATソルバーの機能の一部を組み込んだSMTソルバーです。非ブール問題を処理します。したがって、ソルバーをハッキングして直接節を挿入すると、パフォーマンスが大幅に向上することは必ずしもありません。

Z3には専用のブール型SATソルバもあり、純粋にブール型の問題を解決している場合、このソルバははるかに高速です。 (check-sat)を(check-sat-using sat)に置き換えるか、「sat」という戦術を実行することで、このソルバーを強制的に使用することができます。このソルバーの実装はsat_solver.h/.cppにあります。ハックしたい場合は、周りを見回すのが一番です。

Z3では、一部の戦術では前処理ステップとしてAIG独自の実装を使用しています（aig_tactic.h/.cppを参照）。