Марин Дж. Хеул - американский ученый-компьютерщик из Университета Карнеги-Меллона . Heule разработал доказательства решения SAT для решения математических задач, включая булеву задачу о троек Пифагора , теорему Шура номер 5 и гипотезу Келлера в размерности семь.
Карьера [ править ]
Хеул получил докторскую степень в Делфтском технологическом университете в Нидерландах в 2008 году и был доцентом-исследователем Техасского университета в Остине и адъюнкт-профессором факультета компьютерных наук Университета Карнеги-Меллона . [1] [2]
В мае 2016 года Марин Хеул вместе с Оливером Куллманном и Виктором Мареком решила проблему булевых пифагоровых троек с помощью компьютерного доказательства и решения SAT . [3] Утверждение доказанной теоремы таково:
Теорема - множество {1,. . . , 7824} можно разбить на две части, так что ни одна часть не содержит пифагорова тройку, а это невозможно для {1,. . . , 7825}. [4]
Для чисел до 7825 существует 2 7825 ≈ 3,63 × 10 2355 возможных раскрасок . Эти возможные раскраски были логически и алгоритмически сужены до примерно триллиона (все еще очень сложных) случаев, и они были исследованы с помощью решателя логической выполнимости . Создание доказательства заняло около 4 процессорных лет вычислений в течение двух дней на суперкомпьютере Stampede в Техасском центре передовых вычислений и сгенерировало предположительное доказательство объемом 200 терабайт, которое было сжато до 68 гигабайт.
Статья с описанием доказательства была опубликована на конференции SAT 2016 [4], где получила награду за лучшую работу. [4] В 1980-х годах Рональд Грэм предложил премию в 100 долларов за решение проблемы, которая была присуждена Heule. [5]
У Хойлера также есть компьютеризированный метод доказательства SAT для решения числа Шура 5 в 2017 году и гипотезы Келлера в размерности семь в 2020 году. [6] [7]
В 2018 году Хьюле и Скотт Ааронсон получили финансирование от Национального научного фонда для применения решения SAT к гипотезе Коллатца . [6]
Ссылки [ править ]
- ^ "Marijn JH Heule" . cs.utexas.edu . Проверено 8 марта 2021 года .
- ^ "Marijn JH Heule" . cs.cmu.edu . Проверено 8 марта 2021 года .
- ↑ Лэмб, Эвелин (26 мая 2016 г.). «Математическое доказательство в двести терабайт - самое большое доказательство за всю историю» . Природа . 534 (7605): 17–18. Bibcode : 2016Natur.534 ... 17L . DOI : 10.1038 / nature.2016.19990 . PMID 27251254 .
- ^ a b c Heule, Marijn JH; Куллманн, Оливер; Марек, Виктор В. (2016). «Решение и проверка булевых пифагоровых троек с помощью Cube-and-Conquer». In Creignou, Надя; Ле Берр, Даниэль (ред.). Теория и приложения тестирования выполнимости - SAT 2016: 19-я Международная конференция, Бордо, Франция, 5-8 июля 2016 г., Материалы . Конспект лекций по информатике. 9710 . С. 228–245. arXiv : 1605.00723 . DOI : 10.1007 / 978-3-319-40970-2_15 .
- ↑ Лэмб, Эвелин (26 мая 2016 г.). «Математическое доказательство в двести терабайт - самое большое доказательство за всю историю» . Природа . 534 (7605): 17–18. Bibcode : 2016Natur.534 ... 17L . DOI : 10.1038 / nature.2016.19990 . PMID 27251254 .
- ^ а б Хартнетт, Кевин. "Компьютерный поиск решает математическую проблему 90-летней давности" . Журнал Quanta . Проверено 8 марта 2021 .
- ^ Хартнетт, Кевин. «Попытка компьютерных ученых опровергнуть гипотезу Коллатца» . Журнал Quanta . Проверено 8 марта 2021 .
