14 citations · 14 across the 2 of their papers we have counts for
3 papers
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…
Computational Complexity of Motion Planning of a Robot through Simple Gadgets
Erik D. Demaine, Isaac Grosof, Jayson Lynch +1
We initiate a general theory for analyzing the complexity of motion planning of a single robot through a graph of "gadgets", each with their own state, set of locations, and allowe…
Push-Pull Block Puzzles are Hard
Erik D. Demaine, Isaac Grosof, Jayson Lynch
This paper proves that push-pull block puzzles in 3D are PSPACE-complete to solve, and push-pull block puzzles in 2D with thin walls are NP-hard to solve, settling an open question…