Марин Хюле
Марин Хюле | |
|---|---|
| Рожденный | 12 марта 1979 г. |
| Альма-матер | Делфтский технологический университет |
| Занятие | Доцент |
| Работодатель | Университет Карнеги-Меллон |
| Известный | Использование решателей SAT для решения математических гипотез |
| Веб-сайт | http://www.cs.cmu.edu/~mheule/ |
Мариенус Йоханнес Хендрикус Хойле (родился 12 марта 1979 года в Рейнсбурге , Нидерланды ) [1] [2] — голландский ученый-компьютерщик из Университета Карнеги-Меллона, изучающий решатели SAT . Хойле использовал эти решатели для решения математических гипотез, таких как проблема булевых троек Пифагора , теорема Шура номер 5 и гипотеза Келлера в седьмом измерении.
Карьера
[ редактировать ]Хойле получил докторскую степень в Делфтском технологическом университете в Нидерландах в 2008 году. С 2012 по 2019 год он был научным сотрудником, а затем доцентом-исследователем в Техасском университете в Остине. С 2019 года он является доцентом. на факультете компьютерных наук Университета Карнеги-Меллон . [2]
В мае 2016 года он вместе с Оливером Куллманном и Виктором В. Мареком использовал решение SAT для решения булевой задачи пифагорейских троек . [3] [4] Формулировка доказанной ими теоремы такова:
Теорема . Множество {1, . . . , 7824} можно разбить на две части так, чтобы ни одна часть не содержала пифагорову тройку, а для {1, . . . , 7825}. [5]
Чтобы доказать эту теорему, возможные раскраски {1, ..., 7825} были разделены на триллион подслучаев с помощью эвристики . Затем каждый подкласс решался с помощью решателя логической выполнимости . Создание доказательства заняло около 4 лет ЦП вычислений в течение двух дней на суперкомпьютере Stampede в Техасском вычислительном центре и привело к созданию пропозиционального доказательства объемом 200 терабайт (которое было сжато до 68 гигабайт в виде списка использованных подслучаев). ). [5] Статья с описанием доказательства была опубликована на конференции SAT 2016. [5] где он получил награду за лучшую бумагу. [5] Премия в 100 долларов, которую Рональд Грэм первоначально предложил за решение этой проблемы в 1980-х годах, была присуждена Хойле. [3]
Он использовал решение SAT, чтобы доказать, что номер Шура 5 в 2017 году был 160. [4] [6] Он доказал гипотезу Келлера в седьмом измерении в 2020 году. [7]
В 2018 году Хойл и Скотт Ааронсон получили финансирование от Национального научного фонда на применение решения SAT к гипотезе Коллатца . [7]
В 2023 году вместе с Суберказо он доказал, что хроматическое число упаковки бесконечной квадратной сетки равно 15. [8] [9]
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ Калмтаут, Мартейн ван (6 июня 2016 г.). «Доказательство того, что его можно разместить только на 200 ноутбуках» (PDF) . де Фолькскрант (на голландском языке). п. 23. Архивировано (PDF) из оригинала 5 января 2022 года . Проверено 11 мая 2021 г.
- ^ Jump up to: а б Хойле, Марин (20 августа 2019 г.). «Марейн Дж. Х. Хойле» (PDF) . www.cs.cmu.edu . Проверено 15 июня 2021 г.
- ^ Jump up to: а б Лэмб, Эвелин (26 мая 2016 г.). «Доказательство по математике объемом в двести терабайт — самое большое за всю историю» . Природа . 534 (7605): 17–18. Бибкод : 2016Natur.534...17L . дои : 10.1038/nature.2016.19990 . ПМИД 27251254 .
- ^ Jump up to: а б Хартнетт, Кевин. «Ученые-компьютерщики пытаются опровергнуть гипотезу Коллатца» . Журнал Кванта . Проверено 8 марта 2021 г.
- ^ Jump up to: а б с д Хойле, Марин Дж. Х.; Куллманн, Оливер; Марек, Виктор В. (2016). «Решение и проверка булевой задачи о тройках Пифагора с помощью Cube and Conquer». В Креньу, Надя; Ле Берр, Даниэль (ред.). Теория и применение тестирования выполнимости – SAT 2016: 19-я Международная конференция, Бордо, Франция, 5-8 июля 2016 г., Материалы . Конспекты лекций по информатике. Том. 9710. стр. 228–245. arXiv : 1605.00723 . дои : 10.1007/978-3-319-40970-2_15 .
- ^ Хойле, Марин Дж. Х. (2017). «Шур номер пять». arXiv : 1711.08076 [ cs.LO ].
- ^ Jump up to: а б Хартнетт, Кевин. «Компьютерный поиск решает 90-летнюю математическую задачу» . Журнал Кванта . Проверено 8 марта 2021 г.
- ^ Суберказо, Бернардо; Хойле, Марин Дж. Х. (23 января 2023 г.). «Упаковочное хроматическое число бесконечной квадратной сетки равно 15». arXiv : 2301.09757 [ cs.DM ].
- ^ Хартнетт, Кевин (20 апреля 2023 г.). «Число 15 описывает тайный предел бесконечной сетки» . Журнал Кванта . Проверено 20 апреля 2023 г.
Внешние ссылки
[ редактировать ]| Международный | |
|---|---|
| Национальный | |
| Другой | |
