四色定理

Robertson らによる四色定理の証明の勉強をしたいと思います。

Link

これは「四色定理の初等的な証明」と解釈するのがよさそうです。「ほとんど正しく証明されている」と思えるようにはなるのですが、「証明として完全に正しい」と確信できるようになるにはかなりの努力が必要です。「これなら自分で証明した方が楽だ」と思うかもしれません。

三角化された平面グラフで次数の大きな頂点が多ければ、四色での彩色が難しくなる傾向があると思われます。しかし、オイラーの公式より、次数の大きな頂点があればその分次数の小さな頂点がなければなりません。それで、次数の大きめの頂点が次数の小さな頂点に囲まれていたり、次数の小さな頂点が集まった地域（その一部が可約配置となります）が出来てしまうことが、放電法により証明されます。電荷を移動させるには、ルールとして周囲に次数の小さな頂点があることが要求されるからです。この考え方は基本的には Appel & Haken と同じです。違うのは放電法による手続きもコンピューターを使うので、検証がしやすく、かつ cartwheel と呼ばれる小さな領域で行うことが可能となったことです。

可約性に関しては D-reducible などの正確な定義がインターネットで見つけられず苦労しました。論文を読んでも signed matching の意味がよくわからず、これも苦労しました。辺彩色が使われますが、これは計算の高速化の意味が大きいようです。

驚いたのは15.の構造の数理　四色問題（1）です。Appel & Haken は1976年に証明を発表しましたが、1980年代には証明が間違っていると噂が広まったそうです。Appel & Haken は 1989年に出版した本で、1976年の証明の細部のほころびはすべて修正可能であることを示した、というのです。1976年の証明は完全なものではなかったが、修正可能な小さな間違いしかなく、証明が間違いというほどではない、ということだと思います。当時発見されていた間違いに対するものなので、現在のコンピュータ技術で検証するとどうなるのか知りたいところではあります。

16.の Four color theorem (wikipedia) の一部分の Google翻訳です。

1980年代初頭、アペル＝ハーケンの証明に欠陥があるという噂が広まった。アーヘン工科大学のウルリッヒ・シュミットは、1981年に出版された修士論文のためにアペルとハーケンの証明を調べた。彼は不可避性の部分の約40%をチェックし、排出手順（放電法の手続き）に重大な誤りを発見した（アペル＆ハーケン1989 ）。1986年、アペルとハーケンは、数学インテリジェンサーの編集者から、彼らの証明の欠陥の噂に対処する記事を書くように依頼された。彼らは、噂は「[シュミットの]結果の誤解」によるものだと答え、詳細な記事を書くことで応じた。彼らの最高傑作であるEvery Planar Map is Four-Colorableは、完全で詳細な証明であると主張する本（400ページを超えるマイクロフィルムの付録付き）で、1989年に出版された。それはシュミットによって発見された誤りと、他の人によって発見されたいくつかのさらなる誤りを説明し、修正した。

プログラムの実行

3 の 4CT information page からプログラムとデータを入手して、Windows10 + MSYS2 + MinGW-w64 で実行してみました。

ディレクトリを作ってその中に unavoidable.conf reduce.c discharge.c present7 present8 present9 present10 present11 rules を入れておきます。そのディレクトリにいってコンパイルします。とりあえず最適化オプションは -O2 としました。

$ gcc -O2 -o reduce reduce.c
$ gcc -O2 -o discharge discharge.c

両方とも warning がでますが無視しても実行できます。

$ reduce


   This has ring-size 6, so there are 122 colourings total,
   and 95 balanced signed matchings.

   There are 16 colourings that extend to the configuration.

            remaining               remaining balanced
           colourings               signed matchings

                  106               25
                   10               15
                    8               11
                    4               3
                    1               0
                    0


                  ***  D-reducible  ***

$ discharge present7
Verifying present7
Reading rules from file `rules'.
Total of 67 rules resulted in 103 outlets of degree 7.
Outlets written into file `outlet.et'.
Reading unavoidable set from file `unavoidable.conf'.
Total of 633 configurations.
present7 verified.

ソースコードを見ると古いC言語の書き方ですが、芸術的プログラムです。実行速度はかなり速いです。

reduce.c と reduce.c の両方ともグラフが３角化されているということを有効に使おうという意図が感じられます。

unavoidable.conf には各頂点の座標がありますが、リングの頂点は置いてあるだけで、辺が交差しないように配慮されていません。1024x + y と説明されていますが、逆に 1024y + x と解釈して、x軸は左から右、y軸は上から下へ、原点は左上の隅としたほうがいいようです。

REDUCIBILITY

Tait-3-辺彩色を使うそうです。頂点彩色に比べて彩色も速くなるのでしょうが、グラフが大きくないので効果はそれほど大きくはないと思われます。Kempe-Chain による塗り替えを大量にやらなくてはならないので、こっちの効果は大きいようです。

Tait-3-辺彩色から３進数にコード化するのですが、難しいです。縮約したグラフの彩色を説明していますが、これも難しいです。 Kempe-Chain による塗り替えに相当することを、reduce.c の stillreal でやっているようなのですが、"Reducibility in the Four-Color Theorem" を読んでみても説明がよくわかりません。

ただ、D-reducible と C-reducible の意味がわかってきたので、頂点彩色版の Reducibility の確認をするプログラムを自分で作ってみることにしました。Tait-3-辺彩色版を理解するのは後でよさそうです。まずは D-reducible を整理してみます。

最少反例があると仮定します。三角化されていると仮定するので、最小というのは頂点の個数が最小の反例ということになります。これは複数あるかもしれません。

細かなことは省略するとして、最小反例にはリングがあり、外側と内側に分割しています。外側 + リングとリング + 内側を別々に4-彩色することが可能なはずです（小さなグラフになっているので）。両方の彩色でリングの彩色で共通のものはなく、外側がリングに求める彩色と、内側がリングに求める彩色は矛盾することになります。ここまでは Birkhoff と同じです。

内側に Reducibility の判定をしたいグラフが配置されているものとします。リング + 内側を４色以内で彩色する方法のすべてから、リング部分の彩色を抜き出したものの集合を goodColoring とします。リングの部分だけを4-彩色して、goodColoring に含まれないものの集合を badColoring とします。badColoring に含まれるリングの彩色を使った場合、リング + 内側を4-彩色することは不可能です。

次に使うのが Birkhoff が説明している Complementary Kempe chains です。３つのタイプがあります。badColoring からリングの彩色を１つ選びます（この選ぶ順序に結果が依存しないことを証明するべきかもしれません、たぶん誰かがすでにやってるはずですが）。その彩色において、３つの Complementary Kempe chains のどれかで、どのように Complementary Kempe chains がつながっていても、ある Complementary Kempe chains の塗り替えによって、goodColoring のどれかにすることができる、という性質をもっているかどうかを調べます。この性質をもっていた場合は、そのリングの彩色を badColoring から取り除き、goodColoring に付け足します。そうでなければ、なにもせずに次の badColoring の彩色を同じように調べます。

上記を繰り返して、badColoring が空になれば D-reducible と判定されます。空ではないのに goodColoring に移せるものがなくなった場合は C-reducible であるかどうかを調べます。

unavoidable.conf には D-reducible でないものには、縮約する辺が指定されています。その辺を縮約したグラフを彩色して、リングの彩色を取り出して goodColoringX とします。goodColoringX に含まれないリングの彩色のすべてを badColoringX とします。それから、D-reducible の判定のときに残った badColoring のすべての彩色が badColoringX に含まれていれば C-reducible と判定できます。なぜなら、この条件を満たすと辺を縮約したグラフは4-彩色不可能であることになり、最小反例とした仮定に矛盾するからです。

ただし、縮約する辺を本当に縮約したグラフを作る必要はありません。もし本当に縮約してしまうと、リングの頂点で同じ頂点に複数の名前がついているとかしなければならず、複雑になってきます。そこで、辺は両端の頂点が同じ色の場合は１、異なる色の場合は０と定義して、縮約する辺は１にその他の辺は０になる色の割り当てを探す、とすればプログラムのわずかな変更で対応できます。

ということで Java でプログラムを作ったのですが、激遅でした。。。　ただ、D-reducible でないものでは最後まで残る badColoring の数が reduce.c のものと一致し、D-reducible の解釈が正しいようだと自信がもてました。

8 の "A systematic approach to …" を読んでみると（といってもほとんど分からないのですが）Heinrich Heesch が分類して、A-, B-, C-, D-reducibility となったらしいです。さらに K-reducibility というのもあって "Kempe-boxequations" という概念がつくられたそうですがよく分かりません。それとは独立に "block count consistency" というのもあるようです。

UNAVOIDABILITY の方も読んでいますが、きちんと理解するのは大変そうです。しかし、わかってきたのは、もう少し一般化して論理的に整理するとブール代数を使った証明に変形できそうだということです。この4CTの証明ではグラフの全体を一般的に表現する方法を見つけていなくて、個々の部分グラフを具体的に表現するために場合分けが大量に必要になっています。そして大量の場合分けの結果、すべての平面グラフが４色で彩色できるという、同じ方向を向いているのがなぜなのか理解が難しくなっています。ブール代数を使った方法では、多くの場合分けを使う前の根元に近いところで計算されるため理解が容易になります。

UNAVOIDABILITY

good configuration と rule（pass）の頂点には、γで表される自然数が定義されています。これは最小反例のグラフでの、その頂点の次数を表しています。

放電法は cartwheel 上で行われます。なるほど cartwheel を使えばコンピューター上で平面グラフを構成するのが容易です。それにこうした制限のある中での放電法はなにか違った印象があります。

cartwheel の頂点のγに範囲を持たせて一般化したのが axle ということらしいです。axle のγの範囲が分割されていき、axle が場合分けされます。Symmetry と Reducibility と hubcap の３種です。どう場合分けをするのかを具体的に書いてあるのが "present7", "present8", "present9", "present10", "present11" です。これらのファイルの内容が、所与の性質を持ち、ちゃんと場合分けされているのかを検証するのがプログラム discharge.c の目的です。

rules

# This file describes a set of rules equivalent to the set from the paper
# `The Four-Colour Theorem' by N. Robertson, D. P. Sanders, P. D. Seymour
# and R. Thomas. Please refer to the manuscript `Discharging Cartwheels'.
# As explained therein, to describe a rule we list beta(v_0), delta(v_0),
# beta(v_1), delta(v_1), and all triples (i,beta(v_i),delta(v_i)) such
# that 2<=i<=16 and v_i belongs to V(G).
#
# The first line of each rule describes beta(v_0), delta(v_0), beta(v_1)
# and delta(v_1) using the convention that "5" means "55", "6" means "66",
# etc. The second line describes all triples (i,beta(v_i),delta(v_i))
# using the same convention as above and interpreting "9" to mean "12".
# If there are no triples (i,beta(v_i),delta(v_i)), then the second line
# is omitted.
#
# 22 April 1995, slightly revised 14 January 1997
#
#

# Rule 1
1        5 59

2        invert

# Rule 2
3        56 79
3 5

4        invert

# Rule 3
5        56 69
3 56        5 5

6        invert

# Rule 4
7        6 69
3 5        5 56        9 5

8        invert

行頭の # はコメント行であることを表し、空行が rule の定義の区切りのようです。改行は LF です。# Rule 1 のように書いてある番号が Fig. 4 The rules に出てくる順番、そのすぐ下の行の数字がその rule に割り振られた番号のようです。# Rule 5 だけなぜか TAB を使ってないので、TAB も空白と解釈したほうが無難です（1997年に少し修正したと書いてあるので、変更した部分なのかもしれません）。フォーマットとしては次のような１行または２行です。

# Rule (Fig. 4 での番号)LF
(ruleの番号)TAB(v_0のbeta)(v_0のdelta)空白(v_1のbeta)(v_1のdelta)LF
(頂点の番号)空白(beta)(delta)TAB(頂点の番号)空白(beta)(delta) TABで区切った繰り返し LF

あるいは

(ruleの番号)TABinvertLF

で、これは直前の rule の鏡像のことだと思われます。discharge.c では invert は最初の i の１文字だけで判断されます。

beta と delta が同じである場合は省略して１つになります。ただし、delta の 9 は 12 を意味します。

裏返しにして重なる rule は、２つに分割して、片方の invert をするようです。rule 10, 31 がそうです。rule 12 は裏返しても同じになるで invert しません。rule 1 は特別で invert しますが、動かす電荷が２なので正味の効果が同じになります。不思議なのは rule 4 でなぜ分割しているのかわかりません。（回転させる計算の都合上、hat の位置か fan の位置か曖昧な頂点が生じないようにこうしたようです。）

頂点の番号は次の図のように解釈されます。rule はこの図の部分グラフになっています（正確には辺を付け足す場合もありますが、それはγの値から導くことができます）。FIG. 4. The rules. の 21, 22, 27, 29 番目の rule の図が裏返しになったグラフになっています。どうしてそうしたのか分かりません。

rule

good configuration にはγが９以上の頂点は多くても１つしか現れず、現れた場合はその頂点を hub とした場合のみを考えればいいようです（たぶん）。rule では、source または sink を hub にした場合、その rule の spoke の位置にγ=９以上の頂点が現れる場合は、その頂点の上の fan はその rule に現れません。

そのためγとしては、{5, 6, 7, 8, 9以上} の４つの場合だけでよく、spoke のγが９以上の場合はその上の fan は必要ないということで、有限化されるようです。（これで証明できるように good configuration と rule がつくられている、ということです）

outlet.et

rules ファイルを実際に読み込むのは ReadOutlets で次のように呼び出されます。

main --> CheckHubcap --> ReadOutlets --> DoOutlet

1つの rule を読み込んだら DoOutlet で outlet に変換されます（あるいは捨てられるようです）。すべての rule が処理されたら、CheckHubcap に戻ります。

CheckHubcap --> PrintOutlet

PrintOutlet が呼び出され、outlet がファイル outlet.et に書き出されます。

次数が7のときの outlet.et の先頭部分を見てみます。

0  1              1
 1   5   5

1  1              2
 1   5   5

2  1              3
 1   5   6
 2   5   5

3  1              4
 1   5   6
 7   5   5

4  1              5
 1   5   6
 2   5   6
 8   5   5

マイナスの数もでてきます。

16  1              17
 1   7   7
 2   5   6
 8   5   5

17  -1              -17
 1   7  12
 7   5   6
 6   5   5

通し番号値（これは source から sink に移動する電気の量です）対応する rule の通し番号（ファイル rules での番号）の±、が書かれている行があり、その次から、axle での頂点の番号 γの下限 γの上限、となっています。

rule の番号が正のときは axle での頂点の番号１が source で、０が sink です。負の時は０が source で、１が sink です。

rule が axle の座標（頂点の番号）に変換され、あとは axle上の座標変換で回転させて使うようです。

/*************************************************************************
     CheckHubcap
If str==NULL it assumes that A is the trivial axle of degree deg, where
deg=A->low[0]. It reads rules and computes the corresponding outlets. It
writes the outlets into the file specified by OUTLETFILE so they can be
verified for accuracy.
If str!=NULL it verifies hubcap line as described in [D]
**************************************************************************/
void
CheckHubcap(A, str, lineno, print)
int lineno, print;
tp_axle *A;
char str[];        /* input line */

CheckHubcap で、present ファイルから読み込まれた条件や hubap の簡単なチェックが行われます。hubap は最大２つの spoke に関するものなので、その２つの positioned outlet が１つにつながれて posout[ ] で参照される構造体の配列にコピーされます。そのときに、int s[ ] が 0 に初期化されます（これは後で outlet の分類に使われます）。そして "Discharging cartwheels" の (H1) をチェックするために CheckBound が呼び出されます。

CheckHubcap --> CheckBound

CheckBound

hubcap というのは

(x, y, v)

という形をしていて、x, y は spoke の頂点の番号（x == y の場合もあります）で、v は整数です。present ファイルの中に、axle のγにある程度の制限をしてから出てきます。その axle で source と sink が hub, x, y のどれかという条件の positioned outlet によって hub に移される電気の量が v 以下であることを主張するものです。それを検証するのが関数 CheckBound です。

axle すべての頂点のγを決めてから hub に移される電気の量を求めるのではなく、ある程度γを絞った状態で電気の量の概算することで効率化するものと思われます。直接 axle 全体を分析するのではなく、Hubcap に分割してから分析を進めるという分割統治法です。

positioned outlet（これは outlet に、outlet をどれだけ回転させるか、という情報を持たせたものです）を２つに分類します。enforced と permitted です。

enforced　これは positioned outlet で要求されるγの範囲が、axle で指定されている範囲より広いか同じ場合です。この axle に compatible な cartwheel すべてがその位置でその rule が適用されます。

permitted　これは positioned outlet で要求されるγの範囲と、axle で指定されている範囲に共通部分がある場合です。この axle に compatible な cartwheel でその位置でその rule が適用されるものが存在します。

配列 s[pos] がアルゴリズムを理解する鍵になりそうです。各 positioned outlet に対応し、-1, 0, 1 の３つの値をとります。 -1 はその positioned outlet が axle に適用されない場合（permitted でない場合）または、その positioned outlet が適用される場合がすでにチェック済みの場合です。0 はその positioned outlet が axle に permitted されている場合です。1 はその positioned outlet が axle に適用されている（enforced されている場合）または適用すると仮定された場合（この場合は、その positioned outlet が enforced される axle がつくられ CheckBound が再帰的に呼び出されます）です。

関数 CheckBound のシグネチャです。maxch に v が入れられます。depth, lineno, print は詳しい内容を表示するためのもので必須ではありません。

void
CheckBound(A, posout, s, maxch, pos, depth, lineno, print)
int maxch, s[], pos, depth, lineno, print;
tp_posout posout[];
tp_axle *A;

（１）s[i] == 0 になっている positioned outlet が enforced か permitted でないかを判定します。enforced の場合は s[i] = 1 にセットして、!permitted の場合は s[i] = -1 にセットします。

（２）s[i] == 1 になっている positioned outlet の value の値（hub に送られる電気の量です）を int forcedch に集計します。 s[i] == 0 かつ value が正の値をもつ positioned outlet の value の値を int allowedch に集計します。（value が負の値である positioned outlet まで合算してしまうと、maxch 以下になることを保証するのが困難になるためだと思われます。）

（３）forcedch + allowedch <= maxch となっていればこの hubcap の検証は成功で終了です。そでなかった場合は、forcedch > maxch を調べて成立している場合は axle A が reducible か（good configuration が現れるか）をチェックします。reducible でなければ検証は失敗でプログラムは終了です。そうでなければ以下に続きます。

（４）sprime と axle AA の記憶領域を確保します。

（５）PO = posout[pos] とします。PO は CheckBound が呼ばれたときに引数 pos で指定された positioned outlet への参照です。変数 pos が pos から positioned outlet のすべてを渡る for ループに入ります。

（６）axle A を AA にコピーします。それから AA のγの範囲を A の範囲と PO での範囲の共通部分にします。

（７）int good = 1 にセットします。0 から pos 未満の positioned outlet で AA に enforced されるものがないか調べます。もしあれば、現在 pos で指定された positioned outlet が適用される場合については、すでに検証済みということになります。この場合は CheckBound の再帰的呼び出しを行わないことを表すため good = 0 とします。

（８）good != 0 の場合の処理です。sprime[ ] に s[ ] の内容をコピーします。sprime[pos] = 1 にセットします。
CheckBound(AA, posout, sprime, maxch, pos + 1, depth + 1, lineno, print);
で再帰的に呼び出します。（pos が pos+1 になっていて "DISCHARGING CARTWHEELS" の説明とは異なっていますが、たいした違いではないでしょう。）

（９）good == 0 または CheckBound の再帰的呼び出しが問題なく帰ってこれた場合です。s[pos] = -1 とします。allowedch から PO の value を減じます。allowedch + forcedch <= maxch が成立するかを計算します。成立すれば、残りの s[i] == 0 になっている positioned outlet が適用されるかどうかにかかわらず、maxch 以下となるのでこの hubcap の検証は成功で終了です。sprime と AA のメモリーを開放して呼び出し元に復帰します。不等式が成立しなければ、次の positioned outlet で同様に繰り返します。次のが無ければ、検証は失敗でプログラムは終了です。

CheckBound についておおよそのところは理解できました。論文と discharge.c を読めば理解できるようには書かれていますが "DISCHARGING CARTWHEELS" で配列 s をもう少し詳しく説明してくれれば理解しやすかったかなと思います。

この証明方法は頂点の次数にこだわるという特徴があります。Birkhoff のアイデアがそうだったので当然かもしれません。しかし、このことが Hadwiger予想研究には障害になっていそうです。グラフを縮約したとき次数がどうなってゆくのかについて、簡潔で、良い性質がなかなか見つからないようです。頂点の次数と彩色数との関係も容易ではないでしょう。そのため、n点の完全グラフに縮約不可能なグラフを縮約したものも n点の完全グラフに縮約不可能であるという自明な性質が十分に使えず、証明が困難になっているのではないでしょうか。ブール方程式による証明では縮約による変化が簡単に分類できます。

Reduce

関数 Reduce は引数に与えられた axle に（正確には、axle に compatible なすべての cartwheel に）ある good configuration が現れることを検証するのが目的です。

good configuration が現れることを確認する方法は、最少反例が彼らのいう“internally 6-connected triangulation”であることを利用するもので、向き付けられた三角形を貼り合わせていく方法で、ほんの少しだけホモロジーが入ってます。

引数 A が NULL で呼び出されると、unavoidable.conf を読み込むなどの準備が行われます。

GetConf, ReadConf

main --> Reduce(NULL, 0, 0) --> GetConf(conf, redquestions) --> ReadConf(*conf, F, NULL)

ReadConf ではチェックも行われ tp_confmat A; に読み込まれます。

#define VERTS      27        /* max number of vertices in a free completion + 1 */
#define DEG        13        /* max degree of a vertex in a free completion + 1 */
typedef long tp_confmat[VERTS][DEG];        /* must be long */

good configuration のデータが読み込まれるわけですが、A[0][0] は ring も含めた頂点の個数、A[0][1] は ring-size です。頂点の番号は１から始まります。A[頂点の番号][0] はその頂点の次数（ring 以外の頂点ではγと同じです）。A[頂点の番号][1] からはその頂点に隣接する頂点の番号が時計回りで格納されています。

GetConf は GetQuestion も呼び出します。

GetQuestion

GetConf(conf, redquestions) --> GetQuestion(*conf, redquestions[noconf])

GetQuestion は *conf から tp_question Q を作ります。question は query の配列です。

typedef struct {
   int u;
   int v;
   int z;
   int xi;
} tp_query;
typedef tp_query tp_question[VERTS];

query は、u から v に進み最も右に曲がると z があるという意味です（u, v, z で時計回りの３角形の面を作っています）。xi は z の次数（γ）ですが例外的に z が ring の頂点の場合がありそのときは xi は 0 です。

まず ring ではない頂点でもっとも次数（γ）が大きい頂点が選ばれ best に代入されます。best に隣接する ring 以外の頂点で最も次数が大きい頂点が secondbest です。これらは Q[0] と Q[1] に入れられます。best と secondbest を結ぶ辺が、good configuration が現れるかを確認する最初の１辺となります。Q[1].u には ring も含めた頂点の個数が、Q[1].v には ring の頂点の個数が入れられます。Q[ ].u == -1 で終了です。Q[ ].z はそれまでに使われていない頂点になっています。

   Q[0].z = best;
   Q[0].xi = L[best][0];
   Q[1].z = secondbest;
   Q[1].xi = L[secondbest][0];

頂点 best を中心に時計回りの三角形をつくっていきます。が、good configuration には頂点を１つ取り除くと２つに分割されるものがあります。そのくびれているところの頂点に隣接しているリングの頂点を１つ付け足すことで、三角形をつなげていきます。enhancement とよんでいます。付け足す頂点は２つのうちのどちらかですが、どちらでもいいようです。そのくびれた所の頂点は hat か fan の位置には現れないとしてよいようです。（くびれたところの頂点の gamma は６以上になっています。ですから hat か fan の位置には現れることはできません。good configuration にある gamma が９以上の頂点はあっても１つだけです。その頂点は hub の位置にしか現れないとしてよさそうです。最後の633番目の good configuration には gamma が11の頂点があります。gamma が11の頂点を表す記号は説明されていません。Appel and Haken では定義されています。１度しか現れないからでしょうか）

GetConf は Radius も呼び出します。

Radius

GetConf(conf, redquestions) --> Radius(*conf)

Radius(*conf) は *conf が radius at most two をもつかチェックします。問題なく終われば Reduce に戻り main に戻ります。good configuration の center を見つけ出すわけですが、この情報は使われません。

ここまでは、準備です。本当に処理されるのは A が NULL でないときです。そのときに呼び出される関数をみていきます。

関数 Reduce は Getadjmat を呼び出します。

Getadjmat, DoFan

Reduce --> Getadjmat(B, adjmat) --> DoFan(deg, i, A->upp[i], adjmat)

typedef int tp_adjmat[CARTVERT][CARTVERT];

Getadjmat は skeleton 上で隣接している２頂点 u, v に対して、(u, v, adjmat[u][v]) が時計回りで skeleton の３角形の面になるようにします。もしその三角形がなければ adjmat[u][v] == -1 です。

axle B が axle A の skeleton であるとは、spokes の頂点については A でのγの上限 u_A(i) が８以下の場合は、B でのγを u_A(i) にし、spokes の他の場合と他の頂点については、A の設定のまま、としたものです。

skeleton B から（といっても実際は axle A のコピーを skeleton と解釈するだけです）adjmat がつくられます。ただし、spoke の頂点のγが９以上の場合はその上の fan は無視されます（DoFan は呼び出されません）。

GetEdgelist, AddToList

次は GetEdgelist です。edgelist は good configuration を探し出すときの最初の１辺がγで分類された配列です。

Reduce --> GetEdgelist(B, edgelist) --> AddToList(edgelist, u, v, degree)

typedef int tp_edgelist[12][9][MAXELIST];

skeleton B で頂点 u, v が隣接しているものとします。B での u のγを a、v のγを b とすると、a >= b, b <= 8 and a <= 11 のとき、ある i = 0, 1, … で edgelist[a][b][2*i+1] = u, edgelist[a][b][2*i+2] = v が代入されます。特に a == b のときは、u と v を逆順にしたものもリストアップされます。ただし、spoke の頂点のγが９以上の場合はその上の fan は無視されます。

SubConf, RootedSubConf

いよいよ SubConf が呼び出され、h 番めの good configuration が skeleton B に well-positioned で現れるかどうかチェックされます。もし現れないのなら 0 を返し、現れるのなら配列 image に頂点の対応を記録し、1 を返します。image[0] が 0 ならそのままの向きで、1 なら裏返しで現れることを表します。

well-positioned とは、spoke v が good configuration に含まれない頂点であるとき、v に隣接している２つの hat のうちの少なくとも１つがその good configuration に含まれないことです。すべての spoke に対しこの条件を満たさなくてはなりません。

“wrap around and meet themselves”問題（たとえていうと、犬が自分のしっぽをくわえてる状態でしょうか）があるそうです。good configuration は最小反例の誘導部分グラフでなくてはなりません。そのため、good configuration の頂点どうしが、その good configuration に含まれない辺で結ばれてはならないことになります。そのため well-positioned の確認がされ、semi-reducible と呼ばれる状態になります。後でさらに CheckIso で確認するようです。

Reduce --> SubConf(adjmat, B->upp, redquestions[h], edgelist, image) --> RootedSubConf(degree, adjmat, question, image, x, y, clockwise)

/**********************************************************************
        SubConf
Given "adjmat", "degree" and "edgelist" derived from an axle A, and
"question" for a configuration L it tests using [D, theorem (6.3)]
if L is a well-positioned induced subconfiguration of the skeleton
of A. If not returns 0; otherwise returns 1, writes an isomorphism
into image, and sets image[0] to 1 if the isomorphism is orientation-
preserving, and 0 if it is orientation-reversing.
***********************************************************************/
int SubConf(adjmat, degree, question, edgelist, image)
tp_adjmat adjmat;
tp_vertices degree;
tp_edgelist edgelist;
tp_vertices image;
tp_question question;

SubConf は edgelist の question[0].xi と question[1].xi で指定されたγをもつ部分から、最初の１辺を取り出し順に試してゆきます。時計回りと反時計回りを試します。実際には RootedSubConf を呼び出します。その good configuration が現れるなら 1 で復帰、現れないなら 0 で復帰します。

int RootedSubConf(degree, adjmat, question, image, x, y, clockwise)
int degree[], x, y, clockwise;
tp_adjmat adjmat;
tp_vertices image;
tp_question question;

最初の１辺が指定されて呼び出されるので、そこから、すり合わせていきます。question の query を１つづつ読んで、adjmat から得られる頂点のγ（axle B で定義されているγの上限が使われます）と一致するか調べます。axle B の頂点が重複して対応していないかも配列 used でチェックされます。well-positioned かもチェックされ問題なく対応していれば 1 で復帰し、そうでなければ 0 で復帰します。対応は配列 image に格納されます。もちろん 0 で復帰したときは image の内容は無効です。

image[good configuration側の頂点の番号] = 対応する axle B の頂点の番号

引数 clockwise が 0 のときは、query の u と v を逆に入れ替えて解釈し裏返しにします。

well-positioned な位置に現れる good configuration が見つかったときは、配列 image の情報をもとに CheckIso でもう一度チェックします。

CheckIso

Reduce --> CheckIso(conf[h], B, image, lineno)

/*********************************************************************
            CheckIso
Verifies that image is an isomorphism between L and a well-positioned
induced subconfiguration K of the skeleton of A
*********************************************************************/
void
CheckIso(L, A, image, lineno)
tp_confmat L;
tp_axle *A;
tp_vertices image;
int lineno;

CheckIso は Getadjmat を呼び出して adjmat をつくります。ほかはソースコードにあるコメントの通りチェックが行われるようです。チェックの結果問題があれば、そこでエラーメッセージを出してプログラムは終了です。

A!=NULL で呼び出されたときの reduce の動作を整理してみます。

/*********************************************************************
            Reduce
 If A==NULL it initializes by allocating memory and reading reducible
 configurations from the file specified by UNAVSET, and computing
 "redquestions" (i.e. questions corresponding to the unavoidable set)
 If A!=NULL it tests reducibility of A as described in [D]
*********************************************************************/
int Reduce(A, lineno, print)
int lineno, print;
tp_axle *A;

Astack は axle構造体の配列への参照で、スタックとして使われます。B もaxle構造体への参照ですが skeleton として使われます。

static tp_axle **Astack, *B;

Astack の大きさは MAXASTACK ですが、これは５と定義されています。たったの５つで済むようです。

（１）引数で与えられた axle A を Astack に入れます。

（２）for ループに入りますが、これは Astack が空になるまで続けられます。

（３）Astack から axle を取り出し skeleton B とします。

（４）B から配列 adjmat の設定のため Getadjmat(B, adjmat) を呼び出します。

（５）B から配列 edgelist の設定のため GetEdgelist(B, edgelist) を呼び出します。

（６）for ループに入ります。このループは順に good configuration を指定し、SubConf(adjmat, B->upp, redquestions[h], edgelist, image) を呼び出して、B に指定された good configuration が現れるかを確認します。現れればこの for ループを抜けます。ループを抜けても現れる good configuration が見つからなければ、0 で関数 Reduce から復帰します。

（７）ここに来るのは B に現れる good configuration が見つかったときだけです。CheckIso(conf[h], B, image, lineno) を呼び出して、誘導部分グラフになっているかなどもチェックします。

（８）B に現れる good configuration に対応する頂点で、かつγの上限と下限がことなる頂点をさがします。見つかれば、B をコピーして Astack に入れてから見つかった頂点のγの上限を１つ下げたものにします。これは good configuration に対応する頂点すべてで行われます。ここまでが（２）の for ループです。

（９）１で関数 Reduce から復帰します（これは成功を意味します）。

例えば「v₁ が γ₁ でかつ v₂ がγ ₂」のときに good configuration が現れることが確認できたら、「v₁ が γ₁-1 でかつ v₂ がγ ₂」の場合と「v₁ が γ₁ でかつ v₂ がγ ₂-1」の場合を調べるという具合にγを下げていきます。これが（８）の意味です。

presentation

“branch-and-bound approach”というそうなんですが、全体を細かく場合にわけて処理するという方針です。全体を表す trivial axle（これは証明に必要な axle の全体です）が condition により細かく分けられて処理されます。どう分けて、どう処理するかを書いてあるのが、present ファイルです。

ファイル present7 は 5,301行あります。一部を書き出してみます。

Degree 7
L0 C  1 -5
  L1 C  2 -5
    L2 C  3 -5
      L3 C  4 -5
        L4 R
      L3 C  7 -5
        L4 R
      L3 C  4  7
        L4 C  7  7
          L5 C 12 -5
            L6 C  5  8
              L7 C  4  8
                L8 H  (2,2,5) (4,4,-2) (5,5,0) (1,3,7)  (6,7,0)
              L7 C  6  6
                L8 H  (1,1,4) (2,2,5) (5,5,0) (6,6,0) (7,7,-1) (3,4,2)
              L7 H  (1,1,4) (2,2,5) (5,5,0) (6,6,2) (7,7,-3) (3,4,2)
            L6 C  6  8
              L7 S 4 1 6 18

（中略）

L0 C  8 -5
  L1 C 11 -5
    L2 R
  L1 C 12 -5
    L2 R
  L1 C  9  7
    L2 H  (3,3,1) (1,2,4)  (4,7,3)  (5,6,2)
  L1 C  9 -5
    L2 H  (1,1,2) (3,3,2) (2,4,4)  (5,6,1) (5,7,2) (6,7,2)
  L1 H  (2,3,3)  (5,6,2)  (1,4,4) (1,7,4) (4,7,3)
L0 C  9 -5
  L1 S 1 0 0 5288
L0 C 10 -5
  L1 S 2 0 0 5288
L0 C 11 -5
  L1 S 3 0 0 5288
L0 C 12 -5
  L1 S 4 0 0 5288
L0 C 13 -5
  L1 S 5 0 0 5288
L0 C 14 -5
  L1 S 6 0 0 5288
L0 H  (1,1,2) (2,2,2) (3,3,2) (4,5,2)  (6,7,2)
Q.E.D.

１行目は hub の次数です。半角空白２つ単位でインデントされていますが、プログラムで読み込まれるときには無視されます。

L の次の数字がレベルを表し MAXLEV より小さくなくてはなりません。MAXLEV は 12 と定義されています。そのあと０個以上（実際には１個になってるようですが）の空白があり、S, R, H, C のいずれかの文字があります。

木構造になっていて、内部ノードは C がある行、末端の葉ノードは S, R, H がある行です。

C は condition、S は Symmetry disposition、R は reducibility disposition、H は Hubcap disposition を表しています。

condition は次の形で書かれています。p はレベルを表す０以上の整数、n は axle の頂点の番号、m は整数で {-8, -7, -6, -5, 6, 7, 8, 9} のどれかです。

Lp C n m

それでは基本的なアルゴリズムを確認します。（main 関数で実行されます。）

（１）まず present ファイルの１行目が読み込まれ、hub の次数が確認されます。

（２）axle の配列 axle の領域が確保され、axle[0] が trivial axle に初期化されます。レベルを表す変数 lev が０に初期化されます。以後 present ファイルが順に読み込まれます。最初は lev == 0 からです。

（３）読み込まれた行が condition なら axle[lev] を axle[lev+1] にコピーします。それから、m の正負によって次のどちらかが実行されます。（これは関数 CheckCondition で実行されます。）

m が正の場合、axle[lev] の頂点n の上限を m-1 にします。axle[lev+1] の頂点n の下限を m にします。
m が負の場合、axle[lev] の頂点n の下限を 1-m にします。axle[lev+1] の頂点n の上限を -m にします。

lev を１つ増やします。

（４）読み込まれた行が、S, R, H の場合は、それぞれの disposition を検証する関数に飛びます。検証が成功し戻ってきたら、lev を１つ減らします。

（５）lev が負になれば、検証が成功し終了してよいことになります。最後に Q.E.D が確認されればプログラムは終了です。（本当は Q.E までしか確認してませんけど）

重要なのは（３）で、自分の持てる axle を削って子に与えるイメージです。

今説明したアルゴリズムは基本であって、Symmetry disposition の検証のためのデータを保持するためのコードが織り込まれます。

Symmetry disposition は回転と裏返す変換で、すでにチェック済みの axle に含まれている場合の処理です。ただし fan-free axle でなくてはなりません。fan-free axle とはすべての fan の頂点のγの上限が12で下限が５になっている axle です。Symmetry の確認には、すでに successful であることが確認されている fan-free axle を参照しなくてはなりません。このへんについての "DISCHARGING CARTWHEELS" の説明は難解で、ソースコードを読んだほうが楽です。

チェック済みとみなせる fan-free axle のデータは tp_outlet sym[ ] に格納され、その個数は int nosym です。これらは main関数で宣言され、記憶領域が確保されます。

sym[ ] への登録は、関数 CheckCondition で行われます。"DISCHARGING CARTWHEELS" で history とよばれているものは、CheckCondition で static tp_cond cond[MAXLEV]; と宣言されている配列 cond です。static と宣言されているので CheckCondition が終わっても cond のデータはそのまま保持されます。さらにＣ言語の規約により、cond[ ].n, cond[ ].m のすべてが１度だけ 0 に初期化されます（この初期化は最初に CheckCondition が呼ばれるとき、または最初に呼ばれる前に行われます）。

#define MAXLEV     12        /* max level of an input line + 1 */

typedef struct {
   int n;
   int m;
} tp_cond;        /* condition */

/*************************************************************************
       CheckCondition
Verifies condition line as described in [D]
*************************************************************************/
void
CheckCondition(S, A, sym, pnosym, lev, lineno, print)
int lev;         /* level of input line */
int lineno;      /* number of input line */
int *pnosym;     /* number of symmetries */
tp_outlet sym[]; /* symmetries (see "main") */
char *S;         /* input line */
tp_axle *A;      /* called A_lev in [D] */
int print;       /* print mode */

cond のデータは axle が fan-free であるかどうかの判定に使われます。present ファイルは木構造になっているので、ルートから現在ノードまでのパス上の condition が配列 cond に記録されることになります。が、しかし、この cond の記録の更新は CheckCondition の終りに行われ、fan-free の判定は直近の同じレベルの cond に対して行われます。これは successful であることが確認されてから sym[ ] に登録するための工夫だと思われます。

tp_outlet sym[ ] に登録されるデータです。number は successful であることが確認された直後の行番号です。valu は 1 ですがこれは論理の真を表しています。nolines は condition の個数です。他に頂点の番号とそのγの下限と上限が記録されます。

      T = &sym[(*pnosym)++];
      T->number = lineno;
      T->value = 1;
      T->nolines = lev + 1;

S, R, H の disposition が処理された後、main 関数で sym[ ] のその lev のデータが削除（実際にはその分の nosym が減らされます）されます。どうしてかというと、ここで削除される fan-free axle は親の fan-free axle に含まれている（正確には、親の世代までの condition からつくられる fan-free axle に含まれている）からです。それから lev が１つ減らされます。

Symmetry disposition は次の形で present ファイルに書かれています。

Lp S k epsilon level line

k は axle を回転させる量です。epsilon は {0, 1} で 1 の場合は axle を裏返しにします。level と line は参照する tp_outlet を識別するためのものです。Symmetry disposition は関数 CheckSymmetry で処理されます。

/*************************************************************************
       CheckSymmetry
Verifies symmetry line as described in [D]
*************************************************************************/
void
CheckSymmetry(S, A, sym, nosym, lineno)
int nosym, lineno;
char *S;        /* input line */
tp_axle *A;
tp_outlet sym[];

CheckSymmetry は配列 sym[ ] から指定された tp_outlet から探し出し、epsilon == 0 の場合は関数 OutletForced を呼び出し、そうでない場合は関数 ReflForced を呼び出します。OutletForced は hubcap で使ったものの使い回しです。

/*********************************************************************
            OutletForced
If (T,x) is enforced by A, then returns the value of T, otherwise 0
*********************************************************************/
int
OutletForced(A, T, x)
int x;
tp_outlet *T;
tp_axle *A;

OutletForced は tp_outlet を指定された量の回転させます。その結果のものが axle A により enforced されることを確認します。

/************************************************************************
            ReflForced
Returns the value of T if M is fan-free and every cartwheel compatible
with A is compatible with tau^(x-1)sigma M, where M is the axle
corresponding to T
************************************************************************/
int
ReflForced(A, T, x)
int x;
tp_outlet *T;
tp_axle *A;

ReflForced は tp_outlet を指定された量の回転をしてから、hub の次数を deg として、spoke の頂点 1 と deg を結ぶ直線の中間と hub を通る直線を軸にして裏返します。その結果のものが axle A により enforced されることを確認します。

reducibility disposition は次の形で present ファイルに書かれています。

Lp R

関数 Reduce が呼び出され、axle A に good configuration が現れることが確認されます。

Hubcap disposition は次の形で present ファイルに書かれています。

Lp H (x₁, y₁, v₁) (x₂, y₂, v₂) … (x_k, y_k, v_k)

本当は数列 x₁, y₁, x₂, y₂, …, x_k, y_k にすべての spoke の頂点が２度現れるのですが、同じ (x, y, v) は省略して１度だけ書かれています。そのため処理が複雑になっています。関数 CheckHubcap 内で次の変数が宣言されています。MAXVAL は12です。

   char *ch;
   int x[MAXVAL + 2], y[MAXVAL + 2], v[MAXVAL + 2];
   int covered[MAXVAL + 2], aux[MAXVAL + 2];
   int i, j, a, total, deg;

x[ ], y[ ], v[ ] にはそれぞれの値がおさめられます。

covered[ ] はまずすべての要素が0に初期化されます。その後、順に (x, y, v) に読み込まれたとき、２度現れた頂点については coverd[その頂点の番号] = -1 が代入されます。まだ１度しか現れていない頂点に関してはペアになっている頂点の番号が代入されます。x がまだ１度しか現れていない頂点だとすると coverd[x] = y となります。

行内の (x, y, v) がすべて読み終えると、coverd[spoke の頂点の番号] != 0 になっているはずです。coverd[spoke の頂点の番号] == -1 であれば、その spoke の頂点は２度現れたことになります。そうでなければ、covered[covered[そのspoke の頂点の番号]] == そのspoke の頂点の番号、となっているはずです。なぜなら、省略された (x, y, v) を付け足すことで、すべての spoke の頂点が２度現れるようにできるはずだからです。covered[x] == y かつ covered[y] == x となっていなければなりません。こうして省略されていた (x, y, v) が見つけ出されます。見つけ出された (x, y, v) の v の値は aux[ ] に格納された値を使います（このようなことが出来るように aux[ ] に代入されています）。

　(x₁, y₁, v₁), (x₂, y₂, v₂), …, (x_n, y_n, v_n)

と、すべての spoke の頂点が２度現れる形になったとします。これに現れるすべての v の和を V とします。

　V = v₁ + v₂ + … + v_n

"Discharging cartwheels" では説明されていませんが、 (x, y, v) で x == y の場合は v を２倍にして合計する必要があります。

放電が終わったあとの hub の電気の量を N_p(W) とします。d は hub の次数です。hubcap が正しく設定されているとすると次の不等式が成立します。（floor は床関数です）

　N_p(W) ≤ 10(6-d) + floor( (1/2)V )

N_p(W) ≤ 0 であることを保証するには次の不等式が成立すればよいことになります。

　10(6-d) + floor( (1/2)V ) ≤ 0

次の不等式と同値です。

　floor( (1/2)V ) ≤ 10(d-6)

２倍します。

　2*floor( (1/2)V ) ≤ 20(d-6)

V が整数であることから、次の不等式と同値です。

　V < 20(d-6) + 2

この否定は

　V ≥ 20(d-6) + 2

ですが、V は整数なので次と同値です。これが偽になることがプログラムで確認されます。

　V > 20(d-6) + 1

以上で、discharge.c がやっていることの概要がわかったと思います。見事に cartwheel という小さな範囲で証明されます。Heesch の予想「オバーチャージされる頂点の２つ隣の範囲を超えることなく現れる可約な配置の不可避集合が証明できる」というのがあったそうで、Birkhoff がイメージした証明が完成したように思えます。

ただ、コンピューターで証明するにしても、そのプログラムを理解するのも大変だし、プログラムを作成してデバグするのも大変な作業です。「証明が正しい」ことを理解しただけで、「証明」を理解するのとは違うのではないかという疑問もあります。

もしも、もっと複雑な条件で成立するような定理ならコンピュータで処理（証明）するのも仕方がないと思ったはずです。しかし、四色定理と Hadwiger予想はあまりにも単純で基本的なものです。こうした場合はより深く分析することで証明を試みるのが当たり前です。

REDUCIBILITY 2

Tait-3-辺彩色が使われています。

Tait-3-辺彩色： triangulation された平面グラフで、三角の面を囲む３つの辺に -1, 0, 1 のすべてが現れるように 3-辺彩色する。その平面グラフが４色以内で頂点彩色できることと同値。near-triangulation（３つより多くの辺に囲まれた面が１つだけあってもよく、その面は無限面とよばれる）の場合も同様。

頂点彩色 $\phi$ から辺彩色 $\kappa$ へ容易に変換することができます。辺 $e$ の端点を $u,v$ とします。

$$\kappa(e) = \begin{cases} -1 &\text{ if\quad} \{\phi(u),\phi(v)\} = \{1,2\}\text{ or } \{3,4\}\\ \ \ \ 0 &\text{ if\quad} \{\phi(u),\phi(v)\} = \{1,3\}\text{ or } \{2,4\}\\ \ \ \ 1 &\text{ if\quad} \{\phi(u),\phi(v)\} = \{1,4\}\text{ or } \{2,3\}\\ \end{cases}$$

$K$： configuration　$R$： ring　$G$：$R$ による $K$ の free completion とします。

$R$ の頂点を $r, r-1, \dots, 1$ の $r$ 個とし、この順で輪になっているものとします。

$e_i$ は $i$ と $i-1$ を結ぶ辺としますが、$e_1$ は $1$ と $r$ を結ぶ辺です。$R$ の辺を順に並べます。

$$e_r, e_{r-1}, \dots, e_{k+1},e_{k}, \dots, e_{1}$$

$R$ の辺彩色 $\kappa$ と $\lambda$ が similar であるというのは、$\{\kappa^{-1}(-1),\kappa^{-1}(0),\kappa^{-1}(1)\} = \{\lambda^{-1}(-1),\lambda^{-1}(0),\lambda^{-1}(1)\}$ となっている場合です。

$\kappa$ が canonical であるというのは、まず $\kappa(e_r) = 0$ であり、以降 $0$ の辺が続き、（もしあるのならば）$\kappa(e_{k}) = 1$ となり、以降は任意となっている場合です。

すべての $R$ の辺彩色は、similar な canonical 辺彩色を１つだけもちます。

$R$ の辺彩色 $\kappa$ が balanced しているというのは、

$$|\kappa^{-1}(-1)|,\;|\kappa^{-1}(0)|,\;|\kappa^{-1}(1)|,\;r$$

これらすべての偶奇が同じときです。これは、$\kappa$ が $R$ の頂点彩色（隣接する頂点は異なる色でなくてはなりません）に対応するための必要十分条件のようです。

$R$ の辺彩色 $\kappa$ は次のように３進法整数にコード化されます。canonical な辺彩色では負になることはありません。

$$code = \kappa(e_r)3^{r-1} + \kappa(e_{r-1})3^{r-2} + \dots + \kappa(e_2)3 + \kappa(e_1) = \sum^r_{i=1}\kappa(e_i)3^{i-1}$$

Complementary Kempe chains が使われますが、３種類ありますが $\theta = -1, 0, 1$ で表されます。同じKempe chain 内の頂点どうしが隣接しているのならば $\theta$ で彩色された辺で結ばれることになります。

$R$ の signed matching $M$ が定義されます。これは $R$ の辺の分割の仕方を定義したもので、ある辺彩色が fit する signed matching が（通常は）複数あることが、その辺彩色の Complementary Kempe chains のつながり方が複数あることに対応するようです。

$$M = \{(m_1,\mu_1),(m_2,\mu_2),\dots,(m_k,\mu_k)\}$$

$m_i$ は $R$ の異なる辺のペア $\{a_i,b_i\}$ で $a_i \gt b_i$ とします。$\mu_i = \pm 1$ です。$\kappa$ が $M$ に fit する辺彩色とすると、$\mu = 1$ なら $\kappa(a_i) = \kappa(b_i)$ であり、$\mu = -1$ なら $\kappa(a_i) \neq \kappa(b_i)$ でなくてはなりません。

論文にはありませんが、サインを取り除いた unsigned matching $uM$ を次のように定義します。

$$uM = \{(a_1,b_1)\,(a_2,b_2) \dots (a_k,b_k)\}$$

カタラン数の "() を正しく並べる方法" と "多角形の三角形分割" の応用と考えるのが分かりやすいと思います。$a_i$ が左かっこ '(' の位置を表し、$b_i$ が対応する右かっこ ')' の位置を表すものと解釈できます。

プログラムを取り出し改造して、リングサイズ $r=6$ で unsigned matching を出力してみました。

{ ( 2, 1) }
{ ( 3, 1) }
{ ( 3, 2) }
{ ( 4, 1) }
{ ( 4, 1) ( 3, 2) }
{ ( 4, 2) }
{ ( 4, 3) }
{ ( 4, 3) ( 2, 1) }
{ ( 5, 1) }
{ ( 5, 1) ( 3, 2) }
{ ( 5, 1) ( 4, 2) }
{ ( 5, 1) ( 4, 3) }
{ ( 5, 2) }
{ ( 5, 2) ( 4, 3) }
{ ( 5, 3) }
{ ( 5, 3) ( 2, 1) }
{ ( 5, 4) }
{ ( 5, 4) ( 2, 1) }
{ ( 5, 4) ( 3, 1) }
{ ( 5, 4) ( 3, 2) }
{ ( 6, 1) }
{ ( 6, 1) ( 3, 2) }
{ ( 6, 1) ( 4, 2) }
{ ( 6, 1) ( 4, 3) }
{ ( 6, 1) ( 5, 2) }
{ ( 6, 1) ( 5, 2) ( 4, 3) }
{ ( 6, 1) ( 5, 3) }
{ ( 6, 1) ( 5, 4) }
{ ( 6, 1) ( 5, 4) ( 3, 2) }
{ ( 6, 2) }
{ ( 6, 2) ( 4, 3) }
{ ( 6, 2) ( 5, 3) }
{ ( 6, 2) ( 5, 4) }
{ ( 6, 3) }
{ ( 6, 3) ( 2, 1) }
{ ( 6, 3) ( 5, 4) }
{ ( 6, 3) ( 5, 4) ( 2, 1) }
{ ( 6, 4) }
{ ( 6, 4) ( 2, 1) }
{ ( 6, 4) ( 3, 1) }
{ ( 6, 4) ( 3, 2) }
{ ( 6, 5) }
{ ( 6, 5) ( 2, 1) }
{ ( 6, 5) ( 3, 1) }
{ ( 6, 5) ( 3, 2) }
{ ( 6, 5) ( 4, 1) }
{ ( 6, 5) ( 4, 1) ( 3, 2) }
{ ( 6, 5) ( 4, 2) }
{ ( 6, 5) ( 4, 3) }
{ ( 6, 5) ( 4, 3) ( 2, 1) }

サインなしの matching では次の数列が狭義単調減少数列になるように作られていることが分かります。

$$a_1, a_2, \dots, a_k$$

全体としては辞書式にソートされた順で作り出しています。

次は、$\mu_i$ を決めて signed matching がつくられます。ただし、balance してなくてはなりません。$M$ が balanced しているというのは、$r-\sum^k_{i=1}(\mu_i-1)/2$ が偶数であることと定義されています。これは $-1$ になっている $\mu_i$ の個数と $r$ の偶奇が同じであるということです。

balanced signed matching $M$ に fit するリングの辺彩色が作られます。同じ $M$ に fit する辺彩色どうしは、$M$ で表される Kempe-chain を考慮した塗り替えで、互いに移り変われるという性質があります。

ですが、ここで問題があります。"Reducibility in the Four-Color Theorem" の説明では符号が合わないのではないかと思うのです。

$$\Big\{\Big|c+\sum^k_{i=2}\epsilon_i h_i\Big|:\epsilon_i\in\{0,1\}\Big\}$$

とありますが、次のようにマイナスにするのが正しいと思われます。

$$\Big\{\Big|c-\sum^k_{i=2}\epsilon_i h_i\Big|:\epsilon_i\in\{0,1\}\Big\}$$

論文にはありませんが semi canonical な辺彩色を定義したほうがよさそうです。$e_r$ が $0$ で他の辺は $-1, 0, 1$ の中で任意とします。

定数 $c$ は signed matching $M$ のコードです。basecol の値が、関数testmatch が augment を呼ぶときに引数として与えられます。（ $r$ はリングサイズです）$(3^r -1)/2$ は３進数で表すと $11 \dots 1$ と $r$ 個の $1$ が並んだ数です。

$$basecol = \begin{cases} \:0 &\text{ if\quad} a_1 \lt r\\ \:(3^r -1)/2 &\text{ if\quad} a_1 = r \end{cases}$$

canonical な辺彩色（または semi canonical な辺彩色）を扱うので、$a_1 \lt r$ の場合というのは必然的に $\theta = 0$ の場合となります。$a_1 = r$ の場合は $\theta = 1$ の場合と思って下さい。$\theta = -1$ の場合は、$a_1 = r$ の場合の数をすべて $-1$ 倍することで表すことができるからです。

つぎの $g_i$ の定義は論文にはありませんが、プログラムとの対応であったほうがいいです。

$$g_i = \begin{cases} \:3^{a_i-1}+\mu_i3^{b_i-1} &\text{ if\quad} a_1 \lt r\\ \:-3^{a_i-1}-(3-\mu_i)3^{b_i-1}/2 &\text{ if\quad} a_1 = r \end{cases}$$

signed matching $M$ のコード $c$ を次のように表すことができます。

$$c = basecol + \sum^k_{i=1}g_i$$

choice sequence $(h_2, h_3, \dots, h_k)$ の定義です。（$2 \le i \le k$）

$$h_i = \begin{cases} \:2(3^{a_i-1}+\mu_i3^{b_i-1}) &\text{ if\quad} a_1 \lt r\\ \:3^{a_i-1}+\mu_i3^{b_i-1} &\text{ if\quad} a_1 = r \end{cases}$$

各 $\epsilon_i$（$2 \le i \le k$）の値を $\{0,1\}$ から任意に選ぶことで、$M$ に fit する semi canonical な辺彩色 $d$ が計算されます。

$$d = c - \sum^k_{i=2}\epsilon_i h_i = basecol + \sum^k_{i=1}g_i - \sum^k_{i=2}\epsilon_i h_i = basecol + g_1 + \sum^k_{i=2}(g_i-\epsilon_i h_i)$$

$\epsilon_i = 1$ の場合、$a_i$ と $b_i$ の位置の桁を $\mu_i$ に従うもう１つの数の組に置き換えることが簡単な計算でわかります。これは $a_i$ と $b_i$ の間の Kempe-Chain の色の塗り替えに相当します。

$a_1 \lt r$ の場合は $d$ が負になることはありません。この場合の $d$ すべての集合は、$\theta = 0$ で $M$ に fit する canonical な辺彩色のすべてです。

$a_1 = r$ の場合の $d$ すべての集合は、$\theta = 1$ で $M$ に fit する semi canonical な辺彩色のすべてです。その中で $d \ge 0$ である $d$ すべての集合が $\theta = 1$ で $M$ に fit する canonical な辺彩色のすべてです。

$a_1 = r$ の場合の $-d$ すべての集合は、$\theta = -1$ で $M$ に fit する semi canonical な辺彩色のすべてです。その中で $-d \ge 0$ である $-d$ すべての集合が $\theta = -1$ で $M$ に fit する canonical な辺彩色のすべてです。

${\cal C}^\ast$ をリング $R$ の canonical で balance した 3-辺彩色のすべてを含む集合とします。

${\cal C}(K)$ を $G$ の3-辺彩色から R の部分の辺彩色を取り出したもので、canonical なものすべての集合とします。

${\cal C}_0$ を差集合 ${\cal C}^\ast - {\cal C}(K)$ とします。

もし、${\cal C}_0$ に canonical で balance した辺彩色が１つもなければ、その時点で $K$ は D-reducible と判定できます。そうでない場合の基本的な考え方を説明します。その辺彩色を $c$ として、$c$ がある $\theta$ で fit する signed matching $M$ の集合を作ります。たとえば $\theta = 0$ で。

$$\{ M_1, M_2, M_3, \dots\}$$

この集合の各 $M_i$ において、その $M_i$ に $\theta = 0$ で fit する辺彩色で ${\cal C}_0$ に含まれないものがあるかを調べます。もしすべての $M_i$ において $\theta = 0$ で fit する辺彩色の少なくとも１つが ${\cal C}_0$ に含まれていないならば、$c$ を ${\cal C}_0$ から消します。どのように $\theta = 0$ で Kempe-Chain がつながっていても、塗り替えで ${\cal C}(K)$ の彩色にできることが確認できたからです。これを他の $\theta$ でも行います。他の canonical で balance した辺彩色でも繰り返します。これで生き残った canonical で balance した辺彩色がなくなれば $K$ は D-reducible と判定されます。$\theta$ の切り換えも許した Kempe-Chain の色の塗り替えの繰り返しで ${\cal C}(K)$ の彩色にできることが確認できたからです。${\cal C}_0$ の canonical で balance した辺彩色が全滅すれば、$K$ は D-reducible です。

reduce.c では逆方向から計算することで高速化されています。すべての signed matching $M$ の中からある $\theta$ で fit する辺彩色のすべてが ${\cal C}_0$ に含まれている $M$ が選び出されます。（それは見せかけではなく、意義のある本物の real な $M$ です）そして $M$ から fit する辺彩色を計算し、その辺彩色に $\theta$ でマークします。すべての real な $M$ でこれを行ったあと、すべての $\theta$ でマークされていない辺彩色を消します（生き残るためにはすべての $\theta$ でマークされている必要があります）。それからまた real な $M$ を選んでを繰り返します。消す辺彩色が生じなくなればこの繰り返しは終了です。canonical で balance した辺彩色が全滅していれば、$K$ は D-reducible です。

もう少し詳しく説明します。上記の方法で生成される signed matching を順に $M_1, M_2, M_3, \dots$ とし、これらすべてを要素とする集合を ${\cal M}_0$ とします。

$${\cal M}_0 = \{M_1, M_2, M_3, \dots\}$$

$(M_i)$ と書いて上記の方法で $M_i$ から計算される semi canonical な辺彩色のすべてとします。もし、$M_i$ で $a_1 \lt r$ ならば $(M_i)$ はすべて canonical な辺彩色です。$(M_i) \subseteq {\cal C}_0$ であるならば $(M_i)$ のすべての辺彩色を $\theta = 0$ でマークします。

もし、$M_i$ で $a_1 = r$ ならば $(M_i)$ の辺彩色は、通常、負の値になるものがあります。そこで、いったん semi canonical まで拡張して考えるのがいいと思います。${\cal C}_0$ のすべての要素を $-1$ 倍して集合 $-{\cal C}_0$ とします。 $-1$ 倍しても $1$ と $-1$ が置換されるだけなので、本質的には同じ辺彩色です。

$(M_i) \subseteq ({\cal C}_0 \cup -{\cal C}_0)$ が成立しているならば、$(M_i)$ のすべての辺彩色を $\theta = 1$ でマークすることになります。そして $(-M_i) \subseteq ({\cal C}_0 \cup -{\cal C}_0)$ が成立しているならば、$(-M_i)$ のすべての辺彩色を $\theta = -1$ でマークすることになります。

実際には canonical な辺彩色のみにマークが行われれば十分です。それに $(M_i) \subseteq ({\cal C}_0 \cup -{\cal C}_0)$ と $(-M_i) \subseteq ({\cal C}_0 \cup -{\cal C}_0)$ は同値です。したがって、$(M_i) \subseteq ({\cal C}_0 \cup -{\cal C}_0)$ が成立していれば、$(M_i)$ の正の辺彩色を $\theta = 1$ でマークし、負の辺彩色は $-1$ 倍して $\theta = -1$ でマークすればよいことがわかります。

コードが $0$ である辺彩色は特別な扱いとなります。というのは空である signed matching をつくらないからです。空の signed matching に fit する semi canonical な辺彩色は $0$ しかありません。リング全体が１つの Kempe chain になってる必要があるからです。そのため、リングサイズが偶数の場合は、$0$ が生き残ってる場合でも、生き残っていない場合でも、空の signed matching は無視してよいことになります。生き残っている $0$ は常に $\theta = 0$ でマークされているものとして構いません。リングサイズが奇数の場合は、$0$ は balanced していない辺彩色として扱ってよいことになります。それに対称性から、$\theta = 1$ でマークされていれば、$\theta = -1$ でもマークされているものとしていいです。$\theta = -1$ でマークされていれば、$\theta = 1$ でもマークされているものとしていいです。$\theta = -1,1$ のどちらかでもマークされていればリングサイズは偶数です。

unavoidable.conf の４番目のデータです。先頭行に 2.126 という数字がありますが、この意味の説明はなく無視して構わないようです。次の行から configuration matrix $A = (a_{i,j})$ として説明されています。

2.126
12   8      81     154
 4    1  9   3  9   5 11   7 11
 1  4     2  9 12  8
 2  3     3  9  1
 3  4     4 10  9  2
 4  3     5 10  3
 5  4     6 11 10  4
 6  3     7 11  5
 7  4     8 12 11  6
 8  3     1 12  7
 9  6     2  3 10 11 12  1
10  5     3  4  5 11  9
11  6    10  5  6  7 12  9
12  5    11  7  8  1  9
 895849  535551  154474     512  152726  512000  894101 1048062
 324078  507098  673262  502516

Home