Push-1 is PSPACE-complete, and the automated verification of motion planning gadgets

Zachary DeStefano, Bufang Liang

Push-1 is one of the simplest abstract frameworks for motion planning; however, the complexity of deciding if a Push-1 problem can be solved was a several-decade-old open question.…