Let c(i, j, m) be the color of the j-th facelet in the i-the face under the m-th
(m ≥ 1) state (hereafter, color of facelet (i, j, m), for short), c(i, 4, **1) the center**
facelet color of the i-th face under the initial state. If the m**-th state is the solved**
state, this state may be represented by V
1≤i≤6,0≤j≤8 c(i, j, m) = c(i, 4, 1)
Using 3-variable scheme, c(i, j, m) = c(i, 4, 1) is translated into c(i, j, m, **1) =**
c(i, 4, 1, 1) ∧ c(i, j, m, 2) = c(i, 4, 1, 2) ∧ c(i, j, m, 3) = c(i, 4, 1, 3), where c(. . . 1),
c(. . . 2) and c(. . . **3) are literals that denote the 1st, 2nd and 3rd bit of a color.** Formula c(i, j, m, 1) = c(i, 4, 1, **1) can be translated into the following clauses:**
(c(i, j, m, 1) ∨ ¬c(i, 4, 1, 1)) ∧ (¬c(i, j, m, 1) ∨ c(i, 4, 1, **1)).**
An initial state of a cube is considered as State 1, which is interpreted as V
1≤i≤6,0≤j≤8,k=1,2,3 B(c(i, j, 1, k))
where B(c(i, j, 1, k)) is defined as c(i, j, 1, k) if the value of the k**-th bit color of**
facelet(i, j, 1) is 1, and ¬c(i, j, 1, k**) otherwise.**
Assume we take at most n − **1 moves to solve Rubik's Cube, and associate**
a Boolean variable st with each state t(1 ≤ t ≤ n). " st = true " mean the t-th state is the solved state. Then, this constraint can be represented by V
1≤i≤6,0≤j≤8
(¬st ∨ c(i, j, t) = c(i, 4, 1))
This formula can be converted easily into clauses.

At any time, among S = {s1, s2, . . . , sn}**, we must ensure that exactly one** st is true. The exactly-one constraint can be formalized by the at-least-one **(ALO)**
and at-most-one (AMO) constraint. That is, exactly-one(S) ≡ ALO (S)∧ AMO
(S). The standard SAT encodings of constraints ALO and AMO are the **following.**
ALO(S) ≡ s1 ∨ s2 **∨ · · · ∨** sn AMO(S) ≡ {si ∨ sj |si, sj ∈ **S, i < j**}
The ALO constraint ensures that a variable is true. And the AMO constraint ensures that no more than one variable is true. The standard AMO encoding requires much more clauses. To reduce the number of clauses, we can apply a two-product AMO encoding [14], which is recursively defined as AMO(S) ≡ AMO(U) ∧ **AMO(**V )
1≤k≤n,k V
=(i−1)q+j 1≤i≤p,1≤j≤q
((xk ∨ ui) ∧ (xk ∨ vj ))
where p = ⌈
√n⌉, q = ⌈
n p⌉, U = {u1, u2, . . . , up}, V = {v1, v2, . . . , vq}, each element uiin U and each element vj in V **are auxiliary variables. Here, AMO(**U)
and AMO(V **) apply the standard AMO encoding. The number of clauses and**
auxiliary variables required by this encoding are 2n + p(p − 1)/2 + q(q − 1)/2 and p + q, respectively. When n **= 20, the number of clauses required is 40 +**
4(4 − 1)/2 + 5(5 − 1)/2 = 56. For the n**, the standard AMO encoding requires**
20(20-1)/2=190 clauses.

To encode efficiently the constraints on the turns, we classify the turns of Rubik's Cube into six classes: u, d, l, r, f and b. Let uk(1 ≤ k ≤ n**) be a Boolean**
variable that is associated with the up turn of step k. We perform either U**-, or** U
′- or U2-type up turn at step k when uk is true, and do the other turn otherwise.