DPLLアルゴリズム
この式は矛盾を表し明らかに充足不能である。1リテラル規則を r {\displaystyle r} 、 ¬ r {\displaystyle \neg r} いずれに適用しても空節(リテラルを含まない節)が導かれる。真偽値をどのように割り当てても空節は充足可能にはならず、全体の論理式が充足不能であることが証明できる。
同じ論理式を節集合の形で表現すると以下のようになる。空節を □ で表す。
{ { p , q , ¬ r } , { ¬ q , p } , { ¬ p } , { r , q } } {\displaystyle \{\{p,q,\neg r\},\{\neg q,p\},\{\neg p\},\{r,q\}\}}
(1リテラル規則, p = 偽)
{ { q , ¬ r } , { ¬ q } , { r , q } } {\displaystyle \{\{q,\neg r\},\{\neg q\},\{r,q\}\}}
(1リテラル規則, q = 偽)
{ { ¬ r } , { r } } {\displaystyle \{\{\neg r\},\{r\}\}}
(1リテラル規則, r = 真)
{ {\displaystyle \{} □ } {\displaystyle \}}
空節が含まれるため、充足不能であることが証明された。
同じ論理式を節集合の形で表現すると以下のようになる。
{ { s , t } , { ¬ s , ¬ t } , { p , u } , { ¬ p , u } } {\displaystyle \{\{s,t\},\{\neg s,\neg t\},\{p,u\},\{\neg p,u\}\}}
(純リテラル規則, u = 真)
{ { s , t } , { ¬ s , ¬ t } } {\displaystyle \{\{s,t\},\{\neg s,\neg t\}\}}
(分割規則, s = {\displaystyle s=} 真/偽)
φ 1 = { ¬ t } {\displaystyle \phi _{1}=\{\neg t\}} と
φ 2 = { t } {\displaystyle \phi _{2}=\{t\}}
(1リテラル規則, φ 1 {\displaystyle \phi _{1}} , t = 偽)
{ } {\displaystyle \{\}}
節集合が空になったので、充足可能であることが証明された。