probability - Z3 の条件を満たす割り当てのセットから一様にサンプリングする

Question

Z3定理証明者を使用して、満足のいく割り当てのセットから均一にサンプリングする方法はありますか? そうでない場合、この機能を備えた Z3 に最も近いシステムはどれですか?

Answer 1

Z3 に均一にサンプルを作成させる直接的な方法はありません。

しかし、それは興味深い質問です。たとえば、ユニフォームが何を意味するかについて、どの理論を使用するかによって異なります。

FORMULAツールは、理論のいくつかの特性を考慮した方法で、Z3 の上にランダム化されたサンプリングを実装します。