Marijn Heule

Last updated

Marijn Heule
Born (1979-03-12) March 12, 1979 (age 44)
Rijnsburg, The Netherlands
Alma mater Delft University of Technology
OccupationAssociate professor
EmployerCarnegie Mellon University
Known forUsing 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) [1] [2] 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.

Contents

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. [2]

Visualization of a solution of the Pythagorean Triples Problem Ptn-7824-zoom-1.png
Visualization of a solution of the Pythagorean Triples Problem

In May 2016 he, along with Oliver Kullmann and Victor W. Marek, used SAT solving to solve the Boolean Pythagorean triples problem. [3] [4] The statement of the theorem they proved is

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}. [5]

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). [5] The paper describing the proof was published in the SAT 2016 conference, [5] where it won the best paper award. [5] A $100 award that Ronald Graham originally offered for solving this problem in the 1980s was awarded to Heule. [3]

He used SAT solving to prove that Schur number 5 was 160 in 2017. [4] [6] He proved Keller's conjecture in dimension seven in 2020. [7]

In 2018, Heule and Scott Aaronson received funding from the National Science Foundation to apply SAT solving to the Collatz conjecture. [7]

In 2023 together with Subercaseaux, he proved that the packing chromatic number of the infinite square grid is 15 [8] [9]

See also

Related Research Articles

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

The P versus NP problem is a major unsolved problem in theoretical computer science. In informal terms, it asks whether every problem whose solution can be quickly verified can also be quickly solved.

Proof by exhaustion, also known as proof by cases, proof by case analysis, complete induction or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases or sets of equivalent cases, and where each type of case is checked to see if the proposition in question holds. This is a method of direct proof. A proof by exhaustion typically contains two stages:

  1. A proof that the set of cases is exhaustive; i.e., that each instance of the statement to be proved matches the conditions of one of the cases.
  2. A proof of each of the cases.

In computational complexity theory, a natural proof is a certain kind of proof establishing that one complexity class differs from another one. While these proofs are in some sense "natural", it can be shown that no such proof can possibly be used to solve the P vs. NP problem.

In computational complexity theory, the Cook–Levin theorem, also known as Cook's theorem, states that the Boolean satisfiability problem is NP-complete. That is, it is in NP, and any problem in NP can be reduced in polynomial time by a deterministic Turing machine to the Boolean satisfiability problem.

In computational complexity theory, Karp's 21 NP-complete problems are a set of computational problems which are NP-complete. In his 1972 paper, "Reducibility Among Combinatorial Problems", Richard Karp used Stephen Cook's 1971 theorem that the boolean satisfiability problem is NP-complete to show that there is a polynomial time many-one reduction from the boolean satisfiability problem to each of 21 combinatorial and graph theoretical computational problems, thereby showing that they are all NP-complete. This was one of the first demonstrations that many natural computational problems occurring throughout computer science are computationally intractable, and it drove interest in the study of NP-completeness and the P versus NP problem.

A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.

In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

Satplan is a method for automated planning. It converts the planning problem instance into an instance of the Boolean satisfiability problem, which is then solved using a method for establishing satisfiability such as the DPLL algorithm or WalkSAT.

In computational complexity theory, the PCP theorem states that every decision problem in the NP complexity class has probabilistically checkable proofs of constant query complexity and logarithmic randomness complexity.

The Valiant–Vazirani theorem is a theorem in computational complexity theory stating that if there is a polynomial time algorithm for Unambiguous-SAT, then NP = RP. It was proven by Leslie Valiant and Vijay Vazirani in their paper titled NP is as easy as detecting unique solutions published in 1986. The proof is based on the Mulmuley–Vazirani–Vazirani isolation lemma, which was subsequently used for a number of important applications in theoretical computer science.

MAX-3SAT is a problem in the computational complexity subfield of computer science. It generalises the Boolean satisfiability problem (SAT) which is a decision problem considered in complexity theory. It is defined as:

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when x is true, so the solver should return "satisfiable". Since the introduction of algorithms for SAT in the 1960s, modern SAT solvers have grown into complex software artifacts involving a large number of heuristics and program optimizations to work efficiently.

In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula is satisfiable because it is true when and , while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not.

In computer science, the Sharp Satisfiability Problem is the problem of counting the number of interpretations that satisfy a given Boolean formula, introduced by Valiant in 1979. In other words, it asks in how many ways the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. For example, the formula is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments, , and, we have

The Boolean Pythagorean triples problem is a problem from Ramsey theory about whether the positive integers can be colored red and blue so that no Pythagorean triples consist of all red or all blue members. The Boolean Pythagorean triples problem was solved by Marijn Heule, Oliver Kullmann and Victor W. Marek in May 2016 through a computer-assisted proof.

7825 is the natural number following 7824 and preceding 7826.

References

  1. ↑ Calmthout, Martijn van (June 6, 2016). "Bewijs dat nét op 200 laptops past" (PDF). de Volkskrant (in Dutch). p. 23. Archived (PDF) from the original on January 5, 2022. Retrieved May 11, 2021.
  2. 1 2 Heule, Marijn (August 20, 2019). "Marijn J.H. Heule" (PDF). www.cs.cmu.edu. Retrieved June 15, 2021.
  3. 1 2 Lamb, Evelyn (May 26, 2016). "Two-hundred-terabyte maths proof is largest ever". Nature. 534 (7605): 17–18. Bibcode:2016Natur.534...17L. doi: 10.1038/nature.2016.19990 . PMID   27251254.
  4. 1 2 Hartnett, Kevin. "Computer Scientists Attempt to Corner the Collatz Conjecture". Quanta Magazine . Retrieved March 8, 2021.
  5. 1 2 3 4 Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer". In Creignou, Nadia; Le Berre, Daniel (eds.). Theory and Applications of Satisfiability Testing – SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Lecture Notes in Computer Science. Vol. 9710. pp. 228–245. arXiv: 1605.00723 . doi:10.1007/978-3-319-40970-2_15.
  6. ↑ Heule, Marijn J. H. (2017). "Schur Number Five". arXiv: 1711.08076 [cs.LO].
  7. 1 2 Hartnett, Kevin. "Computer Search Settles 90-Year-Old Math Problem". Quanta Magazine . Retrieved March 8, 2021.
  8. ↑ Subercaseaux, Bernardo; Heule, Marijn J. H. (January 23, 2023). "The Packing Chromatic Number of the Infinite Square Grid is 15". arXiv: 2301.09757 [cs.DM].
  9. ↑ Hartnett, Kevin (April 20, 2023). "The Number 15 Describes the Secret Limit of an Infinite Grid". Quanta Magazine. Retrieved April 20, 2023.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.