whose length is at most 20. In most of the cases, it found a solution immediately.

However, to find an optimal solution, it is also time-consuming in some cases. For example, finding an optimal solution of cube state 1 took 9125 seconds. If information on lookup tables can be encoded in CNF, it is possible that the SAT solver can outperform Cube Explorer.

Our encoding follows almost the idea of brute force enumeration. However, it is impossible for brute force enumeration to find a solution of length **20 with** length 12 of the phase 1 maneuvers on a modern PC in a reasonable time, since brute force enumeration has to check about 1512 ×9 10 ≈ 1023.7**states (note each**
state consists of 48 movable facclets) in the worst case. Hence, the SAT solver has its advantage over generalized approaches such as brute force enumeration.

The main advantage of solving a cube with SAT solvers is that it does not need a huge lookup table indicating the distance from the home state, and the memory requirement is very less. 10 MB RAM memory is enough.

## 7 Conclusions

This paper is the first to solve Rubik's Cube using a SAT solver. The experimental results reveal that our SAT encoding of Rubik's Cube and the improvement on the existing SAT solver are effective. Using the improved SAT solver, Rubik's Cube can be solved in a reasonable time. We believe that the encoding approaches and the ALO solving technique should be useful beyond the planning domain such as Rubik's Cube.

Here many open problem remains. For example, what is the optimal SAT
encoding of Rubik's Cube? The heuristic approach is frequently used **to speed** up SAT solvers. Can the heuristics information be encoded into a SAT **formula?** Indeed, in this paper, we implemented the SAT encoding of partial heuristic information such as the goal state information of phase 1 in two-phase algorithm. However, we cannot still encode the information on lookup tables (pattern database of Rubik's Cube) in Kociemba's algorithm, which is used to prune the superfluous search space. When a SAT formula is given, can we exploit logic structures on the heuristic information? What two-phase algorithm uses is a depth-first search technique. How to encode the depth-first search technique in CNF is also a challenge. Although one now has proved that God's number or the upper bound on the number of moves for Rubik's Cube is exactly 20, We cannot encode yet such a problem into a SAT problem. Nevertheless, in near **future,** we believe that it is possible to perform the SAT encoding of the upper **bound** of Rubik's Cube by extending the current SAT encoding technique of **Rubik's** Cube.

## References

12