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 s

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 https://www.gap-system.org/Doc/Examples/rubik.html