Home

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 oooo``````

In 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
oo``````

There 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 oooo``````

This 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-
|
|
G``````

Alternatively we may use a capital letter to label a movable block:

``````A---B-
|
|
G``````

``````| x
|
+--o--
|
| y``````

Lemma 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.)

A Fork Gadget presents the Agent with a binary choice:

``````       | x
|
+-+
| |
---o-+
|  +------+
y |         | z``````

Lemma 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         z``````

To go from x to z, the block as to be pushed left, and the path to y is blocked:

``````      x
|
--|
| |
o--+--
|  |------|
y         z``````

Similar to the one-way gadget, the Agent may reverse its path.

In 3D, crossovers are trivial, since you can build a corridor above an existing one.

``````   |
[email protected]
|``````

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
|  +------+
|         +-------
[email protected]
|         +----
[email protected]
|         |
+-o--+--o-+
|
b``````

Lemma 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-+   |
|   |
+-+---+
|
y``````

Lemma 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 |   |
[email protected]     |    +------o-+    |   |
|         |             |     |    |        |    |   |
[email protected]+     |     |    |        |    |   |
|         |       |     |     |    |       +-----+   |
+-o-----o-+       |     |     |    |       |         |
\            |     |     |    |       o---+     |
+--+           |     |     |    |       |   |     |
F    |  |           |     |     [email protected]+c2 |     |
+--o--+           |     |          |x1+~x2 |   |     |
|  |        T     |     |          |    +o-+   |     |
|  |------+       |     |          |    |  |   |     |
|   x2    [email protected]@----------+    |  |   |     |
|         |       |     |               | ++---+     |
[email protected]@[email protected]+ o          |
|         +--+    |     +--------------o--+---+      |
+-o--+--o-+  |    |            ~x1+x3     |   |      |
|       [email protected]+   |      |
\           |           ~x1+x2+x3   | c3|      |
+--+          |           |--------o--+   |      |
F    |  |          |           |           |   |      |
+--o--+          |           |          ++---+      |
|  |        T    |           |          |           |
|  +------+      |           |          o---+       |
|         |[email protected]          |   |       |
|         |      |--------------------o-+   |       |
|         |                  ~x1+~x3    |c4 |       |
[email protected]+   |       |
|         |                             |   |       |
+-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:

1. (x1 ∨ x2) ∧ (x1∨ x2) ∧ ( x1 ∨ x3) ∧ ( x1∨ x3)
2. (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:

1. FT-crossovers: horizontal wire from an False-wire in a variable unit crosses the vertial T wire of the same variable unit
2. 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
|            |             |
| x``````

Going 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:

1. from a variable component xi to deposit a key into the clause component
2. returning back to xi
3. later from xk where k != i to some Cl
4. 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----
|             |    |
+-------------+    |
| y``````

The 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.

With the LDU and DLU, we can build a Unidirection Crossover Gadget:

``````                y1
+-----+
| LDU |
+--+--+
|
o
+-----+       |      +-----+
x1 | LDU +---o----------+ DLU |  x2
+-----+       |      +-----+
|
|
+--+--+
| DLU |
+-----+
y2``````

This 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.

Finally, we can construct our VC-crossover:

``````                       y1
|
+---------------+
|               |
|               |
+--+--+         +--+--+
+---+ UCD +---------+ UCD +---+
|   +--+--+         +--+--+   |
x1      |      |               |      |    x2
+-------+      |               |      +-----+
|      |               |      |
|   +--+--+         +--+--+   |
+---+ UCD +---------+ UCD +---+
+--+--+         +--+--+
|               |
|               |
+---------------+
|
y2``````

This 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.