Відмінності між версіями «Проблема трійок Буля — Піфагора»

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку
[перевірена версія][перевірена версія]
м (автоматична заміна {{Не перекладено}} вікі-посиланнями на перекладені статті)
(Немає відмінностей)

Версія за 00:49, 21 лютого 2019

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

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

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

Проблема

Проблема трійок Буля-Піфагора виникла в теорії Рамсея, головним мотивом якої є заперечення абсолютного хаосу в достатньо великих системах [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. 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. ISBN 978-0-387-74640-1. doi:10.1007/978-0-387-74642-5. Процитовано 11 листопада 2016. 
  3. Shreevatsa, R (May 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 (May 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. с. 14 (proposed by Graham). Процитовано 10 листопада 2016. 
  6. Graham, Ron (2008). Old and New Problems and Results in Ramsey Theory. University of California, San Diego[en]. с. 6. Процитовано 10 листопада 2016. 
  7. Cooper, Joshua Cooper; Poirel, Chris (December 4, 2008). Note on the Pythagorean Triple System. 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. Процитовано 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 (June 11, 2016). Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. 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. 
  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 (September 4, 2016). How Hard, Really, is SAT?. Gödel's Lost Letter and P=NP. Процитовано 10 листопада 2016.