最適化問題を解決する1つの方法は、SMTソルバーを使用して（悪い）ソリューションが存在するかどうかを確認し、提案が満足できなくなるまで、より厳しいコスト制約を段階的に追加することです。このアプローチについては、たとえば、http： //www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdfおよびhttp://isi.uni-bremen.de/agra/doc/konf/で説明されています。 08_isvlsi_optprob.pdf。
しかし、このアプローチは効率的ですか？つまり、ソルバーは、追加の制約を使用して解決しようとしたときに、以前のソリューションからの情報を再利用しますか？
ソルバーは、以前のクエリを解決しようとしたときに学習した見出語を再利用できます。popすべての見出語（対応する以降に作成された）を実行するときは常に、Z3よりも覚えておいてくださいpush。したがって、これを実現するには、アサーションを撤回する必要がある場合はpush、popコマンドを実行して「仮定」を使用する必要があります。次の質問では、Z3で「仮定」を使用する方法について説明します。Z3
でのソフト/ハード制約
効率に関しては、このアプローチはすべての問題領域にとって最も効率的なアプローチではありません。一方、ほとんどのSMTソルバーの上に実装できます。さらに、疑似ブールソルバー（0-1整数問題のソルバー）は、最適化問題を解くために同様のアプローチをうまく使用します。