Теорема про чотири фарби — розфарбовування графів та комп’ютерне доведення

1. Теорема та її історія

Теорема про чотири фарби: за будь-якого поділу площини на суцільні регіони ці регіони можна розфарбувати щонайбільше чотирма фарбами так, щоб жодні два сусідні регіони не мали однакового кольору. (Два регіони є сусідніми, якщо вони мають спільний відрізок межі додатної довжини; кутові точки не рахуються.)

• 1852: Френсіс Ґатрі помічає властивість чотирьох фарб, розфарбовуючи карту англійських графств, і запитує свого брата Фредеріка, який звертається до Огастеса де Моргана.
• 1879: Альфред Кемпе публікує нібито доведення з використанням «ланцюгів Кемпе» — техніки, що збереглася в сучасних доведеннях, хоча повне міркування виявилося хибним.
• 1880: Пітер Тейт пропонує інший підхід через гамільтонові цикли — також згодом визнаний недостатнім.
• 1890: Персі Гівуд знаходить помилку в доведенні Кемпе, але рятує його, доводячи слабшу теорему про п’ять фарб.
• 1976: Кеннет Аппель та Вольфганг Гакен використовують комп’ютер для перевірки 1936 звідних конфігурацій — нарешті повне доведення.
• 1997: Ніл Робертсон, Деніел Сандерс, Пол Сеймур та Робін Томас отримують чистіше комп’ютерне доведення з використанням 633 конфігурацій.
• 2005: Жорж Гонтьє формально верифікує теорему в Coq, системі-помічнику доведень.

2. Формулювання мовою теорії графів

Задача розфарбовування карти еквівалентна задачі розфарбовування графа. Перетворіть карту на планарний граф: одна вершина на регіон, одне ребро між вершинами, регіони яких мають спільну межу. Тоді теорема про чотири фарби стверджує: кожен планарний граф є 4-розфарбовуваним.

3. Теорема про п’ять фарб

Простіша теорема про п’ять фарб має витончене доведення сильною індукцією, що не потребує комп’ютера:

1. Кожен планарний граф має вершину v степеня ≤ 5 (за міркуванням із формулою Ейлера).
2. Вилучіть v; за індукцією решта графа є 5-розфарбовуваною.
3. Поверніть v. Якщо її ≤5 сусідів використовують ≤4 фарб, призначте v п’яту фарбу. Готово.
4. Якщо всі 5 сусідів використовують усі 5 фарб (у циклічному порядку c₁, c₂, c₃, c₄, c₅ навколо v), потрібен прийом Кемпе:
5. Розгляньте підграф, породжений фарбами c₁ та c₃. Якщо v₁ та v₃ належать до різних зв’язних компонент, поміняйте фарби в компоненті v₁ — тепер і v₁, і v₃ використовують фарби з {c₁,c₃}, звільняючи одну для v.
6. Якщо вони в одній компоненті: існує c₁-c₃-шлях від v₁ до v₃. Тоді v₂ та v₄ мають належати до різних компонент c₂-c₄-підграфа (вони не можуть перетнути шлях). Поміняйте фарби в компоненті v₂, щоб звільнити c₂ для v.

Те, що це не вдається безпосередньо поширити на чотири фарби, і є причиною, чому доведення для чотирьох фарб потребує перевірки тисяч конфігурацій — «виправлення» Кемпе не завжди працює для кроку 4, коли намагаємося довести, що чотирьох достатньо.

4. Доведення Аппеля–Гакена

Стратегія доведення використовує два ключові поняття:

• Неминучий набір: набір конфігурацій такий, що кожен планарний граф мусить містити принаймні одну з них.
• Звідна конфігурація: конфігурація, яку можна «звести» — якщо граф містить її, то граф є 4-розфарбовуваним тоді й лише тоді, коли є таким менший граф. (По суті: ми завжди можемо поширити 4-розфарбовування з решти графа, щоб включити цю частину.)

Аппель і Гакен знайшли неминучий набір із 1936 конфігурацій і довели, що кожна звідна. Разом це гарантує: будь-який планарний граф містить звідну конфігурацію, тож його можна розфарбувати чотирма фарбами індукцією за розміром.

5. Жадібне розфарбовування графів

Для практичного розфарбовування графів (не обов’язково оптимального) жадібний алгоритм послідовно призначає кожній вершині найменшу доступну фарбу:

function greedyColor(graph) {
  const color = new Array(graph.n).fill(-1);
  for (let v = 0; v < graph.n; v++) {
    const usedColors = new Set(
      graph.adj[v].filter(u => color[u] !== -1).map(u => color[u])
    );
    let c = 0;
    while (usedColors.has(c)) c++;
    color[v] = c;
  }
  return color;
}

Жадібне розфарбовування використовує щонайбільше Δ(G) + 1 фарб (де Δ(G) — максимальний степінь), але може використати більше, ніж хроматичне число χ(G). Порядок вершин має велике значення — оптимальні порядки включають «найбільші першими» (за степенем), «найменші останніми» та DSatur (евристику динамічного насичення).

Знаходження точного хроматичного числа χ(G) загалом є NP-повним. Для планарних графів 4-розфарбовуваність завжди гарантована, але ефективне (за поліноміальний час) знаходження 4-розфарбовування досі є відкритою проблемою — ми знаємо лише, що P-алгоритми існують для {2,3}-розфарбовування планарних графів.

6. Хроматичний многочлен

Хроматичний многочлен P(G, k) підраховує кількість правильних k-розфарбовувань графа G:

Хроматичне число χ(G) — це найменше k > 0, для якого P(G, k) > 0. Обчислення P(G, k) загалом є #P-складним — експоненційно важчим, ніж просто визначити розфарбовуваність.

7. Застосування поза картами

• Розподіл регістрів: в оптимізації компіляторів змінні є вершинами; ребра з’єднують змінні, що «живі» одночасно. Розфарбовування ≤ K фарбами = розподіл по K регістрах процесора без витіснення в пам’ять.
• Призначення частот: стільниковим вежам (вершинам) у радіомережі потрібні різні частоти, якщо їхні зони покриття перекриваються — мінімальне хроматичне число мінімізує потрібний спектр.
• Складання розкладу: завдання (вершини), що спільно використовують ресурси, є суміжними; мінімальне розфарбовування = мінімальна кількість потрібних часових слотів.
• Судоку: судоку 9×9 — це задача розфарбовування графа на 81 вершині дев’ятьма фарбами, де обмеження рядка/стовпця/блока визначають ребра.
• Рендеринг на GPU — розфарбовування обмежень PBD: як описано у статті про динаміку на основі положень (Position-Based Dynamics), обмеження, що спільно використовують вершини, утворюють граф — його розфарбовування на групи уможливлює паралельну обробку на GPU.