here denotes a clockwise quarter turn of the "up" face, and similarly, **D, L, R, F**
and B **denote "down", "left", "right", "front" and "back", respectively. A solution can be represented by a move sequence. As an example, the move sequence**
F2U2B′U
′B2D′U2F
′U2LDR2B2U2F
′U2F
′U2B2L**2 is a solution to the state**
shown in Figure 1. That is, performing in turn each move in this sequence can restores that state to the home state. As defined in [3], we define S18 **the set**
of 18 moves mentioned above, and A10 = {U, U′, U2, D, D′, D2, L2, R2, F2, B2},
which will be used in subsequent sections and the two-phase algorithm given later.

A Rubik's Cube consists of different cubies. By convention, the cubies are classified into edge cubies (two visible facelets), corner cubies **(three visible**
facelets) and center cubies **(one visible facelets, in the center of a side). Correspondingly, according to the cubie where a facelet belongs, the facelets are**
classified into edge facelets, corner facelets and **center facelets**.

One of goals of this paper is to translate the Rubik's cube puzzle into a **satisfability (SAT) problem with CNF (conjunctive normal form). A propositional**
logic formula is said to be in CNF if it is a conjunction ("and") of clauses, **each**
clause being a disjunction ("ors") of Boolean literals, where each literal is either a variable or the negation of a variable.

## 3 Sat Encoding Of The Rubik'S Cube Puzzle

The Rubik's Cube puzzle may be described by the initial state, the move sequence, the map relation of each move and the solved state. Its SAT encoding will consist of such ingredients. A Rubik's Cube has a total of six colors. A naive approach is that a color corresponds a Boolean variable. Thus, representing each color on each facelet requires six Boolean variables. In fact, six colors contains only log 6 ≈ 2.**6 bit information. So the number of Boolean variables can be**
reduced. Let b1b2b3 be the binary representation of k(0 ≤ k ≤ **5). The Boolean**
variable representation of the k-th color is x1(b1), x2(b2), x3(b3), where xi(bi**) is**
xiif biis 1, and xi otherwise. For example, the Boolean variable representation of the second color is x1, x2, x3**. Therefore, 3 Boolean variables suffice for**
representing the color of each facelet. In our SAT encoding, states are divided into two categories: general state and H-state. A state is said to be H**-state** if it can be transformed into the solved state by a sequence of the moves in A10 mentioned above. In the two-phase algorithm, each state in Phase **two is**
H**-state. For general states, we represent each color on each facelet with three** Boolean variables. For H-states, we represent each color on each **facelet with two** Boolean variables. In the 2-variable scheme, we represent the colors of the front, left, back, right face in the solved state by 00, 01, 10 and 11, respectively, and then re-use 00 and 01 to represent the colors of the other two (top and down)
faces. Notice, any move in in A10 **cannot transform any facelet on top and down**
faces to somewhere on the other four faces. H**-states are allowed to use only**
moves in A10. Therefore, under H**-states, the 2-variable scheme does not yield**
any confusing.

4