1974[1] by Ern¨o Rubik. So far, It has been studied for a long time. Yet many simple properties remain unknown. From the viewpoint of SAT applications, this paper studies this puzzle.

With respect to this puzzle, one of the most natural questions is how many moves are required to solve Rubik's Cube in the worst case. This problem has been studied for over 30 years. There has been great progress. **In 1995, Reid** proved that the lower bound on the number of moves and the upper **bound is**
20 and 29, respectively [5,6,7]. Since then, the upper bound was unceasingly improved. In 2006, the upper bound was reduced by Radu [8] to 27. In 2007, Kunkle and Cooperman used computer search methods to refine it to 26. In 2008, Rokicki [3,4] reduced further it from 25 to 22. In 2010, this open problem was settled. Rokicki, Kociemba, Davidson and Dethridge [9,10] proved that God's **number**
(i.e. the upper bound) for the Cube is exactly 20. They spent about **35 CPUyears of idle computer donated by Google to solve all 43,252,003,274,489,856,000**
positions of the Cube. Without a doubt, all the current approaches to proving the upper bound are time-consuming and space-consuming. How to **finish the** theoretical proof of the upper bound is yet a hard problem.

Apart from the approach to compute directly positions of the Cube, one considered the other approaches. In 1985, Korf [11] noted that problems such as Rubik's Cube can be divided into subgoals that are of the property **called**
operator decomposability, and attempted to solve them by searching for macrooperators. Korf's approach succeeded for the 2 × 2 × **2 version of Rubik's Cube,**
but failed to find an optimal solution for the full 3×3×**3 Rubik's Cube, for which**
the solution lengths are close to those of human strategies. Rubik's **Cube is also a** well-known planning problem. This puzzle can be encoded as a planning problem in PDDL (Planning Domain Definition Language). Nevertheless, there **is no** report on solving successfully it using a sat-based planner such as SATPLAN [12].

The purpose of this paper is two-fold. The first purpose is to design an effective SAT encoding of Rubik's Cube. The second purpose is to improve the existing SAT solvers to extend the range of SAT applications. To attain the first purpose, we optimize the encoding of this puzzle in the following ways: **encoding** the At-Most-One (AMO) constraint for minimizing the number of moves by the 2-product encoding [14] proposed recently, and replacing a naive approach of 6 Boolean variables to represent each color on each facelet with a new **approach of** 2 Boolean variables. The number of Boolean variables required by a cube state is cut from 8×6×6 = 288 to 8×6×3 = 144 or 8×6×**2 = 96. Encoding this puzzle**
according to the idea of one-phase algorithm results in a very hard SAT problem. Therefore, we encode this problem according to the idea of two-phase algorithm, and consider the goal state of phase 1 as an additional constraint. In addition to efficiently encoding this puzzle, we improve the existing SAT solvers, and develop a new hybrid SAT solver based on PrecoSAT [13], though the new solver is suited only for Rubik's Cube. The new solver selects some decision variables according to whether a variable occurs in a clause with the AMO constraint, and **splits** the original problem into some subproblems with those decision variables. Each 2