z3 - MaxSAT/MaxSMT の例

Question

次のリンク http://research.microsoft.com/en-us/um/redmond/projects/z3/group_ maxsat _ex.htmlで「MaxSAT/MaxSMT の例」を見つけまし たが、C コードしか提供していません。

Z3 を直接使用してコーディングする方法に興味がありますか? 誰かが親切に例を教えてくれませんか? ありがとう！

Answer 1

Z3 ドキュメントの MaxSAT/MaxSMT の例の主な目的は、API を使用しZ3_check_assumptionsて MaxSAT の 2 つの異なる手順を実装する方法を示すことです。この例には、基本的な考え方を説明するいくつかのコメントと、Fu と Malik による論文への参照が含まれています。fu_malik_maxsatこのペーパーには、この例の手順で使用されるアルゴリズムの詳細な説明があります。Z3 API の上部に実装できる他の MaxSAT アルゴリズムもあります。

Z3 SMT 2.0 フロントエンド (つまり、z3 実行可能ファイル) は、MaxSAT/MaxSMT を直接サポートしていません。ただし、check-satコマンドに仮定を与えることができます。MaxSAT に関心のあるユーザーは、MaxSAT の例を出発点として使用する必要があります。