To test the generalized case, we generated 10 randomly cube states. For each state, the time required by our SAT solver to search for a solution of length 20 or less is shown in Table 2.

The upper bound on the length of the phase 1 maneuvers has been shown to 12 [7]. Our experiments verified that this fact is true. Furthermore, within length 12 of the phase 1 maneuvers, we found always a solution of length 20 or less. As the length of the phase 1 maneuvers increases, the time **to solve a** cube increases sharply. In most of the cases, we can find a solution **within 7000** seconds. If the length of solutions is allowed to be 21, the time to solve a cube by our SAT solver never exceeds 1500 seconds.

| cube state   | length of phase 1   | length of phase 2   | time (seconds)   |
|--------------|---------------------|---------------------|------------------|
| 1            | 10                  | 10                  | 1072             |
| 2            | 11                  | 9                   | 6785             |
| 3            | 10                  | 10                  | 137              |
| 4            | 11                  | 9                   | 6123             |
| 5            | 9                   | 11                  | 87               |
| 6            | 10                  | 10                  | 774              |
| 7            | 11                  | 9                   | 1489             |
| 8            | 10                  | 9                   | 1079             |
| 9            | 12                  | 8                   | 14096            |
| 10           | 10                  | 10                  | 329              |

Table 2. **Runtime took by our SAT solver to solve 10 random cube states**

| cube state    | solution length   | time (seconds)   | solution length   | time (seconds)   |
|---------------|-------------------|------------------|-------------------|------------------|
| (non-optimal) | (non-optimal)     | (optimal)        | (optimal)         |                  |
| 1             | 19                | 0.3              | 19                | 9125             |
| 2             | 19                | 4.5              | 18                | 531              |
| 3             | 18                | 1.5              | 18                | 580              |
| 4             | 16                | 7.3              | 16                | 23               |
| 5             | 19                | 0.3              | 18                | 3243             |
| 6             | 18                | 1.5              | 17                | 315              |
| 7             | 17                | 2.1              | 17                | 25               |
| 8             | 19                | 0.1              | 18                | 4216             |
| 9             | 19                | 1.1              | 18                | 2219             |
| 10            | 19                | 0.1              | 18                | 1452             |

The test platform in Table 3 are the same as that in Table 2. Compared **with**
the SAT solver, Cube Explorer using lookup tables is much faster. As **shown in** Table 3, Cube Explorer took at most 8 seconds to find a non-optimal solution