実際にコーディングする前に、DPLL手順を理解しようとしています。
たとえば、次の句があります。
C1 : {c, !d, !b}
C2 : {d, a}
C3: {b, !d, !a}
C4: {d, c, b, a}
C5: {c, !d, !b}
C6: {d, c, b}
C7: {c}
ここで、決定変数を d = 0、b = 0 とします。節は次のようになります。
C1: {c, 1, 1}
C2: {a}
C3: {1, !a}
C4: {c, a}
C5: {c, 1, 1}
C6: {c}
C7: {c}
ここで、ユニットの伝播と純粋なリテラル規則がどのように役割を果たすのでしょうか?
また、C3 : {1, !a}- を とるa = 1と、これは になり{1, 0}ます。この句の最終的な値は何ですか? {1} にする必要がありますか?
そして、決定変数を適用した後、いずれかの節に value {!b}、つまりリテラルの否定がある場合、どのように処理を進めればよいでしょうか?