Marijn Heule

Marijn Heule is a researcher at the University of Texas at Austin, who specialises in solving large combinatorial problems using computer techniques such as SAT solvers. In 2016, Heule solved the Boolean Pythagorean triples problem with a distributed SAT solver, producing a record-breaking 200-terabyte proof of unsatisfiability.

Marijn Heule
Born March 12, 1979
Residence Unknown
Nationality Dutch
Institutions University of Texas at Austin
Alma mater Delft University of Technology

He contributed to the development of several SAT solvers, including lingeling and the lookahead SAT solver march-cc, and adapted the Glucose SAT solver to support incremental CNF input files. The resulting program, iglucose, was further adapted by Tomas Rokicki to be interactively operable through named pipes, allowing it to be used in Adam P. Goucher's knightship search program, ikpx.

Marijn also discovered Garden of Eden 6, the smallest symmetric Garden of Eden, in collaboration with Christiaan Hartman, Kees Kwekkeboom, and Alain Noels.

Patterns found by Marijn Heule

G

gollark: "THE KNOWLEDGE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF UNLEASHING INDESCRIBABLE HORRORS THAT SHATTER YOUR PSYCHE AND SET YOUR MIND ADRIFT IN THE UNKNOWABLY INFINITE COSMOS.", sort of thing?
gollark: And make it large?
gollark: So, how do you plan to move it all to the front?
gollark: Consider: There's a lot of "fine print", hence why it's small.
gollark: If people do not bother to read things, that is their apioproblem.
This article is issued from Conwaylife. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.