Marijn J. H. Heule

activity

20102023

most citedSolving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer

203 citations · 391 across the 22 of their papers we have counts for

collaborators

Showing 2022Show all

2 papers · 1 filter

cs.LO2022

Exponential separations using guarded extension variables

Emre Yolcu, Marijn J. H. Heule

We study the complexity of proof systems augmenting resolution with inference rules that allow, given a formula $Γ$ in conjunctive normal form, deriving clauses that are not necess…

cs.LO2022

Towards the shortest DRAT proof of the Pigeonhole Principle

Isaac Grosof, Naifeng Zhang, Marijn J. H. Heule

The Pigeonhole Principle (PHP) has been heavily studied in automated reasoning, both theoretically and in practice. Most solvers have exponential runtime and proof length, while so…