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.
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).
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?
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!
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.
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 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 -
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.
"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:"
[1] http://sabrlang.org/rubik/
[2] http://sabrlang.org/code/rubik/source.txt
[3] https://github.com/dbunker/SABR