haskellでランダムな命題式を取得するにはどうすればよいですか? できればCNFの式が必要ですが、そうします
私は、SAT ソルバーも含むパフォーマンス テストの式を使用したいと考えています。私の目標は、SAT ソルバーのパフォーマンスをテストすることではないことに注意してください。私は非常に難しい数式にも興味がないので、難易度はランダムにするか、簡単な数式のみを含める必要があります。
私の現実世界のデータは、SAT ソルバーにとって難しくない命題の公式につながることを知っています。
現時点では、HattライブラリとSBVライブラリをデータ構造として使用して、命題式を操作しています。hGenライブラリも調べました。おそらく、ランダムな式を生成するために使用できます。ただし、ドキュメントはなく、hGenのソース コードを見てもうまくいきませんでした。
私の目標は、ブール変数nを含む数式を選択して取得することです。n