发表机构
Carnegie Mellon University（卡内基梅隆大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文扩展了 Knuth 对皇后图着色问题的编码基准测试，通过比较1584种编码，识别出影响求解器性能的关键因素，并证明团提示同样适用于独热编码。
AI 中文摘要
在《计算机程序设计艺术》中，Knuth 对10种编码技术进行了基准测试，用于计算皇后图的色数：即为 $n \ imes n$ 棋盘上的方格着色所需的最少颜色数，使得没有两个共享行、列或对角线的方格获得相同颜色。在本文中，我们将他的分析大幅扩展，针对同一问题比较了数千种编码，这使我们能够识别出对求解器性能至关重要的其他因素。我们通过变化 (a) 编码每个单元格分配哪种颜色的约束，(b) 禁止同一颜色出现在行、列或对角线上的约束，以及 (c) 对称性破缺约束，获得了该问题的1584种编码。我们发现，影响最大的三个编码因素是 (i) 对称性破缺约束的选择，(ii) 启用所谓的团提示，以及 (iii) 通过阻塞子句强制每个单元格恰好分配一种颜色。此外，虽然 Knuth 提出团提示是顺序编码的一个优势，但我们实际上表明，它们也可以有效地用于独热编码。
英文摘要
In The Art of Computer Programming, Knuth benchmarked 10 encoding techniques for computing the chromatic number of the queen's graph: the minimum number of colors needed to color the squares of an $n \times n$ chessboard so that no two squares sharing a row, column, or diagonal receive the same color. In this paper, we extend his analysis much further by comparing thousands of encodings for the same problem, which allows us to identify additional factors that are important for solver performance. We obtain 1584 encodings for this problem by varying (a) the constraints that encode which color is assigned to each cell, (b) the constraints that forbid the same color appearing in a row, column, or diagonal line, and (c) the symmetry-breaking constraints. We find that the three most impactful encoding factors are (i) the choice of symmetry-breaking constraints, (ii) enabling so-called clique hints, and (iii) enforcing that each cell is assigned exactly one color through blocked clauses. Furthermore, while Knuth proposed clique hints as an advantage of the order encoding, we show in fact that they can be effectively employed for the one-hot encoding as well.
CommentsTo appear in LPAR 2026
