Solving pocket Rubik’s cube (2*2*2) using Z3 and SAT solver | Hacker News Reader

Solving pocket Rubik’s cube (222) using Z3 and SAT solver

yurichev.com

75 pointsdennis71417 comments

This is pretty cool. I tried a while back to make it a bit easier to solve these types of problems where you have a start state, end state, and possible transitions and restrictions, and want to determine the transitions needed to get from start to end using a CNF solver. Here's the Rubik's cube example [1]. Currently uses MiniSat on the backend. It's pretty domain specific as languages go, but for certain problems it works well.

[1] http://sabrlang.org/rubik/

[2] http://sabrlang.org/code/rubik/source.txt

[3] https://github.com/dbunker/SABR

I was just looking for a DSL for instruction set selection and load/store optimization.

Though the "define center colors" approach sounds reasonable, a R/L' turn (and T/B' and F/R') are effectively equal, leaving you with {R; T; F; R'; T'; F'; 2R; 2T; 2F} = 9 possibilities by having the bottom-rear-left cubelet at a constant position. (31 billion nodes when the graph is not trimmed whatsoever by removing redundant moves.)

In the same vein, it seems like evaluating the positions of the "cubelets" instead of "facelets" would reduce computation time a fair amount (8 values to keep track of instead of 24).

Shouldn't that be 8*2 values since the rotation of the cubelets is also important? (I haven't done much research on graph-trimming rubik's cubes, so I'm not quite sure about this.)

It turns out that the orientation of the cutlets is enough to define the entire state. This is also true of the 3x3x3 cube. Each one can have one of 24 orientations, and the position can be determined by the orientation. To prove to yourself that this is true, consider a completed cube centered at the origin and define each pieces geometry in world coordinates. All cube manipulations consist of rotations around one of the 3 axis, there are no translations. There are 24 orientations possible.

Given that, the 2x2x2 cube can be encoded as 8 orientations with 24 value for each. This results in a maximum of 24^8 cube positions or about 100 billion, many of which are not actually valid. So one could start with the solved cube and do a breadth first exploration of the entire space. You'd scan an array of 100B positions for any one that has a known solution (the complete cube is initially the only one). For each position with a known solution, make all possible moves from there and record the move required to solve the cube at any new positions reached. Repeat until no new positions can be reached.

Someone said the 2x2x2 cube can always be solved in 11 moves or less, so 11 scans across a 100B possible positions will be sufficient to create a database of optimal moves to solve from any position. This should be reasonable to do.

As I think about this, on the small cube turning one face has the same effect as turning the opposite one the other direction. So we could start by picking one corner and turn the entire cube so that corner is in final position. From that point, only 4 faces could be turned either CW or CCW, so encoding a move would require 3 or 4 bits, and there would be 1/24 as many positions because the one cubelet is not movable. This would be about 4-5 billions positions which would fit in RAM on a lot of modern laptops or a DVD.

I had expected something like this knowing that it's impossible to solve a 3x3x3 after assembling it with a corner rotated incorrectly. Thanks for this insight!

I wonder if these types of optimization/simplification could happen at a lower level, e.g. by preprocessing the SABR file and exploiting symmetries found there.

And yes, I'm aware that this might be as hard as an optimizing compiler, or even an instance of the SufficientlySmartCompiler [1]. But maybe this instance is simpler, maybe it belongs more to the lines of combining code duplicates, or simplifying algebraic expressions?

[1] http://wiki.c2.com/?SufficientlySmartCompiler

This is an interesting approach, but remark that the 2x2x2 cube can be simply brute-forced (which does not quite work well for 3x3x3) ...

E.g. using Java:

  import java.util.*;

  /* usage: javac R222.java && java R222 >db.txt */
  public class R222 {
    private final static String SOLVED = "RRRRYYYYBBBBOOOOWWWWGGGG";

    private final static int op0[] = {1,3,0,2,21,20,6,7,4,5,10,11,12,13,14,15,9,8,18,19,16,17,22,23};
    private final static int op1[] = {0,1,8,10,5,7,4,6,15,9,14,11,12,13,20,22,16,17,18,19,3,21,2,23};
    private final static int op2[] = {0,19,2,17,4,1,6,3,9,11,8,10,12,7,14,5,16,13,18,15,20,21,22,23};

    private static String update(String cfg, int op) {
        char new_cfg[] = new char[24];
        int targets[] = op == 0 ? op0 : (op == 1 ? op1 : op2);

        for (int i=0; i<24; i++)
            new_cfg[i] = cfg.charAt(targets[i]);
         
        return new String(new_cfg);
    }

    private static void makeDB() {
        Map<String, String> tree = new HashMap<String, String>();
        Map<String, String> tmp_tree = new HashMap<String, String>();

        tree.put(SOLVED, "");
        tmp_tree.put(SOLVED, "");

        while (tmp_tree.size() > 0) {
            Map<String, String> new_tree = new HashMap<String, String>();

            for (Map.Entry<String,String> entry : tmp_tree.entrySet()) {
                String cfg = entry.getKey();
                String ops = entry.getValue();

                for (int op=0; op<3; op++) {
                    String new_cfg = update(cfg, op);
                    if (!tree.containsKey(new_cfg)) { 
                        tree.put(new_cfg, ops + op);
                        new_tree.put(new_cfg, ops + op);
                    } 
                }
            }

            tmp_tree = new_tree;
        }

        for (Map.Entry<String,String> entry : tree.entrySet())
            System.out.println(entry.getKey() + ": '" + entry.getValue() + "'");
    }

    public static void main(String[] args) {
        makeDB();
    }
  }

We get 3674160 configurations and it takes just ~20 seconds (and most of the time is spent doing IO anyway).

  $ java R222 | wc -l
  3674160

This might be useful to evaluate the number of moves (remark that we do "half-turns" here and in the case of 2x2x2 there are just 3 operations).

//edit: TreeMap -> HashMap

You might be interested to also look at how computational group theory software tackles the problem. AFAICT, it can't search for minimal solution, but it find solutions quite quickly. I think group theory captures more (all?) of the structure of the problem than SAT.

https://www.gap-system.org/Doc/Examples/rubik.html

I wonder how good A-star would be at solving something like this? The hard part would be figuring out a good heuristic, but I bet with some experimentation you could come up with something (number of correct facelets, or cubelets, or number of moves to correctly place all cubelets if they moved independently...).

Probably hard to make the heuristic admissable though, so the solution wont be optimal.

For the pocket cube, you can just enumerate all positions. It's a very small space.

For larger Rubik's cubes, a naive A* won't cut it, as it still has exponential growth. Iterative deepening A* built atop a pattern database has worked well though. This paper from 1997 also discusses heuristics -

https://www.cs.princeton.edu/courses/archive/fall06/cos402/p...

And since I'm pulling from Udacity's AI course anyway, might as well provide this; the 3x3 has been fully solved. Depending on the metric -

http://www.cube20.org/ or http://www.cube20.org/qtm

The point with having a good heuristic is to avoid having to walk the vast majority of the search space, so I wouldn't have thought the exponential growth was that big of a problem. But I guess it's harder than I thought.

Uh oh, that Rubik's cube at the bottom doesn't look correctly solved; I think you might have an issue there.

I can not see a better way than this comment to prove that one did not read the article.

"However, you can use 3.3.3 cube to play, because it can act as 2.2.2 cube: just use corners and ignore edge and center cubes. Here is mine I used, you can see that corners are correctly solved:"

Reply on news.ycombinator.com