TE
TechEcho
Home24h TopNewestBestAskShowJobs
GitHubTwitter
Home

TechEcho

A tech news platform built with Next.js, providing global tech news and discussions.

GitHubTwitter

Home

HomeNewestBestAskShowJobs

Resources

HackerNews APIOriginal HackerNewsNext.js

© 2025 TechEcho. All rights reserved.

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

75 pointsby dennis714over 7 years ago

6 comments

trex44over 7 years ago
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&#x27;s the Rubik&#x27;s cube example [1]. Currently uses MiniSat on the backend. It&#x27;s pretty domain specific as languages go, but for certain problems it works well.<p>[1] <a href="http:&#x2F;&#x2F;sabrlang.org&#x2F;rubik&#x2F;" rel="nofollow">http:&#x2F;&#x2F;sabrlang.org&#x2F;rubik&#x2F;</a><p>[2] <a href="http:&#x2F;&#x2F;sabrlang.org&#x2F;code&#x2F;rubik&#x2F;source.txt" rel="nofollow">http:&#x2F;&#x2F;sabrlang.org&#x2F;code&#x2F;rubik&#x2F;source.txt</a><p>[3] <a href="https:&#x2F;&#x2F;github.com&#x2F;dbunker&#x2F;SABR" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;dbunker&#x2F;SABR</a>
评论 #15218012 未加载
_jnover 7 years ago
Though the &quot;define center colors&quot; approach sounds reasonable, a R&#x2F;L&#x27; turn (and T&#x2F;B&#x27; and F&#x2F;R&#x27;) are effectively equal, leaving you with {R; T; F; R&#x27;; T&#x27;; F&#x27;; 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.)
评论 #15214747 未加载
protomikronover 7 years ago
This is an interesting approach, but remark that the 2x2x2 cube can be simply brute-forced (which does not quite work well for 3x3x3) ...<p>E.g. using Java:<p><pre><code> import java.util.*; &#x2F;* usage: javac R222.java &amp;&amp; java R222 &gt;db.txt *&#x2F; public class R222 { private final static String SOLVED = &quot;RRRRYYYYBBBBOOOOWWWWGGGG&quot;; 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&lt;24; i++) new_cfg[i] = cfg.charAt(targets[i]); return new String(new_cfg); } private static void makeDB() { Map&lt;String, String&gt; tree = new HashMap&lt;String, String&gt;(); Map&lt;String, String&gt; tmp_tree = new HashMap&lt;String, String&gt;(); tree.put(SOLVED, &quot;&quot;); tmp_tree.put(SOLVED, &quot;&quot;); while (tmp_tree.size() &gt; 0) { Map&lt;String, String&gt; new_tree = new HashMap&lt;String, String&gt;(); for (Map.Entry&lt;String,String&gt; entry : tmp_tree.entrySet()) { String cfg = entry.getKey(); String ops = entry.getValue(); for (int op=0; op&lt;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&lt;String,String&gt; entry : tree.entrySet()) System.out.println(entry.getKey() + &quot;: &#x27;&quot; + entry.getValue() + &quot;&#x27;&quot;); } public static void main(String[] args) { makeDB(); } } </code></pre> We get 3674160 configurations and it takes just ~20 seconds (and most of the time is spent doing IO anyway).<p><pre><code> $ java R222 | wc -l 3674160 </code></pre> This might be useful to evaluate the number of moves (remark that we do &quot;half-turns&quot; here and in the case of 2x2x2 there are just 3 operations).<p>&#x2F;&#x2F;edit: TreeMap -&gt; HashMap
radokirovover 7 years ago
You might be interested to also look at how computational group theory software tackles the problem. AFAICT, it can&#x27;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.<p><a href="https:&#x2F;&#x2F;www.gap-system.org&#x2F;Doc&#x2F;Examples&#x2F;rubik.html" rel="nofollow">https:&#x2F;&#x2F;www.gap-system.org&#x2F;Doc&#x2F;Examples&#x2F;rubik.html</a>
OskarSover 7 years ago
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...).<p>Probably hard to make the heuristic admissable though, so the solution wont be optimal.
评论 #15217989 未加载
评论 #15217854 未加载
jacinaboxover 7 years ago
Uh oh, that Rubik&#x27;s cube at the bottom doesn&#x27;t look correctly solved; I think you might have an issue there.
评论 #15216180 未加载