具体例での説明
図1のグラフは、3色で彩色不可能なグラフです。これは、頂点0 と 頂点6 を異なる色で着色すれば、辺e0,6 を付け足すことと同じで、頂点0, 1, 2, 6 が4頂点の完全グラフになります。もし 頂点0 と 頂点6 を同じ色で着色するなら、頂点0 と 頂点6 を同じ頂点とみなすことと同じで、この頂点と 3, 4, 5 が4点の完全グラフになり、3色で彩色できないことがわかります。こうした事柄はブール代数で表現できる性質です。また、どの辺を取り除いても3色で彩色できるようになることが、実際にやってみることで確認できます。
頂点0 に隣接する頂点の集合を H とします( H = {1, 2, 3} )。頂点0 と 頂点0 の辺を取り除いたのが図2です。
着色の条件X, Y を定義します。
- 条件X:全体を 3色以内で着色する。
- 条件Y:全体を 3色以内で着色するが、集合H の頂点は 2色以内とする。
色を {α, β, γ} の3色として、条件を満たすすべての着色で、各辺がどうなるかを表にしてみます。辺は両端の頂点の色が等しいとき 1、異なるとき 0 を真理値としてとります。
ただし、色の名を置き換えて同じになる着色は取り除いてあります。白抜きはグラフに含まれない辺です。条件X の着色は122通りあり、1~122行がそれです。そのうちの1~95行が条件Y の着色で、95通りあります。
| 1 | 2 | 3 | 4 | 5 | 6 | |
| No. | 1 | 12 | 123 | 1234 | 12345 | |
| 1 | α | 1:α | 11:α | 111:α | 1111:α | 11111:α |
| 2 | α | 1:α | 11:α | 111:α | 1111:α | 00000:β |
| 3 | α | 1:α | 11:α | 111:α | 0000:β | 11110:α |
| 4 | α | 1:α | 11:α | 111:α | 0000:β | 00001:β |
| 5 | α | 1:α | 11:α | 111:α | 0000:β | 00000:γ |
| 6 | α | 1:α | 11:α | 000:β | 1110:α | 11101:α |
| 7 | α | 1:α | 11:α | 000:β | 1110:α | 00010:β |
| 8 | α | 1:α | 11:α | 000:β | 1110:α | 00000:γ |
| 9 | α | 1:α | 11:α | 000:β | 0001:β | 11100:α |
| 10 | α | 1:α | 11:α | 000:β | 0001:β | 00011:β |
| 11 | α | 1:α | 11:α | 000:β | 0001:β | 00000:γ |
| 12 | α | 1:α | 11:α | 000:β | 0000:γ | 11100:α |
| 13 | α | 1:α | 11:α | 000:β | 0000:γ | 00010:β |
| 14 | α | 1:α | 11:α | 000:β | 0000:γ | 00001:γ |
| 15 | α | 1:α | 00:β | 110:α | 1101:α | 11011:α |
| 16 | α | 1:α | 00:β | 110:α | 1101:α | 00100:β |
| 17 | α | 1:α | 00:β | 110:α | 1101:α | 00000:γ |
| 18 | α | 1:α | 00:β | 110:α | 0010:β | 11010:α |
| 19 | α | 1:α | 00:β | 110:α | 0010:β | 00101:β |
| 20 | α | 1:α | 00:β | 110:α | 0010:β | 00000:γ |
| 21 | α | 1:α | 00:β | 110:α | 0000:γ | 11010:α |
| 22 | α | 1:α | 00:β | 110:α | 0000:γ | 00100:β |
| 23 | α | 1:α | 00:β | 110:α | 0000:γ | 00001:γ |
| 24 | α | 1:α | 00:β | 001:β | 1100:α | 11001:α |
| 25 | α | 1:α | 00:β | 001:β | 1100:α | 00110:β |
| 26 | α | 1:α | 00:β | 001:β | 1100:α | 00000:γ |
| 27 | α | 1:α | 00:β | 001:β | 0011:β | 11000:α |
| 28 | α | 1:α | 00:β | 001:β | 0011:β | 00111:β |
| 29 | α | 1:α | 00:β | 001:β | 0011:β | 00000:γ |
| 30 | α | 1:α | 00:β | 001:β | 0000:γ | 11000:α |
| 31 | α | 1:α | 00:β | 001:β | 0000:γ | 00110:β |
| 32 | α | 1:α | 00:β | 001:β | 0000:γ | 00001:γ |
| 33 | α | 1:α | 00:β | 000:γ | 1100:α | 11001:α |
| 34 | α | 1:α | 00:β | 000:γ | 1100:α | 00100:β |
| 35 | α | 1:α | 00:β | 000:γ | 1100:α | 00010:γ |
| 36 | α | 1:α | 00:β | 000:γ | 0010:β | 11000:α |
| 37 | α | 1:α | 00:β | 000:γ | 0010:β | 00101:β |
| 38 | α | 1:α | 00:β | 000:γ | 0010:β | 00010:γ |
| 39 | α | 1:α | 00:β | 000:γ | 0001:γ | 11000:α |
| 40 | α | 1:α | 00:β | 000:γ | 0001:γ | 00100:β |
| 41 | α | 1:α | 00:β | 000:γ | 0001:γ | 00011:γ |
| 42 | α | 0:β | 10:α | 101:α | 1011:α | 10111:α |
| 43 | α | 0:β | 10:α | 101:α | 1011:α | 01000:β |
| 44 | α | 0:β | 10:α | 101:α | 1011:α | 00000:γ |
| 45 | α | 0:β | 10:α | 101:α | 0100:β | 10110:α |
| 46 | α | 0:β | 10:α | 101:α | 0100:β | 01001:β |
| 47 | α | 0:β | 10:α | 101:α | 0100:β | 00000:γ |
| 48 | α | 0:β | 10:α | 101:α | 0000:γ | 10110:α |
| 49 | α | 0:β | 10:α | 101:α | 0000:γ | 01000:β |
| 50 | α | 0:β | 10:α | 101:α | 0000:γ | 00001:γ |
| 51 | α | 0:β | 10:α | 010:β | 1010:α | 10101:α |
| 52 | α | 0:β | 10:α | 010:β | 1010:α | 01010:β |
| 53 | α | 0:β | 10:α | 010:β | 1010:α | 00000:γ |
| 54 | α | 0:β | 10:α | 010:β | 0101:β | 10100:α |
| 55 | α | 0:β | 10:α | 010:β | 0101:β | 01011:β |
| 56 | α | 0:β | 10:α | 010:β | 0101:β | 00000:γ |
| 57 | α | 0:β | 10:α | 010:β | 0000:γ | 10100:α |
| 58 | α | 0:β | 10:α | 010:β | 0000:γ | 01010:β |
| 59 | α | 0:β | 10:α | 010:β | 0000:γ | 00001:γ |
| 60 | α | 0:β | 10:α | 000:γ | 1010:α | 10101:α |
| 61 | α | 0:β | 10:α | 000:γ | 1010:α | 01000:β |
| 62 | α | 0:β | 10:α | 000:γ | 1010:α | 00010:γ |
| 63 | α | 0:β | 10:α | 000:γ | 0100:β | 10100:α |
| 64 | α | 0:β | 10:α | 000:γ | 0100:β | 01001:β |
| 65 | α | 0:β | 10:α | 000:γ | 0100:β | 00010:γ |
| 66 | α | 0:β | 10:α | 000:γ | 0001:γ | 10100:α |
| 67 | α | 0:β | 10:α | 000:γ | 0001:γ | 01000:β |
| 68 | α | 0:β | 10:α | 000:γ | 0001:γ | 00011:γ |
| 69 | α | 0:β | 01:β | 100:α | 1001:α | 10011:α |
| 70 | α | 0:β | 01:β | 100:α | 1001:α | 01100:β |
| 71 | α | 0:β | 01:β | 100:α | 1001:α | 00000:γ |
| 72 | α | 0:β | 01:β | 100:α | 0110:β | 10010:α |
| 73 | α | 0:β | 01:β | 100:α | 0110:β | 01101:β |
| 74 | α | 0:β | 01:β | 100:α | 0110:β | 00000:γ |
| 75 | α | 0:β | 01:β | 100:α | 0000:γ | 10010:α |
| 76 | α | 0:β | 01:β | 100:α | 0000:γ | 01100:β |
| 77 | α | 0:β | 01:β | 100:α | 0000:γ | 00001:γ |
| 78 | α | 0:β | 01:β | 011:β | 1000:α | 10001:α |
| 79 | α | 0:β | 01:β | 011:β | 1000:α | 01110:β |
| 80 | α | 0:β | 01:β | 011:β | 1000:α | 00000:γ |
| 81 | α | 0:β | 01:β | 011:β | 0111:β | 10000:α |
| 82 | α | 0:β | 01:β | 011:β | 0111:β | 01111:β |
| 83 | α | 0:β | 01:β | 011:β | 0111:β | 00000:γ |
| 84 | α | 0:β | 01:β | 011:β | 0000:γ | 10000:α |
| 85 | α | 0:β | 01:β | 011:β | 0000:γ | 01110:β |
| 86 | α | 0:β | 01:β | 011:β | 0000:γ | 00001:γ |
| 87 | α | 0:β | 01:β | 000:γ | 1000:α | 10001:α |
| 88 | α | 0:β | 01:β | 000:γ | 1000:α | 01100:β |
| 89 | α | 0:β | 01:β | 000:γ | 1000:α | 00010:γ |
| 90 | α | 0:β | 01:β | 000:γ | 0110:β | 10000:α |
| 91 | α | 0:β | 01:β | 000:γ | 0110:β | 01101:β |
| 92 | α | 0:β | 01:β | 000:γ | 0110:β | 00010:γ |
| 93 | α | 0:β | 01:β | 000:γ | 0001:γ | 10000:α |
| 94 | α | 0:β | 01:β | 000:γ | 0001:γ | 01100:β |
| 95 | α | 0:β | 01:β | 000:γ | 0001:γ | 00011:γ |
| 96 | α | 0:β | 00:γ | 100:α | 1001:α | 10011:α |
| 97 | α | 0:β | 00:γ | 100:α | 1001:α | 01000:β |
| 98 | α | 0:β | 00:γ | 100:α | 1001:α | 00100:γ |
| 99 | α | 0:β | 00:γ | 100:α | 0100:β | 10010:α |
| 100 | α | 0:β | 00:γ | 100:α | 0100:β | 01001:β |
| 101 | α | 0:β | 00:γ | 100:α | 0100:β | 00100:γ |
| 102 | α | 0:β | 00:γ | 100:α | 0010:γ | 10010:α |
| 103 | α | 0:β | 00:γ | 100:α | 0010:γ | 01000:β |
| 104 | α | 0:β | 00:γ | 100:α | 0010:γ | 00101:γ |
| 105 | α | 0:β | 00:γ | 010:β | 1000:α | 10001:α |
| 106 | α | 0:β | 00:γ | 010:β | 1000:α | 01010:β |
| 107 | α | 0:β | 00:γ | 010:β | 1000:α | 00100:γ |
| 108 | α | 0:β | 00:γ | 010:β | 0101:β | 10000:α |
| 109 | α | 0:β | 00:γ | 010:β | 0101:β | 01011:β |
| 110 | α | 0:β | 00:γ | 010:β | 0101:β | 00100:γ |
| 111 | α | 0:β | 00:γ | 010:β | 0010:γ | 10000:α |
| 112 | α | 0:β | 00:γ | 010:β | 0010:γ | 01010:β |
| 113 | α | 0:β | 00:γ | 010:β | 0010:γ | 00101:γ |
| 114 | α | 0:β | 00:γ | 001:γ | 1000:α | 10001:α |
| 115 | α | 0:β | 00:γ | 001:γ | 1000:α | 01000:β |
| 116 | α | 0:β | 00:γ | 001:γ | 1000:α | 00110:γ |
| 117 | α | 0:β | 00:γ | 001:γ | 0100:β | 10000:α |
| 118 | α | 0:β | 00:γ | 001:γ | 0100:β | 01001:β |
| 119 | α | 0:β | 00:γ | 001:γ | 0100:β | 00110:γ |
| 120 | α | 0:β | 00:γ | 001:γ | 0011:γ | 10000:α |
| 121 | α | 0:β | 00:γ | 001:γ | 0011:γ | 01000:β |
| 122 | α | 0:β | 00:γ | 001:γ | 0011:γ | 00111:γ |
1 を ex,y に、0 を ¬ex,y に置換え、同一行内で論理積をつくると最小項になります。それらの論理和が、加法標準展開です。
No.1 から最後の 122 までから作ったのが K4∧R 、No.1 から 95 で作ったのが k∧K4∧R です。通常、K4 は4点の完全グラフを表しますが、ここでは4点の完全グラフから作られる論理式です。k は同様に3点の完全グラフから作られる論理式です。R も論理式です。
白抜きした辺を無視した No.1 から 122 までが Σ(K4∧R) 、No.1 から 95 までが Σ(k∧K4∧R) です。このように Σ はグラフに含まれていない辺を無視する操作を表しています。
白抜きした辺を無視した上で、No.96 から 122 までの最小項で、No.1 から 95 までに含まれていないものを探したのが次の表です。
| 1 | 2 | 3 | 4 | 5 | 6 | |
| No. | 1 | 12 | 123 | 1234 | 12345 | |
| 101 | α | 0:β | 00:γ | 100:α | 0100:β | 00100:γ |
| 107 | α | 0:β | 00:γ | 010:β | 1000:α | 00100:γ |
| 104 | α | 0:β | 00:γ | 100:α | 0010:γ | 00101:γ |
| 113 | α | 0:β | 00:γ | 010:β | 0010:γ | 00101:γ |
| 116 | α | 0:β | 00:γ | 001:γ | 1000:α | 00110:γ |
| 119 | α | 0:β | 00:γ | 001:γ | 0100:β | 00110:γ |
| 122 | α | 0:β | 00:γ | 001:γ | 0011:γ | 00111:γ |
No.101,107 はグラフのすべての辺を 0 にするものです。No.104, 113, 116, 119, 122 には 1 になっている辺があります。No.101 と 107、No.104 と 113、No.116 と 119、はそれぞれ同じ最少項になります。これらの最小項の論理否定をとり、最大項をつくります。
No.101 より g ⇔ ( e1,2 ∨ e3,4 ∨ e3,5 ∨ e4,5 ∨ e1,6 ∨ e2,6 ∨ e4,6 ∨ e5,6 )
No.104 より g1 ⇔ ( e1,2 ∨ e3,4 ∨ ¬e3,5 ∨ e4,5 ∨ e1,6 ∨ e2,6 ∨ e4,6 ∨ ¬e5,6 )
No.116 より g2 ⇔ ( e1,2 ∨ ¬e3,4 ∨ e3,5 ∨ e4,5 ∨ e1,6 ∨ e2,6 ∨ ¬e4,6 ∨ e5,6 )
No.122 より g3 ⇔ ( e1,2 ∨ ¬e3,4 ∨ ¬e3,5 ∨ ¬e4,5 ∨ e1,6 ∨ e2,6 ∨ ¬e4,6 ∨ ¬e5,6 )
そうすると次の恒真式が成立します。
tautology Σ(k∧K4∧R) ⇔ g∧g1∧g2∧g3∧Σ(K4∧R)
次の形で表すこともできます。
tautology { Σ(k∧K4∧R) ∨ ¬Σ(K4∧R) } ⇔ g∧g1∧g2∧g3
g1 を取り上げます。
tautology Σ(k∧K4∧R) → g1
詳しく書きます。
tautology Σ(k∧K4∧R) → ( e1,2 ∨ e3,4 ∨ ¬e3,5 ∨ e4,5 ∨ e1,6 ∨ e2,6 ∨ e4,6 ∨ ¬e5,6 )
g1 では、e3,5 と e5,6 に論理否定が付いています。そこで、この2辺を縮約したグラフを考えます。その辺を“移項”することができます。
tautology e3,5∧e5,6∧Σ(k∧K4∧R) → ( e1,2 ∨ e3,4 ∨ e4,5 ∨ e1,6 ∨ e2,6 ∨ e4,6 )
さらに Σ の中に入れることができます。
tautology Σ(e3,5∧e5,6∧k∧K4∧R) → ( e1,2 ∨ e3,4 ∨ e4,5 ∨ e1,6 ∨ e2,6 ∨ e4,6 )
e3,5 と e5,6 を縮約したグラフは、条件X で彩色できて、条件Y では彩色できません。ただし、合併する頂点の中に集合H の頂点があるときのみ、合併してできた頂頂点を集合H の頂点とします。多重辺が生じても自動的に同一の辺として扱われます。ループが生じることはありません。なぜなら、その場合は条件X でも彩色できないから仮定に反します。
g2, g3 も同様です。
完全グラフでないとき、どの辺にも論理否定のつかない g のような最大項があれば、g1, g2, g3 のようなどれかの辺に論理否定のついた最大項が生じることを証明すれば、Hadwiger予想を証明したことになります。
四色問題についても K5∧R の表の性質とみなすことが出来ます。その性質を表現するにはブール代数が有効です。