Marijn Heule
Marijn Heule | |
|---|---|
| Urodzić się |
12 marca 1979 |
| Alma Mater | Politechnika w Delft |
| Zawód | Profesor nadzwyczajny |
| Pracodawca | Carnegie Mellon University |
| Znany z | Używanie solwerów SAT do rozwiązywania przypuszczeń matematycznych |
| Strona internetowa | http://www.cs.cmu.edu/~mheule/ |
Marienus Johannes Hendrikus Heule (urodzony 12 marca 1979 w Rijnsburgu w Holandii ) jest holenderskim informatykiem z Carnegie Mellon University , który bada rozwiązujące SAT . Heule użył tych solwerów do rozwiązania przypuszczeń matematycznych, takich jak boolowski problem trójek Pitagorasa , twierdzenie Schura numer 5 i przypuszczenie Kellera w wymiarze siódmym.
Kariera
Heule uzyskał stopień doktora na Delft University of Technology w Holandii w 2008 roku. W latach 2012-2019 był pracownikiem naukowym, później adiunktem na University of Texas w Austin . Od 2019 roku jest profesorem nadzwyczajnym na Wydziale Informatyki na Uniwersytecie Carnegie Mellon .
W maju 2016 roku wraz z Oliverem Kullmannem i Victorem W. Markiem wykorzystał rozwiązanie SAT do rozwiązania problemu trójek boolowskich Pitagorasa . Stwierdzenie twierdzenia, które udowodnili, jest
Twierdzenie — Zbiór {1, . . . , 7824} można podzielić na dwie części, tak że żadna część nie zawiera trójki pitagorejskiej, podczas gdy jest to niemożliwe dla {1, . . . , 7825}.
Aby udowodnić to twierdzenie, możliwe kolorowania {1, ..., 7825} podzielono na bilion podprzypadków za pomocą heurystyki . Każda podklasa została następnie rozwiązana za pomocą spełnialności boolowskiej . Stworzenie dowodu zajęło około 4 procesoro-lat obliczeń w ciągu dwóch dni na superkomputerze Stampede w Texas Advanced Computing Center i wygenerowało 200-terabajtowy dowód zdaniowy (który został skompresowany do 68 gigabajtów w postaci listy użytych przypadków podrzędnych ). Artykuł opisujący dowód został opublikowany na konferencji SAT 2016, gdzie zdobył nagrodę dla najlepszego artykułu. Nagroda w wysokości 100 dolarów Ronald Graham , który pierwotnie zaproponował rozwiązanie tego problemu w latach 80., został przyznany firmie Heule.
Użył rozwiązania SAT, aby udowodnić, że numer Schura 5 wynosił 160 w 2017 roku. Udowodnił hipotezę Kellera w wymiarze siódmym w 2020 roku.
W 2018 roku Heule i Scott Aaronson otrzymali fundusze od National Science Foundation na zastosowanie rozwiązania SAT do hipotezy Collatza .
Linki zewnętrzne
| Ogólny | |
|---|---|
| Biblioteki Narodowe | |
| Inny | |
