摘要翻译：
魔方是一种容易理解的拼图，最初被称为“魔方”。它是一个众所周知的规划问题，已经研究了很长时间。然而，许多简单的属性仍然未知。本文研究了现代SAT求解器是否适用于这一难题。据我们所知，我们是第一个把魔方翻译成SAT问题的人。为了减少编码所需的变量和子句的数量，我们用3或2个布尔变量的新方法取代了由6个布尔变量表示每个小面上的每个颜色的朴素方法。为了能够快速求解魔方，我们在6型圈的基础上用18亚型圈的层编码代替了18圈的直接编码。为了进一步加快求解速度，我们对两阶段算法的一些性质进行了编码，作为一个附加约束，并通过增加一些约束子对一些移动序列进行了约束。仅仅使用高效的编码并不能解决这个难题。为此，我们对现有的SAT求解器进行了改进，并基于PrecoSAT开发了一个新的SAT求解器，虽然它只适用于魔方。新的SAT求解器用ALO(\emph{至少一个}）求解策略代替了lookahead求解策略，并将原问题分解为子问题。每个子问题用Precosat求解。实验结果表明，我们的SAT翻译和新的求解技术都是有效的。如果没有高效的SAT编码和新的求解技术，任何SAT求解器都无法求解魔方。利用改进的SAT求解器，我们可以在合理的时间内找到长度为20的解。虽然我们的求解器比使用查找表的Kociemba算法慢，但不需要庞大的查找表。
---
英文标题：
《Solving Rubik's Cube Using SAT Solvers》
---
作者：
Jingchao Chen
---
最新提交年份：
2011
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  Rubik's Cube is an easily-understood puzzle, which is originally called the "magic cube". It is a well-known planning problem, which has been studied for a long time. Yet many simple properties remain unknown. This paper studies whether modern SAT solvers are applicable to this puzzle. To our best knowledge, we are the first to translate Rubik's Cube to a SAT problem. To reduce the number of variables and clauses needed for the encoding, we replace a naive approach of 6 Boolean variables to represent each color on each facelet with a new approach of 3 or 2 Boolean variables. In order to be able to solve quickly Rubik's Cube, we replace the direct encoding of 18 turns with the layer encoding of 18-subtype turns based on 6-type turns. To speed up the solving further, we encode some properties of two-phase algorithm as an additional constraint, and restrict some move sequences by adding some constraint clauses. Using only efficient encoding cannot solve this puzzle. For this reason, we improve the existing SAT solvers, and develop a new SAT solver based on PrecoSAT, though it is suited only for Rubik's Cube. The new SAT solver replaces the lookahead solving strategy with an ALO (\emph{at-least-one}) solving strategy, and decomposes the original problem into sub-problems. Each sub-problem is solved by PrecoSAT. The empirical results demonstrate both our SAT translation and new solving technique are efficient. Without the efficient SAT encoding and the new solving technique, Rubik's Cube will not be able to be solved still by any SAT solver. Using the improved SAT solver, we can find always a solution of length 20 in a reasonable time. Although our solver is slower than Kociemba's algorithm using lookup tables, but does not require a huge lookup table.
---
PDF链接：
https://arxiv.org/pdf/1105.1436