z3 - Z3Py でのモデルのカウント

Question

Z3で満足のいく課題の数を数えようとしています。Z3がそのような情報を提供するかどうか疑問に思っています。もしそうなら、どうすればZ3、特にZ3Pyでモデルを数えることができますか?

Answer 1

テイラーの答えは、満足のいく割り当ての数を提供しますが、それらすべてを反復します。原則として、そのような高価な反復なしでそれを行うことは可能ですが、Z3 はそれを提供しません。

命題論理には効率的なモデル カウンターがあり、これは SAT で使用されている言語と同じです (sharpSAT を検索してそのようなシステムを見つけてください) が、私が知る限り、利用可能なモデル カウンター モジュロ理論はありません。