Z3を使って拘束空間からサンプルする

Question

私は変数に束縛された制約を持っています。この拘束空間を効率的にサンプリングする方法を探しています。私はZ3を試してみたところ、空間が些細なものかどうか（すなわち制約が充足可能かどうか）を教えてくれるようだが、何かを最小化または最大化しない限り、空間からの例を得る方法は見当たらない。

私は何かが不足していますか、これはZ3が何であるかではありませんか？

Answer 1

Z3では、制約を満たす変数への代入の1つの例が得られます（.NET APIのSMT2またはSolver.Modelで(get-model)コマンドを試してください（他のAPIでも同様です）） 。次に、モデルの否定をアサートして、ソルバーに次のクエリの別の割り当てを強制的に実行させることができます。この種のスキームは多くのアプリケーションで使用されていますが、必ずしも「効率的」というわけではありませんが、実際にどのようなサンプリングを行っているかによって異なります（たとえば、Z3モデルは検索スペースにランダムには分散しません）。