solver based on PrecoSAT. The basic framework of this new solver is **similar to**
MoRsat [15], but replaces the lookahead solving strategy with an ALO (at-leastone) solving strategy. Let the notation F(x**) denotes the resulting formula after**
assigning literal x **true and performing iterative unit propagation. The basic**
idea of the ALO solving strategy is to decompose the original problem F **into**
subproblems F(xi)(1 ≤ i ≤ n) if a clause C in F is x1 ∨ x2 ∨ · · · ∨ xn**. If no subproblem is satisfiable, the original problem is unsatisfiable. Each subproblem can**
be solved in a recursive way. Once the recursive depth reaches some constant, say 4, we use PrecoSAT to solve that subproblem. This ALO solving strategy has been applied successfully to MPhaseSAT [17]. In the new solver used for Rubik's Cube, the size of the clause C **used to decompose the original problem** is specified to 6. And the recursive depth of the ALO solving strategy is limited to 4. Under this assumption, this new solver may be described in a recursive way as follows.

Algorithm SATsolver(F, level){Initially level **is set to 1**}
F ← **LookaheadSimplify(**F)
find a clause C **with 6 free variables**
if no such C was found then return **PrecoSAT(**F)
for i = 1 to 6 do assume C = x1 ∨ x2 ∨ x3 ∨ x4 ∨ x5 ∨ x6 F
′ ← F(xi)
if level ≤ 4 **then**
if **SATsolver(**F
′, level + 1) = SAT then return **satisfiable**
else if **PrecoSAT(**F
′) = SAT then return **satisfiable**
end for return **unsatisfiable**
Procedure LookaheadSimplify corresponds multiple failed literal probes in PrecoSAT. It can be either a simple look-ahead or double look-ahead **procedure**
in March [18]. In some cases, this procedure can be removed. The reason why the size of the clause C **in the above algorithm is limited to 6 is that there are** six types of moves, and in the SAT encoding of Rubik's Cube, the clause of size 6 is certainly obtained by encoding six types of moves. For general problems, the size of the clause C **in the above algorithm should be as long as possible.**

## 6 Experimental Studies

We solved Rubik's Cube with the SAT solver described in previous section on a 2.40GHz machine with Intel Core 2 Quad Q6600 CPU. Without adding the constraint conditions of two-phase algorithm given in Section 4, we found that determining whether a cube has an optimal solution with the maneuver (a move sequence is called a maneuver) length of 13 took about 7 hours in the **worst** case by our SAT solver. If the maneuver length of a solution is greater than 13, in general, no modern SAT Solver cannot find efficiently an optimal solution. However, if adding the constraint condition of two-phase algorithm, it is easy