ブール代数

  • 2019/05/29 09:00
  • math
この記事は, 旧ブログから移植された記事です. よって, その内容として, 旧ブログに依存した文脈が含まれている可能性があります. 予めご了承下さい.

ブール代数は古典論理における命題論理と密接に関連している. 結論からいえば, 両者の違いは歴史的な背景ぐらいであり, 殆どの場合は同等の理論であるということができる1. ブール代数はその応用として論理回路の構築に直接役立つことから, 計算機科学, とくにハードウェアの分野において重宝される代数系の 1 つである.

ブール代数の公理とその定理

次に示すのはブール代数の公理系である. 公理系に関する詳細は証明理論 (TODO) の冒頭を参照のこと.

ブール代数

半順序集合 (B,∨,∧,′,0,1)(B,\lor,\land,',0,1) が可補分配束ならば, (B,∨,∧,′,0,1)(B,\lor,\land,',0,1) はブール代数である. すなわち, x,y,z∈Bx,y,z\in B に対して, 次のすべての公理を満たした (B,∨,∧,′,0,1)(B,\lor,\land,',0,1) はブール代数である.

  1. 可換律\htmlId{boolean_algebra1}{\rm 可換律}: x∧y=y∧x,x∨y=y∨xx\land y=y\land x,x\lor y=y\lor x
  2. 分配律\htmlId{boolean_algebra2}{\rm 分配律}: (x∨y)∧z=(x∧z)∨(y∧z),(x∧y)∨z=(x∨z)∧(y∨z)(x\lor y)\land z=(x\land z)\lor(y\land z),(x\land y)\lor z=(x\lor z)\land(y\lor z)
  3. 同一律\htmlId{boolean_algebra3}{\rm 同一律}: ∀x∈L^\forall x\in L に対して x∧1=x,x∨0=xx\land 1=x,x\lor 0=x. ここで 11 は最大限, 単位元である. 00 は最小限, 零元である.
  4. 補元律\htmlId{boolean_algebra4}{\rm 補元律}: ∃x′∈L s.t. ∀x∈L,x∨x′=1,x∧x′=0^\exists x'\in L\ {\rm s.t.}\ ^\forall x\in L, x\lor x'=1, x\land x'=0

また, この 1,01,0 からのみ成る集合をブール領域, ブール代数の下に書かれた式をブール式, n∈Nn\in\mathbb{N} 個のブール領域の引数をとり, 1 個のブール領域の値となる関数 f:Bn→Bf:B^n\to B をブール関数という. 例えば, 2 変数ブール関数 f(x1,x2)f(x_1,x_2) では x1,x2x_1,x_2 がそれぞれ 1,01,0 のいずれかとなるので, 24=162^4=16 通りの 2 変数ブール式が存在することとなる. 以下, 演算の優先順序は左結合性で ′,∧,∨',\land,\lor の順とする. ただし, 括弧内の演算はより優先される.

さてブール代数の公理における乗法 ∧\land と加法 ∨\lor, および 1,01, 0 をそれぞれ入れ替えると, 再びブール代数の公理である. これは双対の原理という公理である.

双対の原理

ブール代数で成立する文/式は, そこに現れるすべての ∨,∧,0,1\lor ,\land,0,1 をそれぞれ ∧,∨,1,0\land,\lor ,1,0 で置き換えても成立する.

これらの公理から補元の一意性, べき等律, 有界律, 吸収律, 結合律, 対合律, ド・モルガンの法則, シャノンの展開定理が導出可能である. 以下 x,y,z∈Bx,y,z\in B とする.

補元の一意性

xx に対する補元は一意である.

補元の一意性

2 つの xx の補元 x1′,x2′x'_1,x'_2 を仮定する. x1′=x1′∧1(∵公理3:同一律)=x1′∧(x∨x2′)(∵公理4:補元律)=(x1′∧x)∨(x1′∧x2′)(∵公理2:分配律)=0∨(x1′∧x2′)(∵公理4:補元律)=(x∧x2′)∨(x1′∧x2′)(∵公理4:補元律)=x2′∧(x∨x1′)(∵公理2:分配律)=x2′∧1(∵公理4:補元律)=x2′(∵公理3:同一律)\begin{aligned} x'_1&=&x'_1\land1&(\because {\rm \href{#boolean_algebra3}{公理 3}:同一律})\\ &=&x'_1\land(x\lor x'_2)&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&(x'_1\land x)\lor (x'_1\land x'_2)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&0\lor (x'_1\land x'_2)&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&(x\land x'_2)\lor (x'_1\land x'_2)&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&x'_2\land(x\lor x'_1)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&x'_2\land1&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&x'_2&(\because {\rm \href{#boolean_algebra3}{公理 3}:同一律}) \end{aligned} より xx の補元が一意であることは明らか.

べき等律

以下が成り立つ.

  1. x∧x⇔xx\land x\Leftrightarrow x
  2. x∨x⇔xx\lor x\Leftrightarrow x

べき等律

束の定理による.

有界律

以下が成り立つ.

  1. x∨1=1x\lor 1=1
  2. x∧0=0x\land 0=0

有界律

x∨1=(x∨1)∧1(∵公理3:同一律)=(x∨1)(x∨x′)(∵公理4:補元律)=x∨(1∧x′)(∵公理2:分配律)=x∨x′(∵公理1,公理3:可換律,同一律)=1x∧0=x∧x∧x′(∵公理4:補元律)=x∧x′(∵定理:べき等律)=0(∵公理4:補元律)\begin{aligned} x\lor 1&=&(x\lor 1)\land1&(\because {\rm \href{#boolean_algebra3}{公理 3}:同一律})\\ &=&(x\lor 1)(x\lor x')&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&x\lor (1\land x')&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&x\lor x'&(\because {\rm \href{#boolean_algebra1}{公理1}, \href{#boolean_algebra3}{公理3}:可換律, 同一律})\\ &=&1\\ x\land0&=&x\land x\land x'&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&x\land x'&(\because {\rm 定理:\href{#idempotence}{べき等律}})\\ &=&0&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律}) \end{aligned}

吸収律

以下が成り立つ.

x∨x∧y=x∧(x∨y)=xx\lor x\land y=x\land(x\lor y)=x

吸収律

x∨x∧y=(x∧1)∨(x∧y)(∵公理3:同一律)=x∧(1∨y)(∵公理2:分配律)=x∧1(∵公理1:可換律,定理:有界律)=x(∵公理3:同一律)x∧(x∨y)=(x∨0)(x∨y)(∵公理3:同一律)=(0∧y)∨x(∵公理2:分配律)=x∨0(∵公理1:可換律,定理:有界律)=x(∵公理3:同一律)\begin{aligned} x\lor x\land y&=&(x\land1)\lor (x\land y)&(\because {\rm \href{#boolean_algebra3}{公理3}: 同一律})\\ &=&x\land(1\lor y)&(\because {\rm \href{#boolean_algebra2}{公理2}:分配律})\\ &=&x\land1&(\because {\rm \href{#boolean_algebra1}{公理 1}: 可換律, 定理: \href{#bounded}{有界律}} )\\ &=&x&(\because {\rm\href{#boolean_algebra3}{公理 3}: 同一律})\\ x\land(x\lor y)&=&(x\lor 0)(x\lor y)&(\because {\rm \href{#boolean_algebra3}{公理3}: 同一律})\\ &=&(0\land y)\lor x&(\because {\rm \href{#boolean_algebra2}{公理2}: 分配律})\\ &=&x\lor 0&(\because \rm{\href{#boolean_algebra1}{公理1}: 可換律,定理: \href{#bounded}{有界律}})\\ &=&x&(\because \rm{\href{#boolean_algebra3}{公理3}: 同一律}) \end{aligned}

結合律

以下が成り立つ.

x∨(y∨z)=(x∨y)∨zx\lor(y\lor z)=(x\lor y)\lor z

結合律

A=x∨(y∨z),B=(x∨y)∨zA=x\lor (y\lor z), B=(x\lor y)\lor z とおく. このとき,

x∧A=x∧(x∨(y∨z))=x(∵定理:吸収律)x∧B=x∧((x∨y)∨z)=x∧(x∨y)∨x∧z(∵公理2:分配律)=x∨x∧z(∵定理:吸収律)=x(∵定理:吸収律)\begin{aligned} x\land A&=&x\land(x\lor (y\lor z))\\ &=&x&(\because {\rm 定理: \href{#absorption}{吸収律}})\\ x\land B&=&x\land((x\lor y)\lor z)\\ &=&x\land(x\lor y)\lor x\land z&(\because {\rm \href{#boolean_algebra2}{公理2}: 分配律})\\ &=&x\lor x\land z&(\because {\rm 定理: \href{#absorption}{吸収律}})\\ &=&x&(\because {\rm 定理: \href{#absorption}{吸収律}}) \end{aligned}

ゆえに x∧A=x∧B=x(L1)x\land A=x\land B=x\tag{L1} また,

x′∧A=x′∧(x∨(y∨z))=x′∧x∨x′∧(y∨z)(∵公理2:分配律)=x′∧(y∨z)∨0(∵公理1,公理4:可換律,補元律)=x′∧(y∨z)(∵公理3:同一律)x′∧B=x′∧((x∨y)∨z)=x′∧(x∨y)∨x′∧z(∵公理2:分配律)=(x′∧x∨x′∧y)∨x′∧z(∵公理2:分配律)=(0∨x′∧y)∨x′∧z(∵公理4:補元律)=x′∧y∨x′∧z(∵公理3:同一律)=x′∧(y∨z)(∵公理2:分配律)\begin{aligned} x'\land A&=&x'\land(x\lor (y\lor z))\\ &=&x'\land x\lor x'\land(y\lor z)&(\because {\rm \href{#boolean_algebra2}{公理2}: 分配律})\\ &=&x'\land(y\lor z)\lor 0&(\because {\rm \href{#boolean_algebra1}{公理1}, \href{#boolean_algebra4}{公理 4}: 可換律, 補元律})\\ &=&x'\land(y\lor z)&(\because {\rm \href{#boolean_algebra3}{公理3}: 同一律})\\ x'\land B&=&x'\land((x\lor y)\lor z)\\ &=&x'\land(x\lor y)\lor x'\land z&(\because {\rm \href{#boolean_algebra2}{公理2}: 分配律})\\ &=&(x'\land x\lor x'\land y)\lor x'\land z&(\because {\rm \href{#boolean_algebra2}{公理2}: 分配律})\\ &=&(0\lor x'\land y)\lor x'\land z&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&x'\land y\lor x'\land z&(\because {\rm \href{#boolean_algebra3}{公理3}: 同一律})\\ &=&x'\land(y\lor z)&(\because {\rm \href{#boolean_algebra2}{公理2}: 分配律}) \end{aligned}

ゆえに x′∧A=x′∧B=x′∧(y∨z)(L2)x'\land A=x'\land B=x'\land(y\lor z)\tag{L2} 従って,

A=A∧1(∵公理3:同一律)=A∧(x∨x′)(∵公理4:補元律)=A∧x∨A∧x′(∵公理2:分配律)=x∧A∨x′∧A(∵公理1:可換律)=x∧B∨x′∧B(∵, より)=B(x∨x′)(∵公理2:分配律)=B∧1(∵公理4:補元律)=B(∵公理3:同一律)\begin{aligned} A&=&A\land1&(\because {\rm \href{#boolean_algebra3}{公理3}: 同一律})\\ &=&A\land(x\lor x')&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&A\land x\lor A\land x'&(\because {\rm \href{#boolean_algebra2}{公理2}: 分配律})\\ &=&x\land A\lor x'\land A&(\because {\rm \href{#boolean_algebra1}{公理1}: 可換律})\\ &=&x\land B\lor x'\land B&(\because,\ {\rm より})\\ &=&B(x\lor x')&(\because {\rm \href{#boolean_algebra2}{公理2}: 分配律})\\ &=&B\land1&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&B&(\because {\rm \href{#boolean_algebra3}{公理3}: 同一律}) \end{aligned}

また, 双対の原理より x(y∧z)=(x∧y)∧zx(y\land z)=(x\land y)\land z.

対合律

以下が成り立つ.

(x′)′=x(x')'=x

対合律

(x′)′=(x′)′∨0(∵公理3:同一律)=(x′)′∨x∧x′(∵公理4:補元律)=((x′)′∨x)((x′)′∨x′)(∵公理2:分配律)=(x∨(x′)′)∧1(∵公理1,公理4:可換律,補元律)=(x∨(x′)′)(x∨x′)(∵公理4:補元律)=x∨((x′)′∧x′)(∵公理2:分配律)=x∨0(∵公理4:補元律)=x(∵公理3:同一律)\begin{aligned} (x')'&=&(x')'\lor 0&(\because \rm{\href{#boolean_algebra3}{公理3}: 同一律})\\ &=&(x')'\lor x\land x'&(\because {\href{#boolean_algebra4}{公理 4}:補元律})\\ &=&((x')'\lor x)((x')'\lor x')&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&(x\lor (x')')\land1&(\because {\rm \href{#boolean_algebra1}{公理1}, \href{#boolean_algebra4}{公理 4}:可換律, 補元律})\\ &=&(x\lor (x')')(x\lor x')&(\because {\rm \href{#boolean_algebra4}{公理 4}: 補元律})\\ &=&x\lor ((x')'\land x')&(\because {\rm \href{#boolean_algebra2}{公理2}:分配律})\\ &=&x\lor 0&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&x&(\because {\rm \href{#boolean_algebra3}{公理3}: 同一律}) \end{aligned}

ド・モルガンの法則

以下が成り立つ. (x∨y)′=x′∧y′(x\lor y)'=x'\land y'

ド・モルガンの法則

x′∧y′x'\land y' が (x∨y)(x\lor y) の補元でなければならない. すなわち, 公理4: 補元律より (x∨y)∨(x′∧y′)=1(x\lor y)\lor (x'\land y')=1 および (x∨y)∧(x′∧y′)=0(x\lor y)\land(x'\land y')=0 が同時に成り立つことを示せばよい.

(x∨y)∨(x′∧y′)=((x∨y)∨x′)((x∨y)∨y′)(∵公理2:分配律)=(y∨(x∨x′))(x∨(y∨y′))(∵公理1:可換律,定理:結合律)=(y∨1)(x∨1)(∵公理4:補元律)=1∧1(∵定理:有界律)=1(∵定理:べき等律)(x∨y)∧(x′∧y′)=(x′∧y′)∧(x∨y)(∵公理1:可換律)=((x′∧y′)∧x)∨((x′∧y′)∧y)(∵公理2:分配律)=(y′∧(x∧x′))∨(x′∧(y∧y′))(∵公理1:可換律,定理:結合律)=(y′∨0)∨(x′∧1)(∵公理4:補元律)=0∨0(∵定理:有界律)=0(∵定理:べき等律)\begin{aligned} (x\lor y)\lor (x'\land y')&=&((x\lor y)\lor x')((x\lor y)\lor y')&(\because {\rm \href{#boolean_algebra2}{公理2}:分配律})\\ &=&(y\lor (x\lor x'))(x\lor (y\lor y'))&(\because {\rm \href{#boolean_algebra1}{公理1}: 可換律, 定理: \href{#associative}{結合律}})\\ &=&(y\lor 1)(x\lor 1)&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&1\land1&(\because {\rm 定理: \href{#bounded}{有界律}} )\\ &=&1&(\because {\rm 定理:\href{#idempotence}{べき等律}})\\ (x\lor y)\land(x'\land y')&=&(x'\land y')\land(x\lor y)&(\because {\rm \href{#boolean_algebra1}{公理1}: 可換律})\\ &=&((x'\land y')\land x)\lor ((x'\land y')\land y)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&(y'\land(x\land x'))\lor (x'\land(y\land y'))&(\because {\rm \href{#boolean_algebra1}{公理1}: 可換律, 定理: \href{#associative}{結合律}})\\ &=&(y'\lor 0)\lor (x'\land1)&(\because {\rm \href{#boolean_algebra4}{公理 4}: 補元律})\\ &=&0\lor 0&(\because {\rm 定理: \href{#bounded}{有界律}} )\\ &=&0&(\because {\rm 定理:\href{#idempotence}{べき等律}}) \end{aligned}

また, 双対の原理より (x∧y)′=x′∨y′(x\land y)'=x'\lor y'.

シャノン展開

任意の nn 変数ブール関数 f(x1,x2,⋯ ,xn)f(x_1,x_2,\cdots,x_n) を x1x_1 について, 次のように展開できる.

f(x1,x2,⋯ ,xn)=(x1′∨x1)∧f(x1,x2,⋯ ,xn)(∵公理4,公理3:補元律,同一律)=x1′∧f(x1,x2,⋯ ,xn)∨x1∧f(x1,x2,⋯ ,xn)(∵公理2:分配律)=x1′∧f(0,x2,⋯ ,xn)∨x1∧f(1,x2,⋯ ,xn)(∵以下に証明)\begin{aligned} f(x_1,x_2,\cdots,x_n)&=&(x'_1\lor x_1)\land f(x_1,x_2,\cdots,x_n)&(\because {\rm \href{#boolean_algebra4}{公理 4}, \href{#boolean_algebra3}{公理 3} :補元律, 同一律})\\ &=&x'_1\land f(x_1,x_2,\cdots,x_n)\lor x_1\land f(x_1,x_2,\cdots,x_n)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&x'_1\land f(0,x_2,\cdots,x_n)\lor x_1\land f(1,x_2,\cdots,x_n)&(\because \href{#chanon_theorem_proof}{以下に証明}) \end{aligned}

シャノン展開

x1=0x_1=0 のとき, f(0,x2,⋯ ,xn)=1∧f(0,x2,⋯ ,xn)∨0∧f(1,x2,⋯ ,xn)=f(0,x2,⋯ ,xn)f(0,x_2,\cdots,x_n)=1\land f(0,x_2,\cdots,x_n)\lor 0\land f(1,x_2,\cdots,x_n)=f(0,x_2,\cdots,x_n) x1=1x_1=1 のとき, f(1,x2,⋯ ,xn)=0∧f(0,x2,⋯ ,xn)∨1∧f(1,x2,⋯ ,xn)=f(1,x2,⋯ ,xn)f(1,x_2,\cdots,x_n)=0\land f(0,x_2,\cdots,x_n)\lor 1\land f(1,x_2,\cdots,x_n)=f(1,x_2,\cdots,x_n)

例として, f(x1,x2,x3)=x1∧x2∨x2∧x3∨x1∧x3f(x_1,x_2,x_3)=x_1\land x_2\lor x_2\land x_3\lor x_1\land x_3 を x1x_1 について展開すると,

f(x1,x2,x3)=x1∧x2∨x2∧x3∨x1∧x3=(x1′∨x1)∧f(x1,x2,x3)(∵公理4,公理3:補元律,同一律)=x1′∧f(x1,x2,x3)∨x1∧f(x1,x2,x3)(∵公理2:分配律)=x1′∧f(0,x2,x3)∨x1∧f(1,x2,x3)(∵定理:シャノンの展開定理)=x1′∧x2∧x3∨x1∧x2∨x2∧x3∨x3(∵公理3:同一律)=x1′∧x2∧x3∨x1∧x2∨x3(∵公理1:可換律,定理:吸収律)\begin{aligned} f(x_1,x_2,x_3)&=&x_1\land x_2\lor x_2\land x_3\lor x_1\land x_3\\ &=&(x'_1\lor x_1)\land f(x_1,x_2,x_3)&(\because {\rm \href{#boolean_algebra4}{公理 4}, \href{#boolean_algebra3}{公理 3} :補元律, 同一律})\\ &=&x'_1\land f(x_1,x_2,x_3)\lor x_1\land f(x_1,x_2,x_3)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&x'_1\land f(0,x_2,x_3)\lor x_1\land f(1,x_2,x_3)&(\because {\rm 定理: \href{#chanon_theorem}{シャノンの展開定理}})\\ &=&x'_1\land x_2\land x_3\lor x_1\land x_2\lor x_2\land x_3\lor x_3&(\because {\rm \href{#boolean_algebra3}{公理 3}:同一律})\\ &=&x'_1\land x_2\land x_3\lor x_1\land x_2\lor x_3&(\because {\rm \href{#boolean_algebra1}{公理1}: 可換律, 定理: \href{#absorption}{吸収律}})\\ \end{aligned}

となる. また双対の原理より,

f(x1,x2,⋯ ,xn)=(x1∧x1′)∨f(x1,x2,⋯ ,xn)(∵公理4,公理3:補元律,同一律)=(x1∨f(x1,x2,⋯ ,xn))∧(x1′∨f(x1,x2,⋯ ,xn))(∵公理2:分配律)=(x1∨f(0,x2,⋯ ,xn))∧(x1′∨f(1,x2,⋯ ,xn))(∵上記証明の双対)\begin{aligned} f(x_1,x_2,\cdots,x_n)&=&(x_1\land x'_1)\lor f(x_1,x_2,\cdots,x_n)&(\because {\rm \href{#boolean_algebra4}{公理 4}, \href{#boolean_algebra3}{公理 3} :補元律, 同一律})\\ &=&(x_1\lor f(x_1,x_2,\cdots,x_n))\land(x'_1\lor f(x_1,x_2,\cdots,x_n))&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&(x_1\lor f(0,x_2,\cdots,x_n))\land(x'_1\lor f(1,x_2,\cdots,x_n))&(\because {\rm \href{#chanon_theorem_proof}{上記証明}の\href{#dual_def}{双対}}) \end{aligned}

この展開をシャノン双対展開という.

標準形

異なる表現のなされたブール式が同値であるかを即座に断定することは, 一般的に困難であることが多い2. ここで, ブール式を一意に表す方法が決まっていれば, 即座に同値であるか判断がしやすく, 便利である. ブール代数では主に 2 つの形式が決められており, その形式への変形を標準化, また正規化という. 以下, nn 変数ブール関数 f(x1,x2,⋯ ,xn)f(x_1,x_2,\cdots,x_n) において, x1,x2,⋯ ,xnx_1,x_2,\cdots,x_n を入力変数, また入力変数およびその否定をリテラルという. さらに nn 個の入力変数に対し, kk 番目のリテラル xkek (1≤k≤n)x_k^{e_k}\ (1\leq k\leq n) を次のように表す.

xkek={xk(=xk1)ek=1 のときxk′(=xk0)ek=0 のとき\begin{aligned} x^{e_k}_k=\begin{cases} x_k&(=x^1_k)&e_k=1{\rm\ のとき}\\ x'_k&(=x^0_k)&e_k=0{\rm\ のとき} \end{cases} \end{aligned}

加法標準形, 主加法標準形

f(x1,x2,⋯ ,xn)f(x_1,x_2,\cdots,x_n) を x1,x2x_1,x_2 についてシャノン展開すると,

f(x1,x2,⋯ ,xn)=x1′∧x2′∧f(0,0,⋯ ,xn)∨x1′∧x2∧f(0,1,⋯ ,xn)∨x1∧x2′∧f(1,0,⋯ ,xn)∨x1∧x2∧f(1,1,⋯ ,xn)\begin{aligned} f(x_1,x_2,\cdots,x_n)&=&x'_1\land x'_2\land f(0,0,\cdots,x_n)\\ &&\lor x'_1\land x_2\land f(0,1,\cdots,x_n)\\ &&\lor x_1\land x'_2\land f(1,0,\cdots,x_n)\\ &&\lor x_1\land x_2\land f(1,1,\cdots,x_n) \end{aligned}

となる. 従って, 全入力変数 x1,x2,⋯ ,xnx_1,x_2,\cdots,x_n についてシャノン展開すると,

f(x1,x2,⋯ ,xn)=x1′∧x2′∧⋯∧xn′∧f(0,0,⋯ ,0)∨x1′∧x2′∧⋯∧xn∧f(0,0,⋯ ,1)∨⋯∨x1∧x2∧⋯∧xn′∧f(1,1,⋯ ,0)∨x1∧x2∧⋯∧xn∧f(1,1,⋯ ,1)\begin{aligned} f(x_1,x_2,\cdots,x_n)&=&x'_1\land x'_2\land\cdots\land x'_n\land f(0,0,\cdots,0)\\ &&\lor x'_1\land x'_2\land\cdots\land x_n\land f(0,0,\cdots, 1)\\ &&\lor\cdots\\ &&\lor x_1\land x_2\land\cdots\land x'_n\land f(1,1,\cdots,0)\\ &&\lor x_1\land x_2\land\cdots\land x_n\land f(1,1,\cdots,1) \end{aligned}

となる (シャノンの定理より数学的帰納法により証明できるが, 省略). これを以下のように定義する.

最小項展開

nn 変数ブール関数 f(x1,x2,⋯ ,xn)f(x_1,x_2,\cdots,x_n) のすべての入力変数 x1,x2,⋯ ,xnx_1,x_2,\cdots,x_n について, シャノン展開した形式 f(x1,x2,⋯ ,xn)=⋁(e1,e2,⋯ ,en)∈Bnf(e1,e2,⋯ ,en)∧⋀i=1nxiei(1)f(x_1,x_2,\cdots,x_n)= \bigvee_{(e_1,e_2,\cdots,e_n)\in B^n}f(e_1,e_2,\cdots,e_n)\land\bigwedge_{i=1}^{n}x_i^{e_i}\tag{1} は f(x1,x2,⋯ ,xn)f(x_1,x_2,\cdots,x_n) の最小項展開である. なお, このときの項数は 2n2^n となる.

これを踏まえ, 加法標準形および主加法標準形を導入する.

加法標準形, 主加法標準形

  • 加法標準形 (disjunctive normal form: DNF) は, ブール式のリテラル, または 2 つ以上のリテラルの積の和のことをいう. ここで, 2 つ以上のリテラルの積で同じ入力変数を 2 度以上含まない論理式を基本積, また標準項という. 基本積のうち, すべての入力変数を含むブール式を最小項という. すなわち, 上記最小項展開の ⋀i=1nxiei\displaystyle\bigwedge_{i=1}^nx^{e_i}_i は最小項である.
  • 主加法標準形 (principal disjunctive normal form: PDNF) は, ブール関数を最小項展開した形式, すなわち最小項展開の形式である.

例えば, 否定論理積 ∣\mid を PDNF で表すとしよう. 否定論理和は 2 項演算子なので, その PDNF は 2 変数ブール関数を最小項展開した形となる.

f(x1,x2)=f(0,0)∧x1′∧x2′∨f(0,1)x1′∧x2∨f(1,0)∧x1∧x2′∨f(1,1)∧x1∧x2f(x_1,x_2)=f(0,0)\land x'_1\land x'_2\lor f(0,1)x'_1\land x_2\lor f(1,0)\land x_1\land x'_2\lor f(1,1)\land x_1\land x_2

便宜上, 2 項演算子 ∣\mid を最小項展開した形を f∣(x1,x2)f_\mid(x_1,x_2) で表すこととする. あとは真理値表 2 の ∣\mid の列のとおりに f∣(x1,x2)f_\mid(x_1,x_2) の値を決めてやればよいので

f∣(x1,x2)=1∧x1′∧x2′∨1∧x1′∧x2∨1∧x1∧x2′∨0∧x1∧x2=x1′∧x2′∨x1′∧x2∨x1∧x2′ \begin{aligned} f_\mid(x_1,x_2)&=&1\land x'_1\land x'_2\lor 1\land x'_1\land x_2\lor 1\land x_1\land x'_2\lor 0\land x_1\land x_2\\ &=&x'_1\land x'_2\lor x'_1\land x_2\lor x_1\land x'_2 \end{aligned}

従って, 否定論理積の PDNF は x1′∧x2′∨x1′∧x2∨x1∧x2′x'_1\land x'_2\lor x'_1\land x_2\lor x_1\land x'_2 となる. この操作を振り返ると, 真理値表から PDNF を書くためには, 結果が 11 となっている入力変数の全パターンに対して, 元の入力変数の値が 11 ならそのまま, 00 ならその補元をとり, それらすべての和を取ればよいことがわかる. 何故ならば, 結果が 00 となる部分は, シャノンの展開定理の証明でも示したように消えてしまうからである. 同じようにして, 否定論理和, 排他的論理和も真理値表 2 の ↓,⊕\downarrow,\oplus の列をみると, 11 となる入力のパターンから

f↓(x1,x2)=x1′∧x2′f⊕(x1,x2)=x1∧x2′∨x1′∧x2 \begin{aligned} f_{\downarrow}(x_1,x_2)&=&x'_1\land x'_2\\ f_{\oplus}(x_1,x_2)&=&x_1\land x'_2\lor x'_1\land x_2\\ \end{aligned}

となる. すなわち, 真理値表で表現できるブール式は PDNF で表せるということである3.

次に, 任意の論理式から PDNF に変換することを考える. 結論からいうと, 次の手順に従えば PDNF へ機械的に変換できることが知られている.

  1. ブール式全体を基本項による積の和の形にする (分配律等を利用)
  2. 最小項でない基本項に対し, その基本項に含まれないすべてのリテラル xix_i について (xi∧xi′)(x_i\land x'_i) を乗ずる
  3. 分配律等に従い展開して, 冗長な項を除去する

以下, PDNF で表されたブール式を f(x1,x2,⋯ ,xn)PDNFf(x_1,x_2,\cdots,x_n)_{\rm P D N F} と書くこととする. 例えば, ブール式 f(x1,x2)=x1∧x2∧x1∨x2f(x_1,x_2)=x_1\land x_2\land x_1\lor x_2 を PDNF で表すとすると,

f(x1,x2)=x1∧x2∧x1∨x2=x1∧x1∧x2∨x2(∵公理1:可換律)=x1∧x2∨x2(∵定理:べき等律)=x1∧x2∨1∧x2(∵公理3:同一律)=x1∧x2∨(x1∨x1′)∧x2(∵公理4:補元律)=x1∧x2∨x1∧x2∨x1′∧x2(∵公理2:分配律)=x1∧x2∨x1′∧x2(∵定理:べき等律) \begin{aligned} f(x_1,x_2)&=&x_1\land x_2\land x_1\lor x_2\\ &=&x_1\land x_1\land x_2\lor x_2&(\because {\rm\href{#boolean_algebra1}{公理1}: 可換律})\\ &=&x_1\land x_2\lor x_2&(\because {\rm 定理:\href{#idempotence}{べき等律}})\\ &=&x_1\land x_2\lor 1\land x_2&(\because {\rm \href{#boolean_algebra3}{公理 3}:同一律})\\ &=&x_1\land x_2\lor (x_1\lor x_1')\land x_2&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&x_1\land x_2\lor x_1\land x_2\lor x_1'\land x_2&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&x_1\land x_2\lor x_1'\land x_2&(\because {\rm 定理:\href{#idempotence}{べき等律}}) \end{aligned}

従って f(x1,x2)PDNF=x1∧x2∨x1′∧x2f(x_1,x_2)_{\rm P D N F}=x_1\land x_2\lor x_1'\land x_2 となる. 例としてもう 1 つ, f(x1,x2,x3)=x1∧x2′∧x3∨x1∧x3′∨x2∧x3′f(x_1,x_2,x_3)=x_1\land x_2'\land x_3\lor x_1\land x'_3\lor x_2\land x'_3 としたときの PDNF は

f(x1,x2,x3)=x1∧x2′∧x3∨x∧x3′∨x2∧x3′=x1∧x2′∧x3∨x1∧(x2∨x2′)∧x3′∨(x1∨x1′)∧x2∧x3′(∵公理3,公理4:同一律,補元律)=x1∧x2′∧x3∨x1∧x2∧x3′∨x1∧x2′∧x3′∨x1∧x2∧x3′∨x1′∧x2∧x3′(∵公理2:分配律)=x1∧x2′∧x3∨x1∧x2∧x3′∨x1∧x2′∧x3′∨x1′∧x2∧x3′(∵定理:べき等律) \begin{aligned} f(x_1,x_2,x_3)&=&x_1\land x'_2\land x_3\lor x\land x'_3\lor x_2\land x'_3\\ &=&x_1\land x'_2\land x_3\lor x_1\land(x_2\lor x'_2)\land x'_3\lor (x_1\lor x_1')\land x_2\land x'_3&(\because {\rm \href{#boolean_algebra3}{公理 3}, \href{#boolean_algebra4}{公理 4}: 同一律, 補元律} )\\ &=&x_1\land x'_2\land x_3\lor x_1\land x_2\land x'_3\lor x_1\land x'_2\land x'_3\lor x_1\land x_2\land x'_3\lor x'_1\land x_2\land x'_3&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&x_1\land x'_2\land x_3\lor x_1\land x_2\land x'_3\lor x_1\land x'_2\land x'_3\lor x'_1\land x_2\land x'_3&(\because {\rm 定理: \href{#idempotence}{べき等律}}) \end{aligned}

従って f(x1,x2,x3)PDNF=x1∧x2′∧x3∨x1∧x2∧x3′∨x1∧x2′∧x3′∨x1′∧x2∧x3′f(x_1,x_2,x_3)_{\rm P D N F}=x_1\land x'_2\land x_3\lor x_1\land x_2\land x'_3\lor x_1\land x'_2\land x'_3\lor x'_1\land x_2\land x'_3 となる.

乗法標準形, 主乗法標準形

f(x1,x2,⋯ ,xn)f(x_1,x_2,\cdots,x_n) を x1,x2x_1,x_2 についてシャノン双対展開すると,

f(x1,x2,⋯ ,xn)=(x1∨x2∨f(0,0,⋯ ,xn))∧(x1∨x2′∨f(0,1,⋯ ,xn))∧(x1′∨x2∨f(1,0,⋯ ,xn))∧(x1′∨x2′∨f(1,1,⋯ ,xn)) \begin{aligned} f(x_1,x_2,\cdots,x_n)&=&(x_1\lor x_2\lor f(0,0,\cdots,x_n))\\ &&\land (x_1\lor x'_2\lor f(0,1,\cdots,x_n))\\ &&\land (x'_1\lor x_2\lor f(1,0,\cdots,x_n))\\ &&\land (x'_1\lor x'_2\lor f(1,1,\cdots,x_n)) \end{aligned}

となる. 従って, 全入力変数 x1,x2,⋯ ,xnx_1,x_2,\cdots,x_n についてシャノン双対展開すると,

f(x1,x2,⋯ ,xn)=(x1∨x2∨⋯∨xn∨f(0,0,⋯ ,0))∧(x1∨x2∨⋯∨xn′∨f(1,0,⋯ ,0))∧⋯∧(x1′∨x2′∨⋯xn∨f(1,1,⋯ ,0))∧(x1′∨x2′∨⋯xn′∨f(1,1,⋯ ,1)) \begin{aligned} f(x_1,x_2,\cdots,x_n)&=&(x_1\lor x_2\lor\cdots\lor x_n\lor f(0,0,\cdots,0))\\ &&\land(x_1\lor x_2\lor\cdots\lor x'_n\lor f(1,0,\cdots,0))\\ &&\land\cdots\\ &&\land(x'_1\lor x'_2\lor\cdots x_n\lor f(1,1,\cdots,0))\\ &&\land(x'_1\lor x'_2\lor\cdots x'_n\lor f(1,1,\cdots,1)) \end{aligned}

となる (シャノンの定理より数学的帰納法により証明できるが, 省略). これを以下のように定義する.

最大項展開

nn 変数ブール関数 f(x1,x2,⋯ ,xn)f(x_1,x_2,\cdots,x_n) のすべての入力変数 x1,x2,⋯ ,xnx_1,x_2,\cdots,x_n について, シャノン双対展開した形式 f(x1,x2,⋯ ,xn)=⋀(e1,e2,⋯ ,en)∈Bn(f(e1,e2,⋯ ,en)∨⋁i=1nxiei′)(2)f(x_1,x_2,\cdots,x_n)= \bigwedge_{(e_1,e_2,\cdots,e_n)\in B^n}(f(e_1,e_2,\cdots,e_n)\lor\bigvee_{i=1}^{n}x_i^{e'_i})\tag{2} は f(x1,x2,⋯ ,xn)f(x_1,x_2,\cdots,x_n) の最大項展開である. なお, このときの項数は 2n2^n となる.

これを踏まえ, 乗法標準形, 主乗法標準形を導入する.

乗法標準形, 主乗法標準形

  • 乗法標準形 (CNF: conjunctive normal form) は, ブール式のリテラル, または 2 つ以上のリテラルの和の積のことをいう. ここで, 2 つ以上のリテラルの和で同じ入力変数を 2 度以上含まないブール式を基本和, また標準項という. 基本和のうち, すべての入力変数を含むブール式を最大項という. すなわち, 上記最大項展開の ⋁i=1nxiei′\displaystyle\bigvee_{i=1}^{n}x_i^{e'_i} は最大項である.
  • 主乗法標準形 (principal conjunctive normal form: PCNF) は, ブール関数を最大項展開した形式, すなわち最大項展開の形式である.

例えば, 否定論理積 ∣\mid を PCNF で表すとしよう. 否定論理積は 2 項演算子なので, その PCNF は 2 変数ブール関数を最大項展開した形となる.

f(x1,x2)=(x1∨x2∨f(0,0))∧(x1∨x2′∨f(0,1))∧(x1′∨x2∨f(1,0))∧(x1′∨x2′∨f(1,1)) f(x_1,x_2)= (x_1\lor x_2\lor f(0,0))\land (x_1\lor x'_2\lor f(0,1))\land(x'_1\lor x_2\lor f(1,0))\land(x'_1\lor x'_2\lor f(1,1))

2 項演算子 ∣\mid を最大項展開した式 f∣(x1,x2)f_{\mid}(x_1,x_2) は, 真理値表 2 の ∣\mid の列のとおりに f∣(x1,x2)f_{\mid}(x_1,x_2) の値を決めてやればよいので

f∣(x1,x2)=(x1∨x2∨1)∧(x1∨x2′∨1)∧(x1′∨x2∨1)∧(x1′∨x2′∨0)=x1′∨x2′ \begin{aligned} f_{\mid}(x_1,x_2)&=&(x_1\lor x_2\lor 1)\land (x_1\lor x'_2\lor 1)\land(x'_1\lor x_2\lor 1)\land(x'_1\lor x'_2\lor 0)\\ &=&x'_1\lor x'_2 \end{aligned}

従って, 否定論理積の PCNF は x1′∨x2′x'_1\lor x'_2 となる. この操作を振り返ると, 真理値表から PCNF を書くためには, 結果が 00 となっている入力変数の全パターンに対して, 元の入力変数の値が 11 なら補元をとり, 00 ならそのままで和を取り, それらすべての積を取ればよいことがわかる. 何故ならば, 結果が 11 となる部分は, 和の性質, すなわち公理 2: 同一律より消えてしまうからである. 同じようにして, 否定論理和, 排他的論理和も真理値表 2 の ↓,⊕\downarrow,\oplus の列をみると, 00 となる入力のパターンから

f↓(x1,x2)=(x1′∨x2′)∧(x1′∨x2)∧(x1∨x2′)f⊕(x1,x2)=(x1′∨x2′)∧(x1∨y1) \begin{aligned} f_{\downarrow}(x_1,x_2)&=&(x'_1\lor x'_2)\land(x'_1\lor x_2)\land(x_1\lor x'_2)\\ f_{\oplus}(x_1,x_2)&=&(x'_1\lor x'_2)\land(x_1\lor y_1) \end{aligned}

となる. すなわち, 真理値表で表現できるブール式は, PCNF で表せるということである5. 次に, 任意の論理式から PCNF に変換することを考える. 結論からいうと, 次の手順に従えば PCNF へ機械的に変換できることが知られている.

  1. ブール式全体を基本項による和の積の形にする (分配律等を利用)
  2. 最大項でない基本項に対し, その基本項に含まれないすべてのリテラル xix_i について xi∧xi′x_i\land x'_i を乗ずる
  3. 分配律等に従い展開して, 冗長な項を除去する

以下, PCNF で表されたブール式を f(x1,x2,⋯ ,xn)PCNFf(x_1,x_2,\cdots,x_n)_{\rm P C N F} と書くこととする. 例えば, ブール式 f(x1,x2,x3)=x1∧(x2′∧x3)′f(x_1,x_2,x_3)=x_1\land(x'_2\land x_3)' を PCNF で表すとすると,

f(x1,x2,x3)=x1∧(x2′∧x3)′=x1∧(x2∨x3′)(∵定理:ド・モルガンの法則)=(x1∨x2∧x2′)∧(x2∨x3′)(∵公理3:同一律)=(x1∨x2)∧(x1∨x2′)∧(x2∨x3′)(∵公理2:分配律)=(x1∨x2∨x3∧x3′)∧(x1∨x2′∨x3∧x3′)∧(x1∧x1′∨x2∧x3′)(∵公理3:同一律)=(x1∨x2∨x3)∧(x1∨x2∨x3′)∧(x1∨x2′∨x3)∧(x1∨x2′∨x3′)∧(x1∨x2∨x3′)∧(x1′∨x2∨x3′)(∵公理2:分配律)=(x1∨x2∨x3)∧(x1∨x2∨x3′)∧(x1∨x2′∨x3)∧(x1∨x2′∨x3′)∧(x1′∨x2∨x3′)(∵定理:べき等律) \begin{aligned} f(x_1,x_2,x_3)&=&x_1\land(x'_2\land x_3)'\\ &=&x_1\land(x_2\lor x'_3)&(\because {\rm 定理: \href{#de_morgan}{ド・モルガンの法則}})\\ &=&(x_1\lor x_2\land x'_2)\land(x_2\lor x'_3)&(\because {\rm \href{#boolean_algebra3}{公理 3}:同一律})\\ &=&(x_1\lor x_2)\land(x_1\lor x'_2)\land(x_2\lor x'_3)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&(x_1\lor x_2\lor x_3\land x'_3)\land(x_1\lor x'_2\lor x_3\land x'_3)\land(x_1\land x'_1\lor x_2\land x'_3)&(\because {\rm \href{#boolean_algebra3}{公理 3}:同一律})\\ &=&(x_1\lor x_2\lor x_3)\land(x_1\lor x_2\lor x'_3)\land(x_1\lor x'_2\lor x_3)\\ &&\land(x_1\lor x'_2\lor x'_3)\land(x_1\lor x_2\lor x'_3)\land(x'_1\lor x_2\lor x'_3)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&(x_1\lor x_2\lor x_3)\land(x_1\lor x_2\lor x'_3)\land(x_1\lor x'_2\lor x_3)\\ &&\land(x_1\lor x'_2\lor x'_3)\land(x'_1\lor x_2\lor x'_3)&(\because {\rm 定理:\href{#idempotence}{べき等律}}) \end{aligned}

従って f(x1,x2,x3)PCNF=(x1∨x2∨x3)∧(x1∨x2∨x3′)∧(x1∨x2′∨x3)∧(x1∨x2′∨x3′)∧(x1′∨x2∨x3′)f(x_1,x_2,x_3)_{\rm P C N F}=(x_1\lor x_2\lor x_3)\land(x_1\lor x_2\lor x'_3)\land(x_1\lor x'_2\lor x_3)\land(x_1\lor x'_2\lor x'_3)\land(x'_1\lor x_2\lor x'_3)

となる. 例としてもう 1 つ, f(x1,x2,x3)=x1∧x2′∨x2∧x3f(x_1,x_2,x_3)=x_1\land x'_2\lor x_2\land x_3 としたときの PCNF は

f(x1,x2,x3)=x1∧x2′∨x2∧x3=(x1∧x2′∨x2)∧(x1∧x2′∨x3)(∵公理2:分配律)=(x1∨x2)∧(x1∨x3)∧(x2′∨x3)(∵公理4:補元律)=(x1∨x2∨x3∧x3′)∧(x1∨x2∧x2′∨x3)∧(x1∧x1′∨x2′∨x3)(∵公理4:補元律)=(x1∨x2∨x3)∧(x1∨x2∨x3′)∧(x1∨x2′∨x3)∧(x1′∨x2′∨x3)(∵公理2:分配律) \begin{aligned} f(x_1,x_2,x_3)&=&x_1\land x'_2\lor x_2\land x_3\\ &=&(x_1\land x'_2\lor x_2)\land(x_1\land x'_2\lor x_3)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律})\\ &=&(x_1\lor x_2)\land(x_1\lor x_3)\land(x'_2\lor x_3)&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&(x_1\lor x_2\lor x_3\land x'_3)\land(x_1\lor x_2\land x'_2\lor x_3)\land(x_1\land x'_1\lor x'_2\lor x_3)&(\because {\rm \href{#boolean_algebra4}{公理 4}:補元律})\\ &=&(x_1\lor x_2\lor x_3)\land(x_1\lor x_2\lor x'_3)\land(x_1\lor x'_2\lor x_3)\land(x'_1\lor x'_2\lor x_3)&(\because {\rm \href{#boolean_algebra2}{公理 2}:分配律}) \end{aligned}

従って f(x1,x2,x3)PCNF=(x1∨x2∨x3)∧(x1∨x2∨x3′)∧(x1∨x2′∨x3)∧(x1′∨x2′∨x3)f(x_1,x_2,x_3)_{\rm P C N F}=(x_1\lor x_2\lor x_3)\land(x_1\lor x_2\lor x'_3)\land(x_1\lor x'_2\lor x_3)\land(x'_1\lor x'_2\lor x_3) となる.

簡単化

ブール式を簡単化する方法について見ていく.

カルノー図

例えばブール関数が f(x1,x2)=x1∧x2′∨x1′∧x2′∨x1∧x2′∨x1∧x2(3)f(x_1,x_2)=x_1\land x'_2\lor x'_1\land x'_2\lor x_1\land x'_2\lor x_1\land x_2 \tag{3} と与えられたとき, 式変形をしていくと簡単化できることがわかる. 事実, (3)=(x1∨x1′)∧x2′∨x1∧(x2′∨x2)=x2′∨x1(3)=(x_1\lor x'_1)\land x'_2\lor x_1\land(x'_2\lor x_2)=x'_2\lor x_1 である. このような, 公理4: 補元律を用いた式変形は, カルノー図という図式を用いることで視覚的に捉えることができる. カルノー図は, 真理値表を 2 次元的に並べる形をしており, 例えば式 (3)(3) をカルノー図で表すと次のようになる.

カルノー図 1
x1\x2x_1\backslash x_2 00 11
00 11 00
11 11 11

緑色の表示となっているセルの部分それぞれが最小項を表しており, 元の論理関数に含まれる最小項のセルには 11, 含まれないセルには 00 を記述する4ことで上図のようになる. このとき, 緑色の表示となっているセルの部分の個数は 2n2^n である. これらをまとめることが, 冗長な変数の削除に対応するのである. カルノー図をみて 11 となるセルの和を書き下すことは, PDNF を書くことと同値である式 ((3)(3) は元から PDNF である. カルノー図 1 から結果として, これが導出できる).

カルノー図の隣接するセルの間では, 全ての変数のうちのどれか 1 つの 11 か 00 が変わった結果となっているので, 公理4: 補元律を利用してまとめることができるのである. 従って, 隣接する 11 のセルをグループ化し, 公理4: 補元律を利用することで簡単化が実現できる.

以下, ii 行目 jj 列目のセルを i:ji:j と示すこととする. 例えば, カルノー図 1 で 11 となるセルは 1:1,2:1,2:21:1,2:1,2:2 で, これらはそれぞれ x1′∧x2′,x1∧x2′,x1∧x2x'_1\land x'_2,x_1\land x'_2,x_1\land x_2 である. ここで, 任意の隣接するセル cic_i をグループ化したことを c1,c2,⋯ ,cn{c_1,c_2,\cdots,c_n} と書くとき, g1=1:1,2:1,g2=2:1,2:2g_1={1:1,2:1}, g_2={2:1,2:2} とグループ化できることがわかる. 従って, それぞれを論理式で基本積の形に表すと,

g1=x1′∧x2′∨x1∧x2′=(x1′∨x1)∧x2′=x2′g2=x1∧x2′∨x1∧x2=x1∧(x2′∨x2)=x1 \begin{aligned} g_1&=&x'_1\land x'_2\lor x_1\land x'_2&=&(x'_1\lor x_1)\land x'_2&=&x'_2\\ g_2&=&x_1\land x'_2\lor x_1\land x_2&=&x_1\land(x'_2\lor x_2)&=&x_1 \end{aligned}

よって, =x2′∨x1=x'_2\lor x_1 とわかる. 別のカルノー図についてもやってみよう.

カルノー図 2
x1x2\x3x4x_1x_2\backslash x_3x_4 0000 0101 1111 1010
0000 00 11 11 00
0101 00 11 00 00
1111 00 00 00 00
1010 11 00 11 11

これは, 4 つの引数をもったブール関数のカルノー図である. カルノー図では, 最上, 最下また最左, 最右のセルは隣接していると考える. 従って, カルノー図 2 におけるグループ化の一つの例として g1=1:2,2:2,g2=1:3,4:3,g3=4:1,4:4g_1={1:2,2:2},g_2={1:3,4:3},g_3={4:1,4:4} と構成できる. よって,

g1=x1′∧x2′∧x3′∧x4∨x1′∧x2∧x3′∧x4=x1′∧x3′∧x4g2=x1′∧x2′∧x3∧x4∨x1∧x2′∧x3∧x4=x2′∧x3∧x4g3=x1∧x2′∧x3′∧x4′∨x1∧x2′∧x3∧x4′=x1∧x2′∧x4′\begin{aligned} g_1&=&x'_1\land x'_2\land x'_3\land x_4\lor x'_1\land x_2\land x'_3\land x_4&=&x'_1\land x'_3\land x_4\\ g_2&=&x'_1\land x'_2\land x_3\land x_4\lor x_1\land x'_2\land x_3\land x_4&=&x'_2\land x_3\land x_4\\ g_3&=&x_1\land x'_2\land x'_3\land x'_4\lor x_1\land x'_2\land x_3\land x'_4&=&x_1\land x'_2\land x'_4 \end{aligned}

ゆえにカルノー図 2 で示される論理関数の簡単な表現は

x1′∧x3′∧x4∨x2′∧x3∧x4∨x1∧x2′∧x4′x'_1\land x'_3\land x_4\lor x'_2\land x_3\land x_4\lor x_1\land x'_2\land x'_4

となる. このグループ化という操作が一意ではないことからわかるように, 簡単化したブール式も一意でないことがわかる. 例えば, g1=1:2,2:2,g2=1:2,1:3,g3=4:1,4:4,g4=4:3,4:4g_1={1:2,2:2},g_2={1:2,1:3},g_3={4:1,4:4},g_4={4:3,4:4} とグループ化すると,

g1=x1′∧x2′∧x3′∧x4∨x1′∧x2∧x3′∧x4=x1′∧x3′∧x4g2=x1′∧x2′∧x3′∧x4∨x1′∧x2′∧x3∧x4=x1′∧x2′∧x4g3=x1∧x2′∧x3′∧x4′∨x1∧x2′∧x3∧x4′=x1∧x2′∧x4′g4=x1∧x2′∧x3∧x4∨x1∧x2′∧x3∧x4′=x1∧x2′∧x3\begin{aligned} g_1&=&x'_1\land x'_2\land x'_3\land x_4\lor x'_1\land x_2\land x'_3\land x_4&=&x'_1\land x'_3\land x_4\\ g_2&=&x'_1\land x'_2\land x'_3\land x_4\lor x'_1\land x'_2\land x_3\land x_4&=&x'_1\land x'_2\land x_4\\ g_3&=&x_1\land x'_2\land x'_3\land x'_4\lor x_1\land x'_2\land x_3\land x'_4&=&x_1\land x'_2\land x'_4\\ g_4&=&x_1\land x'_2\land x_3\land x_4\lor x_1\land x'_2\land x_3\land x'_4&=&x_1\land x'_2\land x_3 \end{aligned}

ゆえに,

x1′∧x3′∧x4∨x1′∧x2′∧x4∨x1∧x2′∧x4′∨x1∧x2′∧x3x'_1\land x'_3\land x_4\lor x'_1\land x'_2\land x_4\lor x_1\land x'_2\land x'_4\lor x_1\land x'_2\land x_3

となる. 1 つの例を見ただけなので, 厳密に言えたことではないが, 一般的にグループの数が少なく, かつグループ内のセルの数を(2n2n 個で)なるべく多く取る方がより簡単な論理式を構成できることがわかる.

さて, ある論理変数の組み合わせが予め起こりえないことがわかっていたとき, その場合もカルノー図を用いて簡単化を進めることができる. このような組み合わせに対する最小項を禁止項, または don’t care 項という. 例えば, f(x1,x2,x3,x4)=x1′∧x2′∧x3′∧x4∨x1′∧x2∧x3′∧x4∨x1′∧x2∧x3∧x4∨x1′∧x2∧x3∧x4′∨x1∧x2′∧x3∧x4∨x1∧x2′∧x3∧x4′(4)\begin{aligned} f(x_1,x_2,x_3,x_4)&=&x'_1\land x'_2\land x'_3\land x_4 \\ &&\lor x'_1\land x_2\land x'_3\land x_4 \\ &&\lor x'_1\land x_2\land x_3\land x_4\\ &&\lor x'_1\land x_2\land x_3\land x'_4\\ &&\lor x_1\land x'_2\land x_3\land x_4\\ &&\lor x_1\land x'_2\land x_3\land x'_4\tag{\htmlId{formula4}{4}} \end{aligned}

というブール関数を簡単化することを考える. このとき, x1∧x2x_1\land x_2, また x1∧x2′∧x3′∧x4′x_1\land x'_2\land x'_3\land x'_4 は禁止項とする. 禁止行の対応するセルには ϕ\phi を記述する. すると, 式 (4)(4) のカルノー図は次のとおりとなる.

カルノー図 3
x1x2\x3x4x_1x_2\backslash x_3x_4 0000 0101 1111 1010
0000 00 11 00 00
0101 00 11 11 11
1111 ϕ\phi ϕ\phi ϕ\phi ϕ\phi
1010 ϕ\phi 00 11 11

禁止項は, 11 でも 00 でもよいということになるので, グループを構成するにあたって自分で都合よく 11 か 00 に解釈してしまって良い. できる限り多くのセルと少ないグループの数で構成するために, いま 3:3,3:43:3,3:4 を 11 と解釈すれば, g1=1:2,2:2,g2=2:3,2:4,3:3,3:4,g3=3:3,3:4,4:3,4:4g_1={1:2,2:2},g_2={2:3,2:4,3:3,3:4},g_3={3:3,3:4,4:3,4:4} とグループ化できる. 従って,

g1=x1′∧x2′∧x3′∧x4∨x1′∧x2∧x3′∧x4=x1′∧x3′∧x4g2=x1′∧x2∧x3∧x4∨x1′∧x2∧x3∧x4′∨x1∧x2∧x3∧x4∨x1∧x2∧x3∧x4′=x2∧x3g3=x1∧x2∧x3∧x4∨x1∧x2∧x3∧x4′∨x1∧x2′∧x3∧x4∨x1∧x2′∧x3∧x4′=x1∧x3 \begin{aligned} g_1&=&x'_1\land x'_2\land x'_3\land x_4\lor x'_1\land x_2\land x'_3\land x_4&=&x'_1\land x'_3\land x_4\\ g_2&=&x'_1\land x_2\land x_3\land x_4\lor x'_1\land x_2\land x_3\land x'_4\lor x_1\land x_2 \land x_3\land x_4\lor x_1\land x_2\land x_3\land x'_4&=&x_2\land x_3\\ g_3&=&x_1\land x_2\land x_3\land x_4\lor x_1\land x_2\land x_3\land x'_4\lor x_1\land x'_2\land x_3\land x_4\lor x_1\land x'_2\land x_3\land x'_4&=&x_1\land x_3 \end{aligned}

ゆえに, 式 (4)\href{#formula4}{(4)} は

f(x1,x2,x3,x4)=x1′∧x3′∧x4∨x2∧x3∨x1∧x3f(x_1,x_2,x_3,x_4)=x'_1\land x'_3\land x_4\lor x_2\land x_3\lor x_1\land x_3

と簡単化できた. カルノー図は, 1 次元につき 2 つまでの引数を扱えると考えると, 人間の次元認識能力の見地から実質 6 つの引数にまで対応できることとなるわけだが, 実際は平面的に考えることが多いので, 大抵, 最大 4 個の引数までしか扱うことができない.

クワイン・マクラスキー法

主にクワイン・マクラスキー法は x∧y∨x∧y′=x∧(y∨y′)=x(5)x\land y\lor x\land y'=x\land(y\lor y')=x\tag{\htmlId{formula5}{5}} を繰り返し利用し, ブール関数を機械的に簡単化していく方法であり, その手順は次のとおりである.

  1. ブール式を PDNF にする
  2. 式 (5)\href{#formula5}{(5)} を利用して圧縮し, 主項を求める
    1. ブール式を 2 進値に割り当てる5
    2. ハミング距離 1 のビット列同士を可能な限り繰り返し組み合わせる
  3. 求めた主項からただ 1 つの最小項を包含する主項(必須項)を求める.
  4. ブール関数を作成する
    1. 必須項の和をとる
    2. 必須項により包含されていない最小項があるとき, 最も簡単な主項を選択し和を取る.

いま, 式 (4)\href{#formula4}{(4)} を簡単化することを考えるとしよう. このとき, まず式を PDNF にする. (4)(4) はすでに PDNF の形式となっているので, 今回は必要ない. 次に, カルノー図 3 の各セル i:ji:j を m0=1:1,m1=2:1,m2=3:1,m3=4:1,m4=1:2,⋯ ,m15=4:4m_0=1:1,m_1=2:1,m_2=3:1,m_3=4:1,m_4=1:2,\cdots,m_{15}=4:4 とおき, PDNF を構成する各最小項について次のようにビット列と対応させる.

m4=x1′∧x2′∧x3′∧x4=0001m5=x1′∧x2∧x3′∧x4=0101m9=x1′∧x2∧x3∧x4=0111m11=x1∧x2′∧x3∧x4=1011m13=x1′∧x2∧x3∧x4′=0110m15=x1∧x2′∧x3∧x4′=1010\begin{aligned} m_4&=&x'_1\land x'_2\land x'_3\land x_4=0001\\ m_5&=&x'_1\land x_2\land x'_3\land x_4=0101\\ m_9&=&x'_1\land x_2\land x_3\land x_4=0111\\ m_{11}&=&x_1\land x'_2\land x_3\land x_4=1011\\ m_{13}&=&x'_1\land x_2\land x_3\land x'_4=0110\\ m_{15}&=&x_1\land x'_2\land x_3\land x'_4=1010 \end{aligned}

ここで, 先と同様, x1∧x2x_1\land x_2 と x1∧x2′∧x3′∧x4′x_1\land x'_2\land x'_3\land x'_4 を禁止項としたときは, それについてもビット列と対応させておく.

m2=x1∧x2∧x3′∧x4′=1100m3=x1∧x2′∧x3′∧x4′=1000m6=x1∧x2∧x3′∧x4=1101m10=x1∧x2∧x3∧x4=1111m14=x1∧x2∧x3∧x4′=1110\begin{aligned} m_2&=&x_1\land x_2\land x'_3\land x'_4=1100\\ m_3&=&x_1\land x'_2\land x'_3\land x'_4=1000\\ m_6&=&x_1\land x_2\land x'_3\land x_4=1101\\ m_{10}&=&x_1\land x_2\land x_3\land x_4=1111\\ m_{14}&=&x_1\land x_2\land x_3\land x'_4=1110 \end{aligned}

これは ⋁m(4,5,9,11,13,15)+dc(2,3,6,10,14)=(4)\displaystyle\bigvee {\rm m}(4,5,9,11,13,15)+{\rm dc}(2,3,6,10,14)=(4) と書かれる. このとき, 例えば m4∨m5m_4\lor m_5 は式 (5)(5) を利用して簡単化できることがわかる. 事実, x1′∧x2′∧x3′∧x4∨x1′∧x2∧x3′∧x4=x1′∧x3′∧x4∧(x2′∨x2)=x1′∧x3′∧x4x'_1\land x'_2\land x'_3\land x_4\lor x'_1\land x_2\land x'_3\land x_4=x'_1\land x'_3\land x_4\land(x'_2\lor x_2)=x'_1\land x'_3\land x_4 である. このような簡単化をすべての可能な組み合わせについて繰り返し実行する. この作業を圧縮ということとする. 先にブール式をビット列と対応させたので, 圧縮とはハミング距離 1 のビット列同士を繰り返し組み合わせることと同値である. 次の表に, 圧縮を 1 度行った結果を示す. 組み合わせられたビット部分は −-, それ以上圧縮できないものを主項といい, ∗\ast で示すものとする6. これを圧縮表ということとする.

1 の数 最小項 ビット列表現
圧縮表 (1 回目)
11 m4,5m_{4,5} 0−01∗0-01\ast
m3,15m_{3,15} 10−010-0
m2,3m_{2,3} 1−001-00
22 m5,9m_{5,9} 01−101-1
m5,6m_{5,6} −101-101
m9,13m_{9,13} 011−011-
m13,14m_{13,14} −110-110
m14,15m_{14,15} 1−101-10
m11,15m_{11,15} 101−101-
m2,6m_{2,6} 110−110-
m2,14m_{2,14} 11−011-0
33 m9,10m_{9,10} −111-111
m10,11m_{10,11} 1−111-11
m6,10m_{6,10} 11−111-1
m10,14m_{10,14} 111−111-

残りのすべての最小項について ∗\ast がつくまで繰り返す.

1 の数 最小項 ビット列表現
圧縮表 (2 回目)
11 m2,3,14,15m_{2,3,14,15} 1−−0∗1--0\ast
22 m5,6,9,10m_{5,6,9,10} −1−1∗-1-1\ast
m9,10,13,14m_{9,10,13,14} −11−∗-11-\ast
m10,11,14,15m_{10,11,14,15} 1−1−∗1-1-\ast
m2,6,10,14m_{2,6,10,14} 11−−∗11--\ast

従って, 主項は m4,5,m2,3,14,15,m5,6,9,10,m9,10,13,14,m10,11,14,15,m2,6,10,14m_{4,5},m_{2,3,14,15},m_{5,6,9,10},m_{9,10,13,14},m_{10,11,14,15},m_{2,6,10,14} であるから, 圧縮表 1 および 2 より, 式 \(\) は次のように表現できることがわかる.

x1′∧x3′∧x4⏟m4,5∨x1∧x4′⏟m2,3,14,15∨x2∧x4⏟m5,6,9,10∨x2∧x3⏟m9,10,13,14∨x1∧x3⏟m10,11,14,15∨x1∧x2⏟m2,6,10,14\underbrace{x'_1\land x'_3\land x_4}_{m_{4,5}}\lor \underbrace{x_1\land x'_4}_{m_{2,3,14,15}}\lor\underbrace{x_2\land x_4}_{m_{5,6,9,10}}\lor\underbrace{x_2\land x_3}_{m_{9,10,13,14}}\lor\underbrace{x_1\land x_3}_{m_{10,11,14,15}}\lor \underbrace{x_1\land x_2}_{m_{2,6,10,14}}

しかしこれはまだ冗長である. この主項から必須項を調べる. 縦軸に主項, 横軸に最小項を並べ, 最小項を包含する主項のセルに印 ◯\bigcirc を, 包含する最小項が 1 つしかない主項のセルに印 ⊚\circledcirc をつける. これを主項表という.

主項表 1
主項 \\backslash 最小項 m4m_4 m5m_5 m9m_9 m13m_{13} m11m_{11} m15m_{15} ビット表現
m4,5m_{4,5} ⊚\color{blue}{\circledcirc} ◯\color{blue}{\bigcirc} 0−010-01
m5,6,9,10m_{5,6,9,10} ◯\bigcirc ◯\bigcirc −1−1-1-1
m9,10,13,14m_{9,10,13,14} ◯\color{blue}{\bigcirc} ⊚\color{blue}{\circledcirc} −11−-11-
m10,11,14,15m_{10,11,14,15} ⊚\color{blue}{\circledcirc} ◯\color{blue}{\bigcirc} 1−1−1-1-
m2,3,14,15m_{2,3,14,15} ◯\bigcirc 1−−01--0
m2,6,10,14m_{2,6,10,14} 11−−11--

従って, 必須項は ⊚\circledcirc のつく m4,5,m9,10,13,14,m10,11,14,15m_{4,5},m_{9,10,13,14},m_{10,11,14,15} である. あとはそれらを書き出し, 残りの主項で最小項を全て含む最も簡単な組み合わせを探すこととなる(ここで現れる必須項が全ての最小項を包含するとは限らない). ここで, もし ⊚\circledcirc が 1 つも含まれない最小項があれば, すなわち必須項にすべての最小項が含まれていなければ, 最も簡単となりかつ, 全ての最小項を含むブール式となるよう適当な主項を選択する. 今回の場合では, 必須項のみで全ての最小項を包含することができている(印を青の表示としておいた)から m4,5,m9,10,13,14,m10,11,14,15m_{4,5},m_{9,10,13,14},m_{10,11,14,15} の和, すなわち x1′∧x3′∧x4∨x2∧x3∨x1∧x3x'_1\land x'_3\land x_4\lor x_2\land x_3\lor x_1\land x_3 が式 (4)(4) の最簡形である. 先に示したカルノー図による簡単化で得られたブール式と同等の結果が得られたことがわかる. なお, クワイン・マクラスキー法は NP 完全である7ため, 使用範囲が限られる.

ペトリック法

先のクワイン・マクラスキー法の最後では, 「最も簡単となりかつ, 全ての最小項を含むブール式となるよう適当な主項を選択」することによって最簡形を得るとのことであったが, この部分をペトリック法で置き換えることにより, 機械的に最簡形のブール式を決定することができる. ここでも, (4)(4) を例に方法を示すこととする. クワイン・マクラスキー法の手順のうち 3 まで実行したものとし, 主項表 1 が得られたとしよう. まず主項表 1 の列を見て, 印のある主項らで和を取り, それらの積をとった次の式を得る.

m4,5∧(m4,5∨m5,6,9,10)∧(m5,6,9,10∨m9,10,13,14)∧m9,10,13,14∧m10,11,14,15∧(m10,11,14,15∨m2,3,14,15)(6)m_{4,5}\land (m_{4,5}\lor m_{5,6,9,10})\land(m_{5,6,9,10}\lor m_{9,10,13,14})\land m_{9,10,13,14}\land m_{10,11,14,15}\land(m_{10,11,14,15}\lor m_{2,3,14,15})\tag{6}

式 (6)(6) を公理2: 分配律および吸収律を用いて変形していくと,

(6)=(m4,5∨m4,5∧m5,6,9,10)∧(m5,6,9,10∧m9,10,13,14∨m9,10,13,14)∧(m10,11,14,15∨m10,11,14,15∧m2,3,14,15)=m4,5∧m9,10,13,14∧m10,11,14,15 \begin{aligned} (6)&=&(m_{4,5}\lor m_{4,5}\land m_{5,6,9,10})\land(m_{5,6,9,10}\land m_{9,10,13,14}\lor m_{9,10,13,14})\land(m_{10,11,14,15}\lor m_{10,11,14,15}\land m_{2,3,14,15})\\ &=&m_{4,5}\land m_{9,10,13,14}\land m_{10,11,14,15} \end{aligned}

この主項の積となっている部分を主項の和とすることで, ブール関数の最簡形が求まる. 従って, 先と同様の結果が機械的に得られたことがわかる.

クワイン・マクラスキー法, ペトリック法の実装

これらは一度プログラムで実装することが割と学習の定番となっているので, Haskell で実装した. 次のリポジトリにて管理している.

falgon/bsimplified - The simple and pure implementation of Quine-McCluskey method, Petrick’s method and parsing of Boolean formula

まず, いま解いた簡単化を再度実行してみる. よくある実装法だと思うが, クワイン・マクラスキー法の圧縮過程は二分木のデータ構造として表現する. 従って, まずはじめに各最小項に対応するノードを作成することで PDNF を表現することとした.

Prelude> :m +BSimplified.QMM Data.Maybe
Prelude BSimplified.QMM Data.Maybe> let tr = fromJust $ pdnfForest (fromJust $ strBitsList ["0001","0101","0111","1011","0110","1010","1100","1000","1101","1111","1110"]) (replicate 6 False ++ replicate 5 True)
Prelude BSimplified.QMM Data.Maybe> tr
[CTNode {row = TruthTableRow { var = 1 (binary), dontcare = False }, mergedFlag = -1, identifier = 18370878410602274422, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 101 (binary), dontcare = False }, mergedFlag = -1, identifier = 17795521015237778886, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = -1, identifier = 9505003458451781531, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 1011 (binary), dontcare = False }, mergedFlag = -1, identifier = 5344459161969259783, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 110 (binary), dontcare = False }, mergedFlag = -1, identifier = 2509103263232437805, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 1010 (binary), dontcare = False }, mergedFlag = -1, identifier = 9465362842462816922, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 1100 (binary), dontcare = True }, mergedFlag = -1, identifier = 5080631804786515567, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 1000 (binary), dontcare = True }, mergedFlag = -1, identifier = 8905849755465195471, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 1101 (binary), dontcare = True }, mergedFlag = -1, identifier = 7582384624143865392, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 1111 (binary), dontcare = True }, mergedFlag = -1, identifier = 4819471800686604738, prevLeft = CTEmpty, prevRight = CTEmpty},CTNode {row = TruthTableRow { var = 1110 (binary), dontcare = True }, mergedFlag = -1, identifier = 8582731269452337816, prevLeft = CTEmpty, prevRight = CTEmpty}]

pdnfForest には QMyBits のインスタンス (DigitListBits, StrBits, RawBits) のリストと Don’t care か否かを制御するフラグのリストを渡す. このとき, 2 つのリストの要素数は同一でなければならない (もしそうでなければ Nothing が返る). ここで, DigitListBits, StrBits, RawBits はそれぞれビット列の表現を包括的に捉えるための型である.

Prelude BSimplified.QMM Data.Maybe> :m +BSimplified.Bits
Prelude BSimplified.QMM Data.Maybe BSimplified.Bits> toRawBits (StrBits "1010") == toRawBits (RawBits 10)
True
Prelude BSimplified.QMM Data.Maybe BSimplified.Bits> toRawBits (StrBits "1010") == toRawBits (DigitListBits [1,0,1,0])
True

クワイン・マクラスキー法によって圧縮を実行する.

Prelude BSimplified.QMM Data.Maybe BSimplified.Bits> quineMcCluskey tr
PrimeImplicants [CTNode {row = TruthTableRow { var = 1 (binary), dontcare = False }, mergedFlag = 2, identifier = 577617992350188464, prevLeft = CTNode {row = TruthTableRow { var = 1 (binary), dontcare = False }, mergedFlag = -1, identifier = 18370878410602274422, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 101 (binary), dontcare = False }, mergedFlag = -1, identifier = 17795521015237778886, prevLeft = CTEmpty, prevRight = CTEmpty}},CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 2, identifier = 6829379978376433071, prevLeft = CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 1, identifier = 8439440437090953821, prevLeft = CTNode {row = TruthTableRow { var = 101 (binary), dontcare = False }, mergedFlag = -1, identifier = 17795521015237778886, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = -1, identifier = 9505003458451781531, prevLeft = CTEmpty, prevRight = CTEmpty}}, prevRight = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = 1, identifier = 3159344086055741426, prevLeft = CTNode {row = TruthTableRow { var = 1101 (binary), dontcare = True }, mergedFlag = -1, identifier = 7582384624143865392, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1111 (binary), dontcare = True }, mergedFlag = -1, identifier = 4819471800686604738, prevLeft = CTEmpty, prevRight = CTEmpty}}},CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 2, identifier = 10719524625750522604, prevLeft = CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 0, identifier = 11617789877111658934, prevLeft = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = -1, identifier = 9505003458451781531, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 110 (binary), dontcare = False }, mergedFlag = -1, identifier = 2509103263232437805, prevLeft = CTEmpty, prevRight = CTEmpty}}, prevRight = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = 0, identifier = 3889360259696288602, prevLeft = CTNode {row = TruthTableRow { var = 1111 (binary), dontcare = True }, mergedFlag = -1, identifier = 4819471800686604738, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1110 (binary), dontcare = True }, mergedFlag = -1, identifier = 8582731269452337816, prevLeft = CTEmpty, prevRight = CTEmpty}}},CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 1, identifier = 18197116026168548551, prevLeft = CTNode {row = TruthTableRow { var = 101 (binary), dontcare = False }, mergedFlag = 0, identifier = 14515361159708671901, prevLeft = CTNode {row = TruthTableRow { var = 1011 (binary), dontcare = False }, mergedFlag = -1, identifier = 5344459161969259783, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1010 (binary), dontcare = False }, mergedFlag = -1, identifier = 9465362842462816922, prevLeft = CTEmpty, prevRight = CTEmpty}}, prevRight = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = 0, identifier = 3889360259696288602, prevLeft = CTNode {row = TruthTableRow { var = 1111 (binary), dontcare = True }, mergedFlag = -1, identifier = 4819471800686604738, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1110 (binary), dontcare = True }, mergedFlag = -1, identifier = 8582731269452337816, prevLeft = CTEmpty, prevRight = CTEmpty}}},CTNode {row = TruthTableRow { var = 10 (binary), dontcare = False }, mergedFlag = 1, identifier = 14507692373987760546, prevLeft = CTNode {row = TruthTableRow { var = 100 (binary), dontcare = False }, mergedFlag = 1, identifier = 17927799263722280277, prevLeft = CTNode {row = TruthTableRow { var = 1010 (binary), dontcare = False }, mergedFlag = -1, identifier = 9465362842462816922, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1000 (binary), dontcare = True }, mergedFlag = -1, identifier = 8905849755465195471, prevLeft = CTEmpty, prevRight = CTEmpty}}, prevRight = CTNode {row = TruthTableRow { var = 110 (binary), dontcare = False }, mergedFlag = 1, identifier = 3574163930668469495, prevLeft = CTNode {row = TruthTableRow { var = 1100 (binary), dontcare = True }, mergedFlag = -1, identifier = 5080631804786515567, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1110 (binary), dontcare = True }, mergedFlag = -1, identifier = 8582731269452337816, prevLeft = CTEmpty, prevRight = CTEmpty}}},CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 0, identifier = 1892010599057419013, prevLeft = CTNode {row = TruthTableRow { var = 110 (binary), dontcare = False }, mergedFlag = 0, identifier = 3438512683213686879, prevLeft = CTNode {row = TruthTableRow { var = 1100 (binary), dontcare = True }, mergedFlag = -1, identifier = 5080631804786515567, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1101 (binary), dontcare = True }, mergedFlag = -1, identifier = 7582384624143865392, prevLeft = CTEmpty, prevRight = CTEmpty}}, prevRight = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = 0, identifier = 3889360259696288602, prevLeft = CTNode {row = TruthTableRow { var = 1111 (binary), dontcare = True }, mergedFlag = -1, identifier = 4819471800686604738, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1110 (binary), dontcare = True }, mergedFlag = -1, identifier = 8582731269452337816, prevLeft = CTEmpty, prevRight = CTEmpty}}}]

実際の計算ではこれで十分なのだが, 一応人間にとってより分かりやすい traceQuineMcCluskey を用意してある. 引数には, pdnfForest で作成したノードのリストと, それに対応する変数名のリストを渡す. 両者の要素数は同一でなければならない (もしそうでない場合 Nothing が返る). ここでは, 先に扱った例題に対応した変数名を渡しているので, 得られた主項が先と同一であることが確認できる.

Prelude BSimplified.QMM Data.Maybe BSimplified.Bits> :m +Control.Monad
Prelude BSimplified.QMM Data.Maybe BSimplified.Bits Control.Monad> void $ traceQuineMcCluskey tr ["m_4","m_5","m_9","m_11","m_13","m_15","m_2","m_3","m_6","m_10","m_14"]
The state of compression #1: ["m_4 m_5","m_5 m_9","m_5 m_6","m_9 m_13","m_9 m_10","m_11 m_15","m_11 m_10","m_13 m_14","m_15 m_3","m_15 m_14","m_2 m_3","m_2 m_6","m_2 m_14","m_6 m_10","m_10 m_14"]
Found prime implicants: ["m_4 m_5"]
The state of compression #2: ["m_5 m_9 m_6 m_10","m_9 m_13 m_10 m_14","m_11 m_15 m_10 m_14","m_15 m_3 m_2 m_14","m_2 m_6 m_10 m_14"]
Found prime implicants: ["m_5 m_9 m_6 m_10","m_9 m_13 m_10 m_14","m_11 m_15 m_10 m_14","m_15 m_3 m_2 m_14","m_2 m_6 m_10 m_14"]

簡単化された最低限の項を得るには minTerms 等を用いる. これも, 変数名と対応した結果を得ることのできる minTermsStr を用意してある.

Prelude BSimplified.QMM Data.Maybe BSimplified.Bits Control.Monad> minTerms tr
[CTNode {row = TruthTableRow { var = 1 (binary), dontcare = False }, mergedFlag = 2, identifier = 577617992350188464, prevLeft = CTNode {row = TruthTableRow { var = 1 (binary), dontcare = False }, mergedFlag = -1, identifier = 18370878410602274422, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 101 (binary), dontcare = False }, mergedFlag = -1, identifier = 17795521015237778886, prevLeft = CTEmpty, prevRight = CTEmpty}},CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 2, identifier = 10719524625750522604, prevLeft = CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 0, identifier = 11617789877111658934, prevLeft = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = -1, identifier = 9505003458451781531, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 110 (binary), dontcare = False }, mergedFlag = -1, identifier = 2509103263232437805, prevLeft = CTEmpty, prevRight = CTEmpty}}, prevRight = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = 0, identifier = 3889360259696288602, prevLeft = CTNode {row = TruthTableRow { var = 1111 (binary), dontcare = True }, mergedFlag = -1, identifier = 4819471800686604738, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1110 (binary), dontcare = True }, mergedFlag = -1, identifier = 8582731269452337816, prevLeft = CTEmpty, prevRight = CTEmpty}}},CTNode {row = TruthTableRow { var = 11 (binary), dontcare = False }, mergedFlag = 1, identifier = 18197116026168548551, prevLeft = CTNode {row = TruthTableRow { var = 101 (binary), dontcare = False }, mergedFlag = 0, identifier = 14515361159708671901, prevLeft = CTNode {row = TruthTableRow { var = 1011 (binary), dontcare = False }, mergedFlag = -1, identifier = 5344459161969259783, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1010 (binary), dontcare = False }, mergedFlag = -1, identifier = 9465362842462816922, prevLeft = CTEmpty, prevRight = CTEmpty}}, prevRight = CTNode {row = TruthTableRow { var = 111 (binary), dontcare = False }, mergedFlag = 0, identifier = 3889360259696288602, prevLeft = CTNode {row = TruthTableRow { var = 1111 (binary), dontcare = True }, mergedFlag = -1, identifier = 4819471800686604738, prevLeft = CTEmpty, prevRight = CTEmpty}, prevRight = CTNode {row = TruthTableRow { var = 1110 (binary), dontcare = True }, mergedFlag = -1, identifier = 8582731269452337816, prevLeft = CTEmpty, prevRight = CTEmpty}}}]
Prelude BSimplified.QMM Data.Maybe BSimplified.Bits Control.Monad> minTermsStr tr ["m_4","m_5","m_9","m_11","m_13","m_15","m_2","m_3","m
_6","m_10","m_14"]
Just [["m_4","m_5"],["m_9","m_13","m_10","m_14"],["m_11","m_15","m_10","m_14"]]

また, ブール式を入力して, 最も簡単な式となる項を見つけられるようにもしてある. ブール式の表記としては, 後述の記号 (否定: ~, 積: *, 和: +, 括弧: (,)) を用いることができる. アルファベット 1 文字は変数名として捉える. ここでは, 例として式 (3)(3) を入力として与える.

$ stack build
$ stack exec bsimplified -- "A*~B+~A*~B+A*~B+A*B"
Minterms (Truth patterns):
        m_0 = { A = True, B = True }
        m_1 = { A = True, B = False }
        m_3 = { A = False, B = False }
The state of compression #1: ["m_0 m_1","m_1 m_3"]
Found prime implicants: ["m_0 m_1","m_1 m_3"]
Simplified terms: (m_0 m_1), (m_1 m_3)

m0,1,m1,3m_{0,1},m_{1,3} が結果として得られた. それぞれ, ビット列上の圧縮された部分を −- で表記すると, m0,1=1−,m1,3=−0m_{0,1}=1-, m_{1,3}=-0 である. これはつまり AB′A B' なので, 従って最簡形は A∨B′A\lor B' である. 当然ながら, 先に求めた解と同じ結果が得られたことが確認できる. 実装については普通に字句解析, 再起下降で計算, 真理値表を構成して PDNF をつくっている. ところで, この最簡形を得るという問題は充足可能性問題であり NP 困難8なので, 変数の多いブール関数に対する最簡形を得ることは難しい. その場合, 現実的な時間で比較的良質な解が得られるヒューリスティックを含む方法で求めることとなる.

ブール代数の例

ここではブール代数の一例として, 計算機科学で一般的に用いられるブール代数を挙げる. 集合 L=0,1L={0,1} に対して ∧\land を積 ⋅:L×L→L\cdot:L\times L\to L, ∨\lor を和 +:L×L→L+:L\times L\to L, 補元 x′x' を否定 x‾\overline{x} とおく. 各演算子は, 次の真理値表 1 に従う (y‾\overline{y} は x‾\overline{x} と同様なので省略).

真理値表1\htmlId{truthtable1}{\rm 真理値表 1}
xx yy x‾\overline{x} x⋅yx\cdot y x+yx+y
11 11 00 11 11
11 00 00 00 11
00 11 11 00 11
00 00 11 00 00

これは紛れもなくブール代数である. この形式の下で書かれる式は一般に論理式, 演算子は論理記号といわれる. 計算機科学の分野において, ブール代数は排他的論理和: ⊕\oplus, 否定論理積: ∣\mid, 否定論理和: ↓\downarrow といった記号らをも含めて論理記号として扱うことが多い. これらの真理値表は x,y∈Lx,y\in L に対して次の通りである.

真理値表2\htmlId{truthtable2}{\rm 真理値表 2}
xx yy x∣yx\mid y x↓yx\downarrow y x⊕yx\oplus y
11 11 00 00 00
11 00 11 00 11
00 11 11 00 11
00 00 11 11 00

とくに, 否定論理積 ∣\mid はそれ一つで積, 和, 否定が定義できるため, 他の論理記号よりも特別視されるような場合のある結合子である. これは, シェファーの棒記号といわれ, 真理値表をみるとわかるように (x∧y)‾\overline{(x\land y)}, また x‾∨y‾\overline{x}\lor \overline{y} と同値である. この否定論理積を使って, x‾:=x∣x\overline{x}:=x\mid x と否定が定義できる. この否定を使って, x∧y:=(x∣y)‾x\land y:=\overline{(x\mid y)} と積が定義できるし, x∨y:=x‾∣y‾x\lor y:=\overline{x}\mid \overline{y} と和も定義できる. どちらかをも定義せずとも, 否定に加えて積があれば和が定義できるし, 和があれば積が定義できる.

参考文献

  1. “What is the difference between Boolean logic and propositional logic?” 2019 年 4 月 13 日アクセス.
  2. “What is the difference between Boolean Algebra and propositional logic? If either they are same or one is a subset of another why should we study those separately?” 2019 年 4 月 13 日アクセス.
  3. J. Donald Monk (1976) “Mathematical Logic (Graduate Texts in Mathematics)” Springer; Softcover reprint of the original 1st ed. 1976版 (1976/9/7). ISBN-13: 978-1468494549
  4. 赤間世紀, 長田康敬, 玉城史朗 (2006)『情報数学入門』共立出版. ISBN-13: 978-4320018143
  5. W. V. Quine (1952) “The Problem of Simplifying Truth Functions” The American Mathematical Monthly Vol. 59, No. 8 (Oct., 1952), pp. 521-531
  6. W. V. Quine (1955) “A Way to Simplify Truth Functions” The American Mathematical Monthly Vol. 62, No. 9 (Nov., 1955), pp. 627-631
  7. [動画] Phalanetra. H.S “Quine McCluskey minimisation and Petrick’s method for obtaining simplified Boolean expressions”, 2019 年 4 月 30 日アクセス.
  8. Lecture #10: Petrick’s Method
  9. Czort, S. (1999) “The complexity of minimizing disjunctive normal form formulas (Master’s thesis)”. University of Aarhus.

  1. イギリスの数学者ジョージ・ブール (英: George Boole) は 19 世紀半ばに人間の思考を代数計算で行うための研究を行い, ブール代数を形式化した. 命題論理はそれよりも昔にフレーゲにより構築された論理体型であるが, これは哲学的投機から派生したものである. 19 世紀後半になると, 哲学者たちは殆どブールの象徴主義を採用し, その後の 20 世紀ではこれらの学問間における明確な区別はなかったとのこと(参考文献2 より引用: The main difference is historical. George Boole was a mathematician interested in efficient practical solutions of complicated logical questions in the middle 19th century. His main innovation was symbolic logic, a system of notation for clear specification of propositions and relations among propositions. [..] Propositional logic goes back to ancient times and derives from philosophical speculation. In the late 19th century philosophers mostly adopted Boole’s symbolism. Therefore in the 20th century there’s no clear distinction between the two fields, ). しかしながら, ブール代数に還元できないいくつかの命題論理が残っているとのこと(参考文献2 より引用: although there remains some propositional logic that cannot be reduced to Boolean symbols. ). これが事実ならば, ブール代数は命題論理のサブセット的な論理であることがいえるが, 参考文献3 p.158 では, “the correspondence between Boolean algebras and sentential logics […] We shall see that there is a full correspondence between these two kinds of mathematical objects. とあり, さらに同著書 p.160 で”the following theorem, which is another kind of completeness theorem for Boolean algebras. […] Hence we may say that the theories of Boolean algebras and of sentential logics are equivalent, in some sense.” とも言われていることから, 大まかに言い切ってしまえば, 殆ど差はないということであろう.↩︎

  2. ブール式は 1 つのブール関数を定めるが, ブール関数はブール式を一意には定めない.↩︎

  3. このあたりは自明とする.↩︎

  4. すなわち, ブール関数の値を記述する. 00 は記述せずに省略される場合もある.↩︎

  5. 2 進値を用いず, 変数を用いて圧縮表を作成する方法はクワイン法といわれる. ウィラード・ヴァン・オーマン・クワイン (英: Willard van Orman Quine) によって提案されたクワイン法がエドワード・J・マクラスキーによって発展されたため, このように言われている.↩︎

  6. この表記の仕方は Wikipedia の記事を参考とした.↩︎

  7. 参考文献 9 より↩︎

  8. これについては, 命題論理のエントリ(TODO)内のトートロジー判定器のセクションにおいて取り上げている.↩︎

活動継続のためのご支援を募集しています