= Marijn Heule
{c}
= Marijn J. H. Heule
{c}
{synonym}
<Marijn Heule> is a <computer scientist> whose work connects <Boolean satisfiability> solving with machine-checkable mathematical proofs. With <Emre Yolcu> and <Xinyu Wu>, he studied proofs of the colouring requirements of <Mycielski graphs>.<Mycielski graphs and PR proofs by Emre Yolcu and others>[Author byline and abstract]{ref}
Their study separates two questions: does a short proof exist in a specified proof system, and can an automated solver find it efficiently? Constructing and checking a proof answers the first without automatically answering the second. The distinction helps explain why stronger proof rules alone do not settle the practical difficulty of proof search.<Mycielski graphs and PR proofs by Emre Yolcu and others>[Abstract and introduction, proof construction and CDCL experiments]{ref}
\Image[https://csd.cmu.edu/sites/default/files/2023-09/Heule-CSD-Direcory-2019.jpg]
{title=Portrait of <Marijn Heule>}
{description=Portrait identified on the https://csd.cmu.edu/people/faculty/marijn-heule[Carnegie Mellon University profile].}
{width=240}
Back to article page
