命題論理論理式の標準形 SAT 充足可能問題、リテラル、解法、Davis-Putnam法

情報系のための離散数学
 楽天ブックス
Yahoo!ショッピング
au PAY マーケット

学習環境

情報系のための離散数学 (猪股俊光 (著)、南野謙一 (著)、共立出版 )の第1章(命題論理)、1.4(論理式の標準形)、1.4.2(SAT)、問題1.15の解答を求めてみる。

Step.1

C = {p}

Step.2

q = p, C = ϕ

Step.3
規則1も規則2も適用できない。

q' = q

Step.4

\begin{array}{l} p_{1} = T \\ p_{2} = F \\ q_{1} = (T \lor p_{2}) \land (\neg T \lor \neg p_{2}) \land (T \lor \neg p_{3}) \land (p_{2} \lor p_{3}) = \neg p_{2} \land (p_{2} \lor p_{3}) \\ q_{2} = (F \lor p_{2}) \land (\neg F \lor \neg p_{2}) \land (F \lor \neg p_{3}) \land (p_{2} \lor p_{3}) = p_{2} \land \neg p_{3} \land (p_{2} \lor p_{3}) \\ C = {q_{1}, q_{2}} \end{array}

Step.2

q = q_{1}, C = {q_{2}}

Step.3

単一の負リテラルが存在するから規則1を適用。

\begin{array}{l} p_{2} = F \\ q = \neg F \land (F \lor p_{3}) = p_{3} \end{array}

単一の正リテラルが存在するからも先を見てを適用。

\begin{array}{l} p_{3} = T \\ q = T \end{array}

これ以上は適用できない。

q' = q = T

これは充足可能なので出力はYES。

よって問題のCNFは充足可能。

コード(Wolfram Language)

p1 = True

p2 = False

p3 = True

(p1 || p2) && (!p1 || !p2) && (p1 || !p3) && (p2 || p3)

Table[
    Table[
        Table[
            {p1, p2, p3,
             (p1 || p2) && (!p1 || !p2) && (p1 || !p3) && (p2 || p3)},
            {p3, {True, False}}
        ],
        {p2, {True, False}}
    ],
    {p1, {True, False}}
]