充足可能な論理式とは何？わかりやすく解説 Weblio辞書

索引トップ用語の索引ランキング

充足可能な論理式

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/01/26 22:53 UTC 版)

「DPLLアルゴリズム」の記事における「充足可能な論理式」の解説

論理式 ϕ = ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) ∧ ( p ∨ u ) ∧ ( ¬ p ∨ u ) {\displaystyle \phi =(s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)} を考える。アルゴリズムは以下の動きになる。 ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) ∧ ( p ∨ u ) ∧ ( ¬ p ∨ u ) {\displaystyle (s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)} リテラル u {\displaystyle u} は肯定でしか現れないため純リテラルである。純リテラル規則を適用する。（u = 真） ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) {\displaystyle (s\vee t)\wedge (\neg s\vee \neg t)} 1リテラル規則、純リテラル規則とも適用できず単純化できないため、分割規則を適用する。 s = {\displaystyle s=} 真/偽に分解する。 ϕ 1 = ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) { s / t r u e } = ( ¬ t ) {\displaystyle \phi _{1}=(s\vee t)\wedge (\neg s\vee \neg t)\{s/true\}=(\neg t)} と ϕ 2 = ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) { s / f a l s e } = ( t ) {\displaystyle \phi _{2}=(s\vee t)\wedge (\neg s\vee \neg t)\{s/false\}=(t)} 最初に ϕ 1 {\displaystyle \phi _{1}} を調べると1リテラル規則より t = 偽の場合に節が無くなり充足可能であることが分かる。これより全体の論理式が充足可能であることが証明できる。（この例では ϕ 2 {\displaystyle \phi _{2}} も t = 真の場合に充足可能である。） DPLLアルゴリズムの実行の過程より、この論理式は u = 真, t = s = 真/偽の場合に充足可能となることが決定できる。同じ論理式を節集合の形で表現すると以下のようになる。 { { 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 \{\}} 節集合が空になったので、充足可能であることが証明された。

※この「充足可能な論理式」の解説は、「DPLLアルゴリズム」の解説の一部です。
「充足可能な論理式」を含む「DPLLアルゴリズム」の記事については、「DPLLアルゴリズム」の概要を参照ください。

充足可能な論理式

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/08/22 13:10 UTC 版)

「デービス・パトナムのアルゴリズム」の記事における「充足可能な論理式」の解説

論理式 ϕ = ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) ∧ ( p ∨ u ) ∧ ( ¬ p ∨ u ) {\displaystyle \phi =(s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)} を考える。アルゴリズムは以下の動きになる。 ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) ∧ ( p ∨ u ) ∧ ( ¬ p ∨ u ) {\displaystyle (s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)} リテラル u {\displaystyle u} は肯定でしか現れないため純リテラルである。純リテラル規則を適用する。（u = 真） ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) {\displaystyle (s\vee t)\wedge (\neg s\vee \neg t)} 1リテラル規則、純リテラル規則とも適用できないため、s について原子論理式除去規則を適用する。 ( t ∨ ¬ t ) {\displaystyle (t\vee \neg t)} この式はトートロジーのみを含み、充足可能であることが証明できる。さらにクリーンアップ規則を用いれば節が無くなる。同じ論理式を節集合の形で表現すると以下のようになる。 { { 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} ) { { t , ¬ t } } {\displaystyle \{\{t,\neg t\}\}} (クリーンアップ規則, t {\displaystyle t} ) { } {\displaystyle \left\{\ \right\}} 節集合が空になったので、充足可能であることが証明された。