cnf - CNF 式を 3-CNF に再キャストするにはどうすればよいですか?

Question

このような CNF 式があり、それを 3-CNF に再キャストしたい:

(a+b+c+d)(~a)(~b+d)(a+b+~d)

どうすればそれができるか知っている人はいますか？

Answer 1

3-CNFは、すべての句に 3 つ以下のリテラルがある接続法標準形です。式のこのような形式を取得するには、すべての演算子 (および、または) が 2 つのオペランドを持つネストされたブール式に式を変換できます。

t1a = (a+b)
t1b = (c+d)
t1 = t1a + t1b
t2 = (~a)
t3 = (~b+d)
t4a = (a+b)
t4 = t4a + ~d
t5a = t1 t2
t5b = t3 t4
t5 = t5a t5b

このネストされた式を 3 つの CNF 句のセットに直接変換できます。

最小化されたソリューション:

(~a)(~b + d)(b + ~d)(c + d)  

WolframAlphaが示唆するよう3-CNFに、より長い句が含まれていないため、あなたの式です。

小さなケースでは、真理値表を埋めることができます。出力が 0 のすべての行を見て、これらすべての行をカバーする minterms を見つけます。次に、minterm のすべてのリテラルを反転すると、CNF. 節に 3 つ以上のリテラルがある場合、中間変数を導入することで、2 つ以上の短い節に分割できます。そのために広く使用されている手順は、Tseitin Transformationまたは Tseitin Encoding と呼ばれます。