Проблема трійок Буля — Піфагора

Річард Радо

Проблема трійок Буля-Піфагора виникла в теорії Рамсея, головним мотивом якої є заперечення абсолютного хаосу в достатньо великих системах [1] [2]. Проблема стосується питання, чи можна поділити множину натуральних чисел ${\displaystyle \{1,2,3,...\}}$ на дві частини так, щоб кожна частина не мала жодної піфагорової трійки, тобто таких ${\displaystyle a}$, ${\displaystyle b}$ і ${\displaystyle c}$ що ${\displaystyle a^{2}+b^{2}=c^{2}}$. У термінах фарбування чисел проблема виглядає так: чи можна розфарбувати натуральні числа в два кольори щоби жодна піфагорова трійка не була монохроматичною. Основні роботи теорії Рамсея, що пов'язані з проблемою трійок Буля-Піфагора, включають теореми Шура, ван дер Вардена та Радо [3].

У 1980-х Рональд Грехем запропонував приз у розмірі 100 доларів тому, хто розв'яже цю проблему [4]. У 2007—2008 роках він нагадав, що проблема була сформульована ще в його публікації разом із Ердешем 1980 року [1], зазначив про обмаль даних, щоби вирішити проблему в той чи інший бік, і за Ердешевою традицією пообіцяв премію (250 $) за результат [5] [6].

У грудні 2008 року Джошуа Купер і Кріс Пойрел надрукували перший приклад розподілу множини натуральних чисел ${\displaystyle \{1,2,3,...,1344\}}$ на дві частини так, щоб кожна частина не мала жодної піфагорової трійки. На обчислювання пішло сотні годин процесорного часу. Результат представлено у вигляді панелі ${\displaystyle 53\times 25+19}$ чорних і білих квадратиків. Квадратик із координатами (${\displaystyle p,q}$) задавав колір числа ${\displaystyle n=25q+p}$. Числа збільшувались знизу до гори, потім зліва направо [7] [8].

2012 року Вільям Кей застосував алгоритм Робіна Мосера та Габора Тардоса та знайшов рішення проблеми трійок для множини ${\displaystyle \{1,2,3,...,1514\}}$ [9].

У травні 2015 року Келлен Маєрс і Дорон Зілбергер оприлюднили роботу зі втілення алгоритму здійсненності бульових формул (SAT) для вичислення чисел Радо, в тому числі стосовно проблеми трійок Буля-Піфагора. Вони ввели поняття дійсного розфарбовування [К 1], яке дає можливість знайти нижню межу для числа Радо. В результаті комп'ютерних обчислювань Маєрс і Зілбергер знайшли, що число Радо ${\displaystyle R_{2}(a^{2}+b^{2}=c^{2})>6500}$ і опублікували сертифікат існування дійсного розфарбовування множини ${\displaystyle \{1,2,3,...,6500\}}$ у трьох формах:

1. Рядок довжиною ${\displaystyle 6500}$ із елементів ${\displaystyle \{0,1\}}$ для позначення кольору всіх чисел у послідовності.
2. Два списки чисел, що показує в яку з двох частин потрапило кожне число при розбивці.
3. Панель ${\displaystyle 70\times 92+60}$ червоних і синіх квадратиків, в якій нумерація квадратиків збільшується зліва направо, потім зверху донизу [10].

У приведеній нижче візуалізаційній панелі червоний колір замінено на жовтий.

У травні 2015 року Джошуа Купер і Ральф Оверстріт розфарбували двома кольорами ${\displaystyle 7664}$ натуральних чисел ${\displaystyle \{1,2,3,...,7664\}}$ так, що всі піфагорові трійки були різнокольоровими [11].

Марійн Гейле, Олівер Кульман та Віктор Марек у травні 2016 року вирішили проблему трійок Буля-Піфагора за допомогою теореми 1.

Доведення

Доказом першого твердження теореми став позитивний приклад розфарбування двома кольорами ${\displaystyle 7824}$ натуральних чисел. Приклад проілюстровано панеллю ${\displaystyle 100\times 78+24}$ квадратиків трьох класів: двох пофарбованих і нефарбованого. До нефарбованого класу належать числа, що не входять до жодної піфагорової трійки, та деякі числа з трійок, чий колір не має значення. Нижній рядок у панелі займають числа ${\displaystyle \{1,2,3,...,100\}}$, над ним — ${\displaystyle \{101,...,200\}}$ і так далі до верхнього рядка ${\displaystyle \{7801,...,7824\}}$.

…

Науковці провели попередній аналіз усіх ${\displaystyle 2^{7825}\approx 3{,}6\cdot 10^{2355}}$ варіантів розфарбування ${\displaystyle 7825}$ чисел та зменшили обсяг доведення другого твердження теореми до близько трильйона (${\displaystyle 10^{12}}$) здебільшого досить складних варіантів. Теорема була доведена шляхом перебору всіх знайдених варіантів, використовуючи розв'язувач класу SAT Solver на 800 ядерному суперкомп'ютері Stampede у Комп’ютерному центрі Техаського університету протягом двох днів. Розв'язувач задіяв парадігму cube-and-conquer (C&C) і спочатку розділяв задачу на мільйон підзадач (cubes). На другій фазі підзадачі розв'язувалися методом CDCL solver [К 2], що також має назву conquer solver.

Розмір файлу з доказами у форматі DRAT [К 3] сягнув 200 терабайтів. З нього було виготовлено і заархівовано сертифікат розміром 68 гігабайтів. Для ${\displaystyle 7824}$ натуральних чисел існує декілька рішень проблеми, але для ${\displaystyle 7825}$ рішень не знайдено [12] [13].

У термінології теорії Рамсея автори знайшли дійсне розфарбування для ${\displaystyle N=7824}$ і довели, що число Радо для рівняння Піфагора у випадку двох кольорів дорівнює ${\displaystyle 7825}$, або стисло:

$${\displaystyle R_{2}(a^{2}+b^{2}=c^{2})=7825}$$

.

Стаття Марійн Гейле, Олівера Кульмана та Віктора Марека була обрана для доповіді на конференції SAT 2016, що відбулася в Бордо (Франція) в липні 2016 року, та була визнана найкращою роботою [14] [15].

Марійн Гейле зробив веб сторінку з поясненнями роботи для пересічних відвідувачів і лінками на файли з результатами [13]. На сторінці зібрані десятки посилань на публікації в ЗМІ та фахових виданнях, у тому числі в Nature[4] і Шпіґель [16], і соціальних мережах. Найзагальнішим постало питання, чи можна суперкомп'ютерні рішення взагалі вважати математикою?

Гейле зі співавторами намагалися знайти особливість знайденого числа ${\displaystyle 7825}$, але його сенс залишився незрозумілим [17].

• Розфарбовування графів
• Теорема Рамсея
• Теорема Шура
• Теорема ван дер Вардена
• Теорема Радо
• Задача здійсненності бульових формул (SAT)