Pushing Blocks via Checkable Gadgets: PSPACE-completeness of Push-1F and Block/Box Dude
Hayashi Ani, Lily Chung, Erik D. Demaine, Jenny Diomidova, Della, Hendrickson, Jayson Lynch

TL;DR
This paper establishes the PSPACE-completeness of Push-1F and Block Dude puzzles, using a novel framework of checkable gadgets to analyze the computational complexity of these popular video game-inspired puzzles.
Contribution
It introduces a new framework for checkable gadgets that extends existing motion-planning frameworks, proving PSPACE-completeness for Push-1F, Push-k, and Block Dude puzzles.
Findings
Push-1F is PSPACE-complete.
Block Dude with liftable or pushable blocks is PSPACE-complete.
New checkable gadgets framework supports complex reductions.
Abstract
We prove PSPACE-completeness of the well-studied pushing-block puzzle Push-1F, a theoretical abstraction of many video games (introduced in 1999). The proof also extends to Push- for any . We also prove PSPACE-completeness of two versions of the recently studied block-moving puzzle game with gravity, Block Dude - a video game dating back to 1994 - featuring either liftable blocks or pushable blocks. Two of our reductions are built on a new framework for "checkable" gadgets, extending the motion-planning-through-gadgets framework to support gadgets that can be misused, provided those misuses can be detected later.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Advanced Malware Detection Techniques
