充足可能な論理式とは? わかりやすく解説

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\}} 節集合が空になったので、充足可能であることが証明された。

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

ウィキペディア小見出し辞書の「充足可能な論理式」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ



英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  

辞書ショートカット

すべての辞書の索引

「充足可能な論理式」の関連用語

充足可能な論理式のお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



充足可能な論理式のページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
Text is available under GNU Free Documentation License (GFDL).
Weblio辞書に掲載されている「ウィキペディア小見出し辞書」の記事は、WikipediaのDPLLアルゴリズム (改訂履歴)、デービス・パトナムのアルゴリズム (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。

©2025 GRAS Group, Inc.RSS