学海网

湖南文理学院算法设计与分析课程设计报告：四色定理说明以及方法说明
一.四色定理的历史
四色地图的一个例子四色定理指出每个可以画出来的地图都可以至多用4种颜色来上色，而且没有两个相接的区域会是相同的颜色。被称为相接的两个区域是指他们共有一段边界，而不是一个点。 这一定理最初是由Francis Guthrie在1853年提出的猜想。很明显，3种颜色不会满足条件，而且也不难证明5种颜色满足条件且绰绰有余。但是，直到1977年四色猜想才最终由Kenneth Appel 和Wolfgang Haken证明。他们得到了J. Koch在算法工作上的支持。
证明方法将地图上的无限种可能情况减少为1,936种状态（稍后减少为1,476种），这些状态由计算机一个挨一个的进行检查。这一工作由不同的程序和计算机独立的进行了复检。　1879年，肯普曾宣布他证明了四色问题。他的证明虽然在11年后被数学家赫伍德否定了，但是人们认为他的证明思路，有很多可取之处。20世纪以来，许多人一直在继续按照他的思路，推进着四色问题的证明工作，并且取得了不少成就。可惜这些成就所提供的检验方法太复杂，人们难以实现。例如有人在1970年设计的方案，用当时的计算机来算，也需要连续不断地工作十万个小时，也就是说，要连续不断地计算11年以上，才能得出结论，所以难以证实。之后，人们又大大地改进了证明方案，而且计算机的能力及其使用方法也有了飞快的进步，为机器证明四色猜想创造了条件。
.......