Samuel Pfrommer and I worked on this project as our final project for CIS 189 (Solving Hard Problems in Practice). The goal of the final project is to apply the tools and concepts covered in class to a problem of our choosing.

Preview

Motivation

We ended up choosing the problem of solving a Rubik's cube since it has been proven recently that it is NP-complete. The hardness of this problem suggests that an efficient SAT solver could potentially tackle this problem. It was also clear to us from the start that we'd have to explore a number of optimizations to enable a quick solve time, which made the project all the more exciting.

Plan

Our plan was to build a GUI where a user can submit the state of a rubik's cube and gets as output a sequence of moves that leads to the solved state. We also wanted the ability to visualize the solution the solver presented, which makes it easier to check that the solver has actually found a feasible solution.

Architecture

The user enters an intiial state into a webpage, which sends the information to a web server. The server then runs the solver in the back-end with the given initial state and sends the client a sequence of moves that will lead to the solve state. If the initial state is invalid, the server informs the client and an error is displayed. Ideally this would be done in the front-end, but we prioritized working on the solver and having the most important set of features implemented in the front-end given the time constraints.

The Solver

We used Google's OR-tools to solve a SAT encoding of the Rubik's cube. The essensce of the encoding is that a cube has an initial state and some sequence of moves that result in the solved state. Furthermore, it has been proven that an arbitrary 3x3x3 cube can be solved in 20 or less moves. This means that we can encode the initial state of a cube and 20 more states corresponding to the worst case where we need 20 moves. We can then apply constraints to ensure that the moves between states are valid, and that a solved state is found. The objective would then be to minimize the number of moves required.

A cube's state can be represented as a set of integer variables for each of the facelets in all the 6 faces (6 faces x 9 facelets = 54 variables for each state). The integer variable is constrained to [0-5], where each integer represents one of the 6 colors.

Given an initial state, we introduce constraints that force the variables of the intiial state to match the provided colors.

We then introduce a set of move constraints, which enforce that the change between two consecutive states is valid. There are 18 valid moves for a 3x3x3 cube; each of the 6 faces can be rotate 90° CW, 90° CCW, or 180°. Given two consecutive states s1 and s2, each facelet in s1 will be mapped to a facelet in s2 under a specific move. Knowing this mapping, we add constraints such that if a move is chosen the mapped facelets have the same color (integer) as the original facelet in the previous state.

We then introduce a final constraint, which enforces that of the 21 states, exactly one is solved (all facelets within a face have the same color). We then run the solver with the objective of minimizing the number of moves until the solved state.

We initially built the solver with a 3x3x3 cube in mind but quickly ran into long runtimes. We then pursued 2x2x2 cubes since they contain fewer states and can be optimized by reducing the number of variables. For example, opposite face moves in a 2x2x2 cube can be treated as equivalent, which halves the search space. In addition, instead of using integer variables, we can encode the colors using 3 boolean variables to represent the digits of a binary number. For example, 0 would be represented by 000 and 5 would be represented by 110.

Web Server

The server is built on Flask and serves React-based front-end. The front-end was developed using NodeJS and bundled into static files that were then served by the Flask server. The user can input an arbitrary initial state in the front-end or shuffle a cube randomly. The initial state is sent to the server, which runs the solver on the given input and send the client the solution (sequence of moves). The client then is able to visualize the moves on the initial state of the cube. The visualization was implemented using Three.js.