Solving Rubik's Cube Using SAT Solvers

Details Solving Rubik's Cube Using SAT Solvers Solving Rubik's Cube Using SAT Solvers

2011-05-07

arxiv.org/abs/1105.1436v1

SPA 2011: SAT for Practical Applications

Computer Science

Artificial Intelligence

13 pages

Scientific paper

Rubik's Cube is an easily-understood puzzle, which is originally called the "magic cube". It is a well-known planning problem, which has been studied for a long time. Yet many simple properties remain unknown. This paper studies whether modern SAT solvers are applicable to this puzzle. To our best knowledge, we are the first to translate Rubik's Cube to a SAT problem. To reduce the number of variables and clauses needed for the encoding, we replace a naive approach of 6 Boolean variables to represent each color on each facelet with a new approach of 3 or 2 Boolean variables. In order to be able to solve quickly Rubik's Cube, we replace the direct encoding of 18 turns with the layer encoding of 18-subtype turns based on 6-type turns. To speed up the solving further, we encode some properties of two-phase algorithm as an additional constraint, and restrict some move sequences by adding some constraint clauses. Using only efficient encoding cannot solve this puzzle. For this reason, we improve the existing SAT solvers, and develop a new SAT solver based on PrecoSAT, though it is suited only for Rubik's Cube. The new SAT solver replaces the lookahead solving strategy with an ALO (\emph{at-least-one}) solving strategy, and decomposes the original problem into sub-problems. Each sub-problem is solved by PrecoSAT. The empirical results demonstrate both our SAT translation and new solving technique are efficient. Without the efficient SAT encoding and the new solving technique, Rubik's Cube will not be able to be solved still by any SAT solver. Using the improved SAT solver, we can find always a solution of length 20 in a reasonable time. Although our solver is slower than Kociemba's algorithm using lookup tables, but does not require a huge lookup table.

Affiliated with

Also associated with

No associations

Rating

Solving Rubik's Cube Using SAT Solvers does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Solving Rubik's Cube Using SAT Solvers, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Solving Rubik's Cube Using SAT Solvers will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-653794