Marijn Heule
{{Short description|Dutch computer scientist}}
{{Use mdy dates|date=April 2021}}
{{Infobox person
| name = Marijn Heule
| birth_date = {{Birth date and age|1979|3|12}}
| birth_place = Rijnsburg, The Netherlands
| alma_mater = Delft University of Technology
| occupation = Associate professor
| employer = Carnegie Mellon University
| known_for = Using SAT solvers to solve mathematical conjectures
| website = http://www.cs.cmu.edu/~mheule/
}}
Marienus Johannes Hendrikus Heule (born March 12, 1979, at Rijnsburg, The Netherlands){{Cite news |last=Calmthout |first=Martijn van |date=6 June 2016 |title=Bewijs dat nét op 200 laptops past |language=Dutch |pages=23 |work=de Volkskrant |url=https://www.cs.utexas.edu/users/marijn/VKN-583245.pdf |url-status=live |access-date=11 May 2021 |archive-url=https://web.archive.org/web/20220105040701/https://www.cs.utexas.edu/users/marijn/VKN-583245.pdf |archive-date=5 January 2022}}{{Cite web|last=Heule|first=Marijn|date=20 August 2019|title=Marijn J.H. Heule|url=http://www.cs.cmu.edu/~mheule/resume.pdf|access-date=15 June 2021|website=www.cs.cmu.edu}} is a Dutch computer scientist at Carnegie Mellon University who studies SAT solvers. Heule has used these solvers to resolve mathematical conjectures such as the Boolean Pythagorean triples problem, Schur's theorem number 5, and Keller's conjecture in dimension seven.
Career
Heule received a PhD at Delft University of Technology, in the Netherlands, in 2008. He was a research scientist, later a research assistant professor, at the University of Texas at Austin from 2012 to 2019. Since 2019, he has been an associate professor in the Computer Science Department at Carnegie Mellon University.File:Ptn-7824-zoom-1.png
In May 2016 he, along with Oliver Kullmann and Victor W. Marek, used SAT solving to solve the Boolean Pythagorean triples problem.{{Cite journal|last=Lamb|first=Evelyn|date=May 26, 2016|title=Two-hundred-terabyte maths proof is largest ever|journal=Nature|volume=534|issue=7605|pages=17–18|bibcode=2016Natur.534...17L|doi=10.1038/nature.2016.19990|pmid=27251254|doi-access=free}}{{Cite web|last=Hartnett|first=Kevin|title=Computer Scientists Attempt to Corner the Collatz Conjecture|url=https://www.quantamagazine.org/can-computers-solve-the-collatz-conjecture-20200826/|access-date=March 8, 2021|website=Quanta Magazine|date=August 26, 2020 }} The statement of the theorem they proved is{{math theorem|The set {1, . . . , 7824} can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for {1, . . . , 7825}.
}}To prove this theorem, the possible colorings of {1, ..., 7825} were divided into a trillion subcases using a heuristic. Each subclass was then solved a Boolean satisfiability solver. Creating the proof took about 4 CPU-years of computation over a period of two days on the Stampede supercomputer at the Texas Advanced Computing Center and generated a 200 terabyte propositional proof (which was compressed to 68 gigabytes in the form of the list of subcases used). The paper describing the proof was published in the SAT 2016 conference,{{Cite conference|last1=Heule|first1=Marijn J. H.|last2=Kullmann|first2=Oliver|last3=Marek|first3=Victor W.|author3-link=Victor W. Marek|year=2016|editor1-last=Creignou|editor1-first=Nadia|editor2-last=Le Berre|editor2-first=Daniel|title=Theory and Applications of Satisfiability Testing – SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings|series=Lecture Notes in Computer Science|volume=9710|pages=228–245|arxiv=1605.00723|doi=10.1007/978-3-319-40970-2_15|isbn=978-3-319-40969-6 |contribution=Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer}} where it won the best paper award. A $100 award that Ronald Graham originally offered for solving this problem in the 1980s was awarded to Heule.
He used SAT solving to prove that Schur number 5 was 160 in 2017.{{Cite arXiv |eprint=1711.08076 |first=Marijn J. H. |last=Heule |title=Schur Number Five|year=2017 |class=cs.LO }} He proved Keller's conjecture in dimension seven in 2020.{{Cite web|last=Hartnett|first=Kevin|title=Computer Search Settles 90-Year-Old Math Problem|url=https://www.quantamagazine.org/computer-search-settles-90-year-old-math-problem-20200819/|access-date=March 8, 2021|website=Quanta Magazine|date=August 19, 2020 }}
In 2018, Heule and Scott Aaronson received funding from the National Science Foundation to apply SAT solving to the Collatz conjecture.
In 2023 together with Subercaseaux, he proved that the packing chromatic number of the infinite square grid is 15{{Cite arXiv |last1=Subercaseaux |first1=Bernardo |last2=Heule |first2=Marijn J. H. |date=2023-01-23 |title=The Packing Chromatic Number of the Infinite Square Grid is 15 |class=cs.DM |eprint=2301.09757 }}{{Cite web |last=Hartnett |first=Kevin |date=2023-04-20 |title=The Number 15 Describes the Secret Limit of an Infinite Grid |url=https://www.quantamagazine.org/the-number-15-describes-the-secret-limit-of-an-infinite-grid-20230420/ |access-date=2023-04-20 |website=Quanta Magazine |language=en}}
See also
References
{{reflist}}
External links
- [http://www.cs.cmu.edu/~mheule/ Official website]
- [https://www.cs.utexas.edu/users/marijn/ Old official website at UT Austin]
{{authority control}}
{{DEFAULTSORT:Heule, Marijn}}
Category:Dutch computer scientists
Category:Delft University of Technology alumni
Category:University of Texas at Austin faculty