充足可能で不合理な式の生成

Question

私はいくつかのテストを実行するためにCNF形式で命題式を生成する必要があるプロジェクトで作業しています。そして、私は次の質問に出くわします：

1. どのようにランダム充足式を生成するには？
2. ランダムな有効な数式を生成するにはどうすればよいですか？我々はランダム式pを生成し、式p or not pを取り、その後、CNFでの結果の式を変換するが、問題は、それは、我々はすべての有効な式これを生成することができていることができ、たとえば、私がアイデアを持っている2番目の質問については、

方法？ここ

許可ブール演算子は以下のとおりです。

or,and,notは、あなたの助け

Answer 1

まずいただきありがとうございますLがkリテラルあらかじめ指定されたkためl1,l2,l3,...,lkの集合とします。リテラルのセットが与えられたので、それらからリテラルを生成することができます。

まず、句の数を選択することをお勧めします。結合されたOR式の数---たとえばm、次にn_1、n_2、...、n_m、ここでn_iはOR接続リテラルの数です。これらの数値はランダムに選択するか、数式のサイズと構造をよりよく制御するパラメータとして使用できます。

例えば、m=2とn1=2とn2=2のために、あなたはli年代はLから選択され、いずれか否定かされていないフォーム(l1 OR l2) AND (l3 OR l4)ののCNFを持っていると思います。

今、あなたはどのような式はリテラルの位置を通って、それぞれの位置のために反復し、次のようになります知っている：

• は一様にランダムにLからリテラルlを選択してください。
• 公正なコインを入れて、リテラルを否定するかどうかを決定します。

あなたはCNFで "ランダム"の式になります。しかし、それが充足可能かどうかは分かりません。

更新（2016年4月5日）です。あなたが効率的に与えられたパラメータk、m、およびni年代にランダム満足できるCNFを生成したい場合は、効率的に（このため、暗黙的に3-SAT問題を解決）に充足された数式を計算することができなければなりません。この理由から、ランダム 3-CNFを生成するための多項式時間アルゴリズム（P = NP）はありません（与えられた構造を持つ充足可能な3-CNFが等しくなるように）。ランダムな3-CNFを生成することは困難であるため、一般にCNFも生成されます。

おそらく実用的な目的のために十分に満足できる3-CNFのサブセットを生成するためのアルゴリズムがあります。満たされていないインスタンスを生成する場合も同じです。