It is impossible to encode directly the entire Kociemba's algorithm into a SAT
problem, because it contains lookup tables. However, it is possible to **encode the** basic idea of Kociemba's algorithm with a CNF formula. Let Cube **CNF(**n)
denote a SAT encoding of Rubik's Cube with a total of n **states, which can** easily be done by the approach given in Section 3. Assume that the k**-th state**
sk reaches a state in H**. A SAT encoding of Rubik's Cube containing the basic**
idea of Kociemba's algorithm can be described by the following formula:
Cube CNF(n) ∧ Hstate(sk) ∧ A10 move(**k, n**)
where Hstate(sk) is true if sk is in H, and A10 move(k, n**) is used to restrict** moves from step k to step n to be moves in A10. Hstate(sk**) is defined as**
V
1≤i≤4,j=3,5
(c(i, j, k) = c(i, j, 4) ∨ c(p(i), j, k) = c(i, j, 4))∧
V
i=5,6∧0≤j≤8
(c(i, j, k) = c(i, j, 4) ∨ c(p(i), j, k) = c(i, j, 4))
where p(i) denotes the opposite face of the i-th face, i.e., the mapping relationship of p is: 1 ↔ 3, 2 ↔ **4, 5** ↔ 6.

Based on the definition of A10, L, L′, R, R′, F, F′, B and B′ **all are not in** A10.

So A10 move(k, n**) may be described by the following logic formula.**
V
k<m≤n
¬(Lm ∨ L
′
m ∨ Rm ∨ R′m ∨ Fm ∨ F
′
m ∨ Bm ∨ B′m)
This means that after step k**, neither clockwise nor counter clockwise 90**
degree turn of any face except for the up and down face is allowed.

The encoding of Rubik's Cube containing the above two constraints can be considered as a SAT encoding of Kociemba's algorithm. Depending on different k, the efficiency of solution is different. In general, k **is set to less than 12. That** is, the length of Phase one is limited to 12.

A move on a cube can change only 20 facelets, and keep the other 28 **facelets**
unchanged. That is to say, the last second state from the solved state have 28 facelets that are placed correctly. Based on this property, we **encode the last** second state as a additional constraint condition. Let t **is the last turn operation.** Then we add the following encodings:
(¬ut∨ unchanged28facelet(U)) ∧(¬dt∨ **unchanged28facelet(**D)) ∧ (¬lt∨ unchanged28facelet(L)) ∧(¬rt∨ **unchanged28facelet(**R)) ∧
(¬ft∨ unchanged28facelet(F)) ∧(¬bt∨ unchanged28facelet(B)).

where unchanged28facelet(U**) can be encoded as follows.**
V
1≤i≤4,3≤j≤8 c(i, j, t − **1) =** c(i, 4, 1) V
0≤j≤8 c(6, j, t − **1) =** c(6, 4, 1)
the other unchanged28facelets are similar. The last second state **from the final**
state of phase 1 can be encoded also in a similar way.

## 5 A Sat Solver For Solving Rubik'S Cube

Based on our experimental observation, the PrecoSAT solver [13], **the Gold** Medal winners in the application category of the SAT 2009 competition, was the fastest on Rubik's Cube. Without any pruning strategy, it is hard to solve Rubik's Cube. Since PrecoSAT has no pruning strategy, it is not good **choice to** use directly PrecoSAT. To solve more efficiently Rubik's Cube, we built a new