Marienus Johannes Hendrikus Heule (nacido el 12 de marzo de 1979 en Rijnsburg , Países Bajos ) [1] [2] es un informático holandés de la Universidad Carnegie Mellon que estudia los solucionadores SAT . Heule ha utilizado estos solucionadores para resolver conjeturas matemáticas como el problema de las ternas pitagóricas de Boole , el teorema número 5 de Schur y la conjetura de Keller en dimensión siete.
Heule recibió un doctorado en la Universidad Tecnológica de Delft , en los Países Bajos , en 2008. Fue científico investigador, más tarde profesor asistente de investigación, en la Universidad de Texas en Austin de 2012 a 2019. Desde 2019, ha sido profesor asociado en el Departamento de Ciencias de la Computación de la Universidad Carnegie Mellon . [2]
En mayo de 2016, junto con Oliver Kullmann y Victor W. Marek, utilizó la resolución SAT para resolver el problema de las ternas pitagóricas booleanas . [3] [4] El enunciado del teorema que demostraron es
Teorema — El conjunto {1, . . . , 7824} se puede dividir en dos partes, de modo que ninguna de ellas contenga una terna pitagórica, mientras que esto es imposible para {1, . . . , 7825}. [5]
Para demostrar este teorema, las posibles coloraciones de {1, ..., 7825} se dividieron en un billón de subcasos utilizando una heurística . Luego, cada subclase se resolvió con un solucionador de satisfacibilidad booleana . La creación de la prueba tomó alrededor de 4 años de CPU de computación durante un período de dos días en la supercomputadora Stampede en el Centro de Computación Avanzada de Texas y generó una prueba proposicional de 200 terabytes (que se comprimió a 68 gigabytes en forma de lista de subcasos utilizados). [5] El artículo que describe la prueba se publicó en la conferencia SAT 2016, [5] donde ganó el premio al mejor artículo. [5] Un premio de $100 que Ronald Graham ofreció originalmente por resolver este problema en la década de 1980 fue otorgado a Heule. [3]
Utilizó la resolución SAT para demostrar que el número de Schur 5 era 160 en 2017. [4] [6] Demostró la conjetura de Keller en dimensión siete en 2020. [7]
En 2018, Heule y Scott Aaronson recibieron financiación de la Fundación Nacional de Ciencias para aplicar la resolución SAT a la conjetura de Collatz . [7]
En 2023, junto con Subercaseaux, demostró que el número cromático de empaquetamiento de la cuadrícula cuadrada infinita es 15 [8] [9]