この質問を再投稿して申し訳ありません。z3 が複数の未飽和コア、複数の満足のいく割り当てを返すようにする方法
完全を期すために、上記のリンクからの元の質問は次のとおりです。
取得に興味があります (QF_LRA の場合)
- 複数の (最小限またはそれ以外の) UNSAT コアおよび - 複数の SAT 割り当て
このトピックに関する以前の議論についてフォーラムをチェックしました。これらは、現在オフラインのように見えるhttp://rise4fun.com/Z3Py/tutorial/musmssなどの z3 Python チュートリアルを参照してい ます。上記のチュートリアルを見つけるために、githubなどの他の提案を試みましたが、うまくいきませんでした。
以前の質問に対する回答を投稿してくれた Nikolaj Bjorner に感謝します。ただし、回答に掲載されているコード フラグメントが完全かどうかはわかりません。誰かがこれについてコメントできますか？
元の質問への回答で参照されている、参照された論文と Mark Liffiton の Web ページを調べました。完全なコード フラグメントを再投稿または明確化できる場合は、最も役に立ちます。
どうもありがとう