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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку
Рональд Грем разом із Ердешем сформулював проблему трійок Буля — Піфагора в публікації 1980 року

Проблема трійок Буля — Піфагора полягає у відповіді на питання, чи можна поділити множину натуральних чисел на дві частини так, щоб у кожній частині не було жодної піфагорової трійки. Марійн Гейле[en], Олівер Кульман та Віктор Марек[en] 2016 року довели, що це можливо лише для і менших чисел. Для множини з чисел і більше такий поділ неможливий. Іншими словами, серед натуральних чисел , розфарбованих у два кольори, завжди знайдеться монохроматична трійка , і що .

У стислій формі результат записується через число Радо для рівняння Піфагора: .

Проблема[ред. | ред. код]

Річард Радо[en]

Проблема трійок Буля — Піфагора виникла в теорії Ремзі, головним мотивом якої є заперечення абсолютного хаосу в достатньо великих системах[1][2]. Проблема стосується питання, чи можна поділити множину натуральних чисел на дві частини так, щоб кожна частина не мала жодної піфагорової трійки, тобто таких , і що . У термінах фарбування чисел проблема виглядає так: чи можна розфарбувати натуральні числа у два кольори щоби жодна піфагорова трійка не була монохроматичною. Основні роботи теорії Ремзі, що пов'язані з проблемою трійок Буля — Піфагора, включають теореми Шура[en], ван дер Вардена та Радо[en][3].

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

[ред. | ред. код]

У грудні 2008 року Джошуа Купер і Кріс Пойрел надрукували перший приклад розподілу множини натуральних чисел на дві частини так, що кожна частина не мала жодної піфагорової трійки. На обчислення пішло сотні годин процесорного часу. Результат було представлено у вигляді панелі  чорних і білих квадратиків. Квадратик із координатами () задавав колір числа . Числа збільшувались знизу до гори, потім зліва направо[7][8].

2012 року Вільям Кей застосував алгоритм[en] Робіна Мосера та Габора Тардоса[en] та знайшов розв'язок проблеми трійок для множини [9].

[ред. | ред. код]

У травні 2015 року Келлен Маєрс і Дорон Зілбергер оприлюднили роботу зі втілення алгоритму здійсненності булевих формул (SAT) для обчислення чисел Радо, зокрема, для проблеми трійок Буля — Піфагора. Вони запровадили поняття дійсного розфарбовування[К 1], яке дає можливість знайти нижню межу для числа Радо. У результаті комп'ютерних обчислювань Маєрс і Зілбергер знайшли, що число Радо , та опублікували сертифікат існування дійсного розфарбовування множини у трьох формах:

  1. Рядок довжиною з елементів для позначення кольору всіх чисел у послідовності.
  2. Два списки чисел, що показує, у яку з двох частин потрапило кожне число під час розбивки.
  3. Панель червоних і синіх квадратиків, в якій нумерація квадратиків збільшується зліва направо, потім зверху донизу[10].

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

[ред. | ред. код]

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

[ред. | ред. код]

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

Теорема[ред. | ред. код]

Теорема 1. Множину натуральних чисел можна поділити на дві частини так, щоб кожна частина не мала жодної піфагорової трійки, але це не можливо для .

Доведення[ред. | ред. код]

Доведенням першого твердження теореми став позитивний приклад розфарбування двома кольорами натуральних чисел. Приклад проілюстровано панеллю  квадратиків трьох класів: двох пофарбованих і нефарбованого. До нефарбованого класу належать числа, що не входять до жодної піфагорової трійки, та деякі числа з трійок, чий колір не має значення. Нижній рядок у панелі займають числа , над ним — і так далі до верхнього рядка .


Науковці провели попередній аналіз усіх варіантів розфарбування чисел та зменшили обсяг доведення другого твердження теореми до близько трильйона () здебільшого досить складних варіантів. Теорема була доведена шляхом перебору всіх знайдених варіантів, використовуючи розв'язувач класу SAT Solver на 800 ядерному суперкомп'ютері Stampede у Комп’ютерному центрі Техаського університету[en] протягом двох днів. Розв'язувач задіяв парадигму cube-and-conquer (C&C) і спочатку розділяв задачу на мільйон підзадач (cubes). На другій фазі підзадачі розв'язували методом CDCL solver[К 2], що також має назву conquer solver.

Розмір файлу з доказами у форматі DRAT [К 3] сягнув 200 терабайтів. Із нього було виготовлено й заархівовано сертифікат розміром 68 гігабайтів. Для натуральних чисел існує декілька розв'язків проблеми, але для розв'язку не знайдено[12][13].

У термінології теорії Рамсея автори знайшли дійсне розфарбування для і довели, що число Радо для рівняння Піфагора у випадку двох кольорів дорівнює , або стисло:

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

Висвітлення та обговорення[ред. | ред. код]

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

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

Див. також[ред. | ред. код]

Коментарі[ред. | ред. код]

  1. Розфарбовування чисел множини (для деякого ) називається дійсним, якщо воно не має монохроматичних розв'язків цього рівняння. Трійка чисел називається монохроматичною в разі ідентичності значень функції розфарбування для кожного елемента: .
  2. CDCL — скорочення від Conflict-Driven Clause Learning[en] — кероване конфліктами навчання диз'юнктам
  3. DRAT — скорочення від англ. Deletion Resolution Asymmetric Tautology

Примітки[ред. | ред. код]

  1. а б Erdős, P.; Graham, R.L. (1980). Old and New Problems and Results in Combinatorial Number Theory (PDF). Université de Genève. Процитовано 10 листопада 2016.
  2. Soifer, Alexander (2009). The Mathematical Coloring Book. Mathematics of Coloring and the Colorful Life of Its Creators. New York: Springer-Verlag. с. xxvii. doi:10.1007/978-0-387-74642-5. ISBN 978-0-387-74640-1. Процитовано 11 листопада 2016.
  3. Shreevatsa, R (20 травня 2016). A simple-to-state problem has been resolved, and there's surprisingly little about this in the news. WordPress.com. Процитовано 10 листопада 2016.
  4. а б Lamb, Evelyn (26 травня 2016). Two-hundred-terabyte maths proof is largest ever. Nature. Процитовано 31 серпня 2016. (укр. 200 терабайт «математики»)
  5. Croot, Ernie; Lev, Vsevolod F. (2007). Open Problems in Additive Combinatorics (PDF): 14 (proposed by Graham). Процитовано 10 листопада 2016.
  6. Graham, Ron (2008). Old and New Problems and Results in Ramsey Theory (PDF). University of California, San Diego: 6. Процитовано 10 листопада 2016.
  7. Cooper, Joshua Cooper; Poirel, Chris (4 грудня 2008). Note on the Pythagorean Triple System (PDF). University of South Carolina, Virginia Tech. Процитовано 10 листопада 2016.
  8. Cooper, Joshua; Poirel, Chris (February 18, 2013 (Submitted on 20 Sep 2008)). Pythagorean Partition-Regularity and Ordered Triple Systems with the Sum Property. ArXiv.org. Процитовано 10 листопада 2016.
  9. Kay, William (2012). An Overview of the Constructive Local Lemma. Ann Arbor: University of South Carolina. ISBN 9781267319937. Архів оригіналу за 12 листопада 2016. Процитовано 10 листопада 2016.
  10. Myers, Kellen John (May, 2015). Computational Advances In Rado Numbers. New Brunswick, New Jersey: Rutgers, The State University of New Jersey. Процитовано 11 листопада 2016.
  11. Joshua Cooper, Ralph Overstreet (2015). Coloring so that no Pythagorean Triple is Monochromatic. ArXiv.org.
  12. Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek (2016). Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. ArXiv.org. doi:10.1007/978-3-319-40970-2_15.
  13. а б Everything's Bigger in Texas. University of Texas at Austin. 2016. Процитовано 31 серпня 2016.
  14. Heule, Marijn J. H.; Oliver Kullmann, Victor W. Marek (11 червня 2016). Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer (PDF). Theory and Applications of Satisfiability Testing – SAT 2016 (вид. Volume 9710 of the series Lecture Notes in Computer Science). Springer. с. 228—245. doi:10.1007/978-3-319-40970-2_15. Процитовано 31 серпня 2016. {{cite conference}}: Cite має пусті невідомі параметри: |розташування= та |авторлінк= (довідка)
  15. 19th International Conference on Theory and Applications of Satisfiability Testing. SAT 2016. July 5-8, 2016. Процитовано 31 серпня 2016.
  16. Dambeck, Holger (30.05.2016). Der längste Mathe-Beweis der Welt. Der Spiegel. Процитовано 10 листопада 2016.
  17. Lipton, RJ; Regan, KW (4 вересня 2016). How Hard, Really, is SAT?. Gödel's Lost Letter and P=NP. Процитовано 10 листопада 2016.