PushPush is NP-hard in 2D
2021-02-11
This is a series of posts where I jot down my learnings from computer science papers I’ve read. Previously, A History of the Groovy Programming Language.
This paper builds on an earlier result which showed that PushPush is NP-hard in 3D, but showing that is is equally hard in 2D.
PushPush
In this game, an agent needs to get from a starting position to a goal. The map is filled with blocks. The agent can push one block at a time, and each block will slide until it hits another block (or a boundary of the map).
With A as the agent, and o as a block, G as the goal.
A o ooo
oooo oooo
oooo oooo
oooo G ooooIn this case the Agent needs to push a block right to open up the path to the Goal.
Reduction from SAT
The high level proof is the standard reduction from SAT - construct a map that “represents” a formula, and prove in both direction:
- if the simulated boolean expression is satisfiable, there is a path the agent can take from the start to the goal
- if there is a path the agent can take from the start to the goal, the simulated boolean expression is satisfiable
Representing SAT formulas
A boolean formula written in conjunctive normal form , is made up of variables (x, y, z, etc.), conjunctions (x or y) which is called a clause, and a disjunction of these clauses, like (x1 ∨ x2) ∧ ( x1∨ x3). Such formulas can be represented in a map using a handful of gadgets.
Corridor
A 2x2 cluster of blocks is unmovable by an agent:
A
oo
ooThere is simply no space for any block to move anywhere.
We can use such clusters to construct “corridors” to guide the Agent:
A oooooo
oo oooooo
oo
ooooooooo
ooooooooo
oooo oooo
oooo oooo
oooo ooooThis forces the agent along a single path, to the right.
If we only use corridors of width 1, we can simplify the drawing by using lines for the corridors. The diagram above will be:
A-+
|
+-----
|
|
|We will also use o to represent a movable block:
A---o-
|
|
GAlternatively we may use a capital letter to label a movable block:
A---B-
|
|
GOne-Way Gadget
| x
|
+--o--
|
| yLemma 1: A one-way gadget permits movement from x to y, but not y to x. (After travelling from x to y, the agent can subsequently return from y to x.)
Fork Gadget
A Fork Gadget presents the Agent with a binary choice:
| x
|
+-+
| |
---o-+
| +------+
y | | zLemma 2: The Agent can pass from x to y or x to z, but taking one path seals off the other.
To go from x to y, the block has to be pushed down, and the path to z is blocked:
x
|
--|
| |
---|--
| o------|
y zTo go from x to z, the block as to be pushed left, and the path to y is blocked:
x
|
--|
| |
o--+--
| |------|
y zSimilar to the one-way gadget, the Agent may reverse its path.
3D Crossover Gadget
In 3D, crossovers are trivial, since you can build a corridor above an existing one.
|
---@---
|To represent a 3D crossing, we will use @: traversing vertically or horizontally is permitted, but those corridors are not connected at all.
Constructing the formulas
We can use the above gadgets to construct our formulas.
Variable-Setting component
The Agent will travel through a series of variable-setting components, each of which has a (T)rue path and a (F)alse path, indicating the value of that variable.
These components have corridors going to the right (called wires), and the two paths merges via One-Way gadgets.
The crossovers (@) indicate that the wires exiting F are not connected to the vertical T path at all.
a
|
+--+
F | |
o--+--+
| | T
| +------+
| +-------
+---------@-----
| +----
+---------@---
| |
+-o--+--o-+
|
bLemma 3: The Agent may travel from a to b only by choosing T or F, but not both. When a path is chosen, the Agent can travel down any wires attached to that path, but not any of the wires attached to the other path.
Clause Component
This represents a clause in the formula, a disjunction of the variables.
x
|
o---+
a | |
---o-+ |
b | |
---o-+ |
c | |
---o-+ |
| |
+-+---+
|
yLemma 4: The Agent may only pass from x to y if at least one block is pushed into it along an attached wire (a, b, or c above).
This is essentially a lock with three keys - the blocks on wires a, b, and c. At least one key must be inserted into the lock in order for the Agent to go from x to y.
Complete SAT reduction
s
|
+--+
F | | +--------+
+--o--+ o----+ |
| | T a | | |
| +------+ | | |
| x1 +-------------------------------o-+ | |
| +-------------------+ | c1 | |
+---------@-------------- | +------o-+ | |
| | | | | | | |
+---------@-------+ | | | | | |
| | | | | | +-----+ |
+-o-----o-+ | | | | | |
\ | | | | o---+ |
+--+ | | | | | | |
F | | | | +----@-----o-+c2 | |
+--o--+ | | |x1+~x2 | | |
| | T | | | +o-+ | |
| |------+ | | | | | | |
| x2 +-------@-----@----------+ | | | |
| | | | | ++---+ |
+---------@-------@-----@---------------+ o |
| +--+ | +--------------o--+---+ |
+-o--+--o-+ | | ~x1+x3 | | |
| +----@--------------------o--+ | |
\ | ~x1+x2+x3 | c3| |
+--+ | |--------o--+ | |
F | | | | | | |
+--o--+ | | ++---+ |
| | T | | | |
| +------+ | | o---+ |
| |------@------------ | | |
| | |--------------------o-+ | |
| | ~x1+~x3 |c4 | |
+---------@---------------------------o-+ | |
| | | | |
+-o--+--o-+ | | |
| | | |
| +-+---+ |
| t | |
+----------------------------------------------+The above figure shows a construction for a formula containing 4 clauses c1 ∨ c2 ∨ c3 ∨ c4. Two versions of the clauses are shown:
- (x1 ∨ x2) ∧ (x1∨ x2) ∧ ( x1 ∨ x3) ∧ ( x1∨ x3)
- (x1 ∨ x2) ∧ (x1∨ x2) ∧ ( x1 ∨ x2 ∨ x3) ∧ ( x1∨ x3)
The only difference betwen these two formulas are in C3. Formula 1 is not satisfiable, formula 2 is satisfiable.
The general idea is:
- Each variable has the True or False gadget
- Each clause in the formula has a clause gadget
- Clause components have a wire to either the True or False path of each variable it contains
Proof: If the simulated is SAT formula is satisfable, there is a path from s to t, as can be verified in the above figure. To proof the other direction, we use a proof by contradiction. Given the path from s to t, suppose the expression is unsatisfiable, then the robot can only reach t by “shortcutting” the design. The design of the variable components ensure only one of the True or False path can be taken. The crossovers ensure no “leakage”. The only possible way to get around this is if the robot could travel from a clause component back to a variable that sets the opposite value. But each variable clause has a block to prevent such actions.
2D Crossovers
This is the part of the table that adds on to the 3D proof. In 3D, crossovers were easy to construct. In 2D, it requires some clever mechanics.
There are two types of crossovers needed:
- FT-crossovers: horizontal wire from an False-wire in a variable unit crosses the vertial T wire of the same variable unit
- VC-crossovers: horizontal wire from some variable unit to a clause unit corsses a vertical wire from another variable unit to some claause unit.
FT-crossovers are traversed in one direction or the other, but never both, becuase once the Agent chooses True or False, it can never get to the other wire. So, FT-crossover is a more limited crossover.
This FT-crossover is also known as a XOR crossover:
XOR crossover
T |
+--+
F |
| +--o
| | |
+----+ +----+--+--+
| | | | | |
| +--o----+ +---o---| Cj
| | |
| xGoing from F to Cj is fine, as is going from T to x, but you cannot do both. After traversing, the same path can be traversed again multiple times in the same direction.
VC crossover
The VC crossovers need to be traversed in either direction (horizontal or vertical). It only needs to be traversed once in each of the four directions:
- from a variable component xi to deposit a key into the clause component
- returning back to xi
- later from xk where k != i to some Cl
- returning back to xk
This crossover is rather complex and can be built up using simpler components.
Locking Door Unit
This is a corridor with a locked door: once traversed, the passage is forever unpasssable:
+ x
|
+--+
|
+--+ +--+
| | | |
+--A--------------+--B
| | |
+--+ |
| |
| |
+--+ |
| | b |
+--C--------+--------+----+----D----
| | |
+-------------+ |
| yThe only possible way from x to y is to push A up, then B down, which serves as a stopper when pushing C right, and finally push D right.
Double Lock Unit
This behaves like a Locking Door Unit, but requires an external key to operate:
+
|
A
|
+------+--------+
|
+----------------+
| |
| +-+-+
| |LDU|
| +-+-+
| |
+----+--+-----+-----C----B
| | | |
| +--------+ |
| |
| |
+------o-------------+---+---+---o-+
| | |
+-------+ |
|
+A is the key and needs to be pushed down to stop C from going all the way left. B needs to be pushed down to stop D from going all the way right. Finally, due to the LDU, there is no way back to x.
Unidirectional Crossover Gadget
With the LDU and DLU, we can build a Unidirection Crossover Gadget:
y1
+-----+
| LDU |
+--+--+
|
o
+-----+ | +-----+
x1 | LDU +---o----------+ DLU | x2
+-----+ | +-----+
|
|
+--+--+
| DLU |
+-----+
y2This gadget can be traversed from x1 to x2, but not from x2 to x1, and from y1 to y2, but not y2 to y1.
Once a path is traversed, it becomes impassable from either direction, but the other path is still traversable.
Bidirectional Crossover Gadget
Finally, we can construct our VC-crossover:
y1
|
+---------------+
| |
| |
+--+--+ +--+--+
+---+ UCD +---------+ UCD +---+
| +--+--+ +--+--+ |
x1 | | | | x2
+-------+ | | +-----+
| | | |
| +--+--+ +--+--+ |
+---+ UCD +---------+ UCD +---+
+--+--+ +--+--+
| |
| |
+---------------+
|
y2This gadget can be traversed as many as four times in any order or x1-x2, x2-x1, y1-y2, y2-y1.
2D Construction
With all these gadgets in place, we can replace all FT-crossovers with a XOR Crossover Gadget, and all VC-crossover with a Bidirectional Crossover Gadget.