Ученые из Университета Карнеги-Меллона решили последнюю, упрямую часть гипотезы Келлера — геометрическую проблему, над которой ученые ломали голову в течение 90 лет.
Структурируя головоломку как то, что компьютерные ученые называют проблемой выполнимости, исследователи решили решить эту проблему с помощью четырех месяцев безумного компьютерного программирования и всего 30 минут вычислений с использованием кластера компьютеров.
Решение было еще одним успеха для подхода пионеров по Marijn Хёль, доцент кафедры компьютерной науки , который присоединился CSD в августе прошлого года. Heule использовал решатель SAT — компьютерную программу, которая использует логику высказываний для решения задач удовлетворяемости (SAT), — чтобы преодолеть несколько устаревших математических задач, включая проблему троек Пифагора и число Шура 5.
Гипотеза, выдвинутая немецким математиком Эдуардом Отт-Генрихом Келлером, связана с мозаикой, а именно с тем, как покрыть область плитками одинакового размера без каких-либо пробелов или перекрытий. Гипотеза состоит в том, что по крайней мере две плитки должны иметь общее ребро, и это верно для пространств любого измерения.
Легко доказать, что это верно для двухмерных плиток и трехмерных кубов. К 1940 году эта гипотеза была подтверждена для всех измерений до шести. Однако в 1990 году математики доказали, что это не работает с размерностью 10 и выше.
Именно тогда гипотеза Келлера захватила воображение Макки, тогда еще студента Гавайского университета. Он был заинтригован своим офисом рядом с вычислительным кластером университета, потому что проблема могла быть переведена с помощью теории дискретных графов в форму, которую могли бы исследовать компьютеры. В этой форме, называемой графом Келлера, исследователи могли искать «клики» — подмножества элементов, которые соединяются без общего лица, тем самым опровергая гипотезу.
В 2002 году Макки сделал именно это, обнаружив клику в восьмом измерении. Тем самым он доказал, что гипотеза неверна в этом измерении и, в более широком смысле, в измерении девять.
Это оставило нерешенной гипотезу для седьмого измерения.
Когда Хеул приехал в CMU из Техасского университета в прошлом году, у него уже была репутация человека, использующего решатель SAT для решения давних открытых математических задач.
Решатель SAT требует структурирования проблемы с использованием пропозициональной формулы — (A или не B) и (B или C) и т. Д. — чтобы решатель мог исследовать все возможные переменные для комбинаций, которые удовлетворяют всем условиям.
Обладая 15-летним опытом, Heule умеет выполнять эти переводы. Одна из целей его исследования — разработать автоматизированное мышление, чтобы этот перевод мог выполняться автоматически, что позволит большему количеству людей использовать эти инструменты для решения своих проблем.
Даже при качественном переводе количество комбинаций, которые нужно было проверить в седьмом измерении, было ошеломляющим — число из 324 цифр — и решения не было видно даже с суперкомпьютером. Но Хеул и другие применили ряд уловок, чтобы уменьшить размер проблемы. Например, если одна конфигурация данных окажется неработоспособной, они могут автоматически отклонить другие комбинации, которые на нее полагаются. А поскольку большая часть данных была симметричной, программа могла исключить зеркальное отображение конфигурации, если бы она зашла в тупик в одном устройстве.
Используя эти методы, они сократили объем поиска примерно до миллиарда конфигураций. К этим усилиям присоединился доктор философии Дэвид Нарваез. студент Рочестерского технологического института, который осенью 2019 года был приглашенным исследователем.
Как только они запустили свой код на кластере из 40 компьютеров, они наконец получили ответ: гипотеза верна для седьмого измерения.
«Причина, по которой мы добились успеха, заключается в том, что Джон обладает многолетним опытом и пониманием этой проблемы, и мы смогли преобразовать ее в поиск, созданный компьютером», — сказал Хел.