PSPACE 完备性：通过非确定性约束逻辑计算模型

我们提出了一种基于在带有顶点最小入流约束的加权有向图中反转边方向的非确定性计算模型。决定该简单图模型能否被操控以反转特定边的方向被证明是 PSPACE 完备的，通过从量化布尔公式进行归约。我们在各种特殊情况下的证明，包括平面图和高度受限顶点配置，其中一些对应于一种被动约束逻辑的类型。我们的框架受到（并且实际上是）Flake 和 Baum 开发的“通用 Rush Hour 逻辑”启发。我们通过给出简单归约表明该计算模型的重要性，展示了几类运动规划问题是 PSPACE-hard 的。我们的主要结果之一是，经典无限制滑动块拼图是 PSPACE-hard 的，即使块被限制为全部多米诺骨牌（1x2 块），目标仅为移动特定块。此结果可视为对现有结果的强化，即受限 Rush Hour 拼图是 PSPACE-complete 的，我们也给出了更简洁的证明。最后，我们强化了推送块拼图 Sokoban 是 PSPACE-complete 的的现有结果，表明即使不允许任何障碍物，Sokoban 也仍为 PSPACE-complete。