joseph@hp-pcd.UUCP (08/14/84)
Concerning the 4-color conjecture and its demonstration by computer,
I would like to add the following to what already appeared above:
Even assuming that the algorithm and its coding is provably correct,
(absurd as this assumption may or may not be) calling its execution
a proof, simply baffles me. Even the mean time to failure of the hardware
is less than the running time of this program. Re-running of the program
to check for the same results has not and probably will not be performed.
(computer time is too valuable) The non-zero probability that there
was a hardware error implies that there is a non-zero probability
that the "proof" is wrong. (a bit could have flipped yielding incorrect
behavior) However unlikely this event may be, anyone who thinks that proofs
can be probabilistic, should be referred to the nearest logic textbook.
--Joseph Albertgary@arizona.UUCP (Gary Marc Levin) (08/23/84)
I have a copy of both the technical reports and the computer
program that was used in the machine assisted ``proof'' of the
4-color conjecture. The cases were chosen by the humans and then
checked by the machine, not the other way around.
I have no philosophic complaint against using a computer as part of
a proof, IF the algorithm is subject to the same scrutiny as the
rest of the proof. See below.
A brief history.
Kempe tried to prove the 4CC by showing that (1) any graph had
to contain at least 1 of a set of 4 small graphs and (2) that
any 5-coloring of the large graph could be re-colored (due to
the structure of each of these small graphs) with only 4
colors.
Condition (1) was that he had chosen an unavoidable set. It
was proven using a counting argument.
Condition (2) was the combinatorial part. Here, all ``external
colorings'' had to be considered. (Because we are considering
planar graphs, it makes sense to speak of an inside and an
outside of the graph. Those nodes that could connect to a node
outside the graph are called the ``ring'' of the graph. An
``external coloring'' is an assignment of colors to the ring of
the graph.)
Then, all inter-connections are considered, subject to the
coloring constraints and the planar properties. In particular,
consider paths of alternating colors; paths with the other
color-pair cannot cross. This partitions the ring into
connected and non-connected parts. The non-connected parts can
be recolored.
If each external coloring has some recoloring that would result
in a 4-coloring of the entire graph, then any graph containing
the subgraph under consideration would be 4-colorable. (The
subgraph is said to be reducible.)
If every subgraph in the unavoidable set is reducible, then all
graphs are 4-colorable and the 4CC is proven.
Kempe's problem was that one of his graphs was not reducible.
The counting argument of (1) is based on a charging principle. The
proof there is convincing and those people I have met who have seen
it have accepted that the set is probably unavoidable. (There is
the problem that the set is in excess of 1500 graphs with >20 nodes
per graph.)
The reducible argument was done on a computer. The paths of
alternating colors are called ``Kempe chains''.
The first problem is that the code to do the checking is
written in 360 MACRO Assembler with self-modifying code.
The second problem is that the code looks like something that a
first semester programmer might turn-in. (Names of friends for
labels aren't helpful when trying to understand a proof.)
(Also, there are pages of magic numbers without comment.
I finally figured what they were (possible partitions of the
ring) and wrote a short program to generate them. They were
correct.)
The third problem is that there are at least 4 places where the
code does not do what the comments claim. Each of these
disagreements results in a less efficient program, but do not
affect correctness. (For instance, there is a variable that
would result in ``pruning'' the search tree if it were set. It
never is set.) My problem is that it took a long time to find
these ``errors'' and I lost confidence in the correctness of
the algorithm.
My feeling is that if the code had been written in a decent
language, the optimizations would have been done correctlly,
making up for the possible inefficiency of compiler generated
code. (I am not certain that a compiler would have been worse
than what appeared anyway.) Further more, the algorithm would
have been provable, closing off one major complaint.
I have always believed that the 4CC was true. I even would accept
a computer assisted proof. I have heard that people are working on
finding a smaller unavoidable set of reducible graphs. I hope that
there will soone be a more convincing argument. Until then, I still
classify the 4CC as a conjecture.
--
Gary Levin / Dept of CS / U of AZ / Tucson, AZ 85721 / (602) 621-4231chongo@nsc.UUCP (Landon C. Noll) (08/26/84)
as a P.S. to my last article: better proofs are always good to try for. often the search for a proof opens up vast new areas of research. searching for a simple proof which does not require may uncover some new areas. as an aside: Euler's Ph.D. paper contained 4 new proofs of the fundimental theorm of Algebra. chongo <> /\../\ -- "Aw Ping-Puckety Yung Tiug Too!! Nee! Nee! Yaaaoooowwwwwwwww!!!!!" Wise King Otto of Happy Valley
ark@rabbit.UUCP (Andrew Koenig) (08/31/84)
Joseph Albert claims: "Even assuming that the algorithm and its coding is provably correct, calling its execution a proof simply baffles me ... The non-zero probability that there was a hardware error implies there is a non-zero probability that the "proof" is wrong." I seem to recall that one of the referees wrote a completely new implementation of the algorithm from scratch and ran it on a different machine, getting the same results.
gwyn@brl-tgr.ARPA (Doug Gwyn <gwyn>) (09/02/84)
In any event, there is ALWAYS a non-zero probability that a mathematical proof is wrong. People are no more infallible than machines.
joseph@hp-pcd.UUCP (09/18/84)
Funny, nobody else seems to know about this other execution
of this. From where do you know it?
(I find it hard to imagine a referee willing to burn several
megahours of their computer time)