充足不能な論理式
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2019/01/26 22:53 UTC 版)
「DPLLアルゴリズム」の記事における「充足不能な論理式」の解説
論理式 ϕ = ( p ∨ q ∨ ¬ r ) ∧ ( ¬ q ∨ p ) ∧ ( ¬ p ) ∧ ( r ∨ q ) {\displaystyle \phi =(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)} の充足可能性を考える。 アルゴリズムは以下の動きになる。 ( p ∨ q ∨ ¬ r ) ∧ ( ¬ q ∨ p ) ∧ ( ¬ p ) ∧ ( r ∨ q ) {\displaystyle (p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)} リテラル1つだけの節 ( ¬ p {\displaystyle \neg p} ) に1リテラル規則を適用する。 ¬ p {\displaystyle \neg p} を真と見なせば p {\displaystyle p} は偽である。 ( q ∨ ¬ r ) ∧ ( ¬ q ) ∧ ( r ∨ q ) {\displaystyle (q\vee \neg r)\wedge (\neg q)\wedge (r\vee q)} 1リテラル規則はさらに ¬ q {\displaystyle \neg q} にも適用できる。 ( ¬ r ) ∧ ( r ) {\displaystyle (\neg r)\wedge (r)} この式は矛盾を表し明らかに充足不能である。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 \}} 空節が含まれるため、充足不能であることが証明された。
※この「充足不能な論理式」の解説は、「DPLLアルゴリズム」の解説の一部です。
「充足不能な論理式」を含む「DPLLアルゴリズム」の記事については、「DPLLアルゴリズム」の概要を参照ください。
充足不能な論理式
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2018/08/22 13:10 UTC 版)
「デービス・パトナムのアルゴリズム」の記事における「充足不能な論理式」の解説
論理式 ϕ = ( p ∨ q ∨ ¬ r ) ∧ ( ¬ q ∨ p ) ∧ ( ¬ p ) ∧ ( r ∨ q ) {\displaystyle \phi =(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)} の充足可能性を考える。 アルゴリズムは以下の動きになる。 ( p ∨ q ∨ ¬ r ) ∧ ( ¬ q ∨ p ) ∧ ( ¬ p ) ∧ ( r ∨ q ) {\displaystyle (p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)} リテラル1つだけの節 ( ¬ p {\displaystyle \neg p} ) に1リテラル規則を適用する。 ¬ p {\displaystyle \neg p} を真と見なせば p {\displaystyle p} は偽である。 ( q ∨ ¬ r ) ∧ ( ¬ q ) ∧ ( r ∨ q ) {\displaystyle (q\vee \neg r)\wedge (\neg q)\wedge (r\vee q)} 1リテラル規則はさらに ¬ q {\displaystyle \neg q} にも適用できる。 ( ¬ r ) ∧ ( r ) {\displaystyle (\neg r)\wedge (r)} この式は矛盾を表し明らかに充足不能である。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 \}\ } 空節が含まれるため、充足不能であることが証明された。
※この「充足不能な論理式」の解説は、「デービス・パトナムのアルゴリズム」の解説の一部です。
「充足不能な論理式」を含む「デービス・パトナムのアルゴリズム」の記事については、「デービス・パトナムのアルゴリズム」の概要を参照ください。
- 充足不能な論理式のページへのリンク