使用 SAT 求解器求解魔方

魔方是一个易于理解的谜题，最初被称为“魔术方块”。这是一个著名的规划问题，已被研究了很长时间，然而许多简单性质仍然未知。本文研究了现代 SAT 求解器是否适用于该谜题。据我们所知，我们是首个将魔方转化为 SAT 问题的工作。为了减少编码所需的变量和子句数量，我们用 3 或 2 个布尔变量的新方法，取代了用 6 个布尔变量表示每个面块颜色的朴素方法。为了能够快速求解魔方，我们将 18 种转动的直接编码替换为基于 6 种类型转动的 18 子类型转动的层编码。为了进一步加速求解，我们将两阶段算法的一些性质编码为附加约束，并通过添加约束子句来限制某些移动序列。仅靠高效编码无法解决该谜题。因此，我们改进了现有的 SAT 求解器，并基于 PrecoSAT 开发了一个新的 SAT 求解器，尽管它仅适用于魔方。该新 SAT 求解器用 ALO（至少一个，\emph{at-least-one}）求解策略取代了前瞻求解策略，并将原问题分解为子问题。每个子问题由 PrecoSAT 求解。实验结果表明，我们的 SAT 转换和新求解技术都是高效的。如果没有高效的 SAT 编码和新求解技术，魔方仍然无法被任何 SAT 求解器求解。使用改进的 SAT 求解器，我们总能在合理时间内找到长度为 20 的解。尽管我们的求解器比使用查找表的 Kociemba 算法慢，但不需要巨大的查找表。