Source-linked AI summary
Coloring Queens with Thousands of Encodings
Bernardo Subercaseaux, Benjamin Przybocki, Marijn J. H. Heule
TL;DR
The paper asks how encoding choices affect SAT solver performance on queen-graph coloring, a setting Knuth used to benchmark 10 encodings. It compares 1,584 encodings and identifies symmetry breaking, clique hints, and exactly-one cell constraints as especially impactful.
Problem
The effects of SAT encoding choices on solver performance remain poorly understood, despite encoding choices having a dramatic impact.
Source: §1 · p. 1Method
The authors compare 1,584 queen-graph coloring encodings, including one-hot and order encodings, with variations in encoding choices.
Source: §1 · p. 2, §2.1.1 · p. 3, §2.1.2 · p. 4Results
Symmetry-breaking choices, clique hints, and exactly-one cell constraints are the three encoding factors identified as especially impactful.
Source: §1 · p. 2Takeaways & Limitations
For similar graph-coloring problems, the authors recommend enabling clique hints, enforcing exactly one color per cell, and testing several symmetry-breaking constraints.
Source: §1 · p. 2The SAT solver settings were fixed, and the authors lack a framework to predict or explain how encoding differences affect runtimes.
Source: §4 · p. 14
Abstract
from arXiv · showhide
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.
1 Introduction
Using queen-graph coloring to study SAT encodings, the paper compares 1,584 encodings—far more than Knuth’s 10—and finds three encoding choices especially consequential: symmetry breaking, clique hints, and exactly-one cell constraints.
1 Introduction
- The encodings vary how cells receive colors, how same-color conflicts are forbidden along rows, columns, and diagonals, and which symmetry-breaking assumptions are added.The paper groups these as within-cell, between-cell, and symmetry-breaking constraints.Source: §1 · p. 2
- Symmetry-breaking choices, clique hints, and exactly-one cell constraints are the three encoding factors the authors identify as especially impactful.Clique hints state that every color appears in each size-n clique; the graph-coloring constraints imply them, but SAT solvers struggle with the required pigeonhole reasoning.Source: §1 · p. 2
- The study compares 1,584 encodings, motivated by Knuth’s benchmark of 10 and the still poorly understood effects of encoding choices on solver performance.The queen’s graph is a concrete problem whose suitable instances take seconds or minutes to solve with a proper encoding.Source: §1 · pp. 1–2
- Unlike Knuth’s experiments, the results show one-hot encodings perform best, and clique hints can also be used with one-hot encoding.Knuth used clique hints only with order encoding and did not test alternative symmetry-breaking constraints; his row-1 symmetry breaking performs worse than most tested methods.Source: §1 · p. 2
- The chromatic-number problem is a natural graph-coloring variant of the classic 8-queens independent-set problem.The 8-queens question asks whether eight queens can be placed so that none attacks another; this is equivalent to an independent set of size 8 in the queen’s graph.Source: §1 · p. 2
- For n=8, 9, and 10, the queen graph’s chromatic number is n+1; establishing the n=10 result was hard for many earlier approaches.The authors report that their best encoding solves it in roughly four seconds.Source: §1 · p. 3
2 Encodings
The encodings vary how cells receive colors, how same-color conflicts are excluded, and how symmetries are broken. The section also describes clique hints that require every color to appear in each size-n clique.
2.1.1 One-Hot Encoding
- One-hot variables c(i,j),k represent cell-color assignments; within-cell options range from at-least-one to exact-one via pairwise or recursive encodings.Recursive variants can use wide or narrow clauses, linear or pooled splits, and sorted or randomized variable orderings.Source: §2.1.1 · p. 3
2.1.2 Order Encoding
- Order variables o(i,j),k encode a cell's color through an ordered sequence of colors, with variants that drop monotonicity clauses or randomize the order per cell.Dropping the clauses permits multiple colors to satisfy the encoding for a cell; random ordering uses an independent permutation for each cell.Source: §2.1.2 · p. 4
2.2.1 Independence Constraint
- The independence constraint prevents any color from appearing more than once among cells sharing a row, column, or diagonal, using pairwise or recursive at-most-one encodings.When recursive encodings are used for both within-cell and independence constraints, their cut, split style, and variable ordering are matched.Source: §2.2.1 · p. 4
2.2.2 Clique Hints
- Clique hints assert that every color appears in each size-n clique; the authors' hints outperform Tajima's weaker order-based version, while off-by-one diagonal hints were detrimental.A lemma generalizes the hint by lower-bounding how many vertices of a clique receive colors from a selected subset.Source: §2.2.2 · pp. 4–5
2.3 Symmetry Breaking
- Symmetry breaking targets color permutations and board rotations or reflections; for odd n, plus or cross configurations fix five central colors and add clauses to select one representative per symmetry class.The authors verified the correctness of the symmetry-breaking clauses using the SR proof format.Source: §2.3 · pp. 5–7
3 Results
Across the n = 9 and n = 10 analyses, symmetry breaking and exactly-one within-cell constraints emerge as major performance factors. Results also show that encoding performance can depend on the instance and on choices such as clique hints and clause ordering.
3 Results
- The main analysis focused on n = 9 and n = 10, with clique hints and symmetry breaking enabled; n = 8 was considered too easy for thorough encoding comparisons.This setup yielded 1584 encodings for n = 9 and 1188 for n = 10 because plus and cross symmetry breaking apply only to odd n.Source: §3 · p. 7
- At n = 9, symmetry breaking without clique hints solved the worst case in 0.21 core hours, versus 11.02 core hours with hints but no symmetry breaking.The authors report that symmetry breaking's impact trumps clique hints as n increases.Source: §3 · p. 7
3.1 Regression Models
- Symmetry breaking and exactly-one within-cell encodings are the most important modeled factors, and the best-setting one-hot encodings outperform order encodings.The implementation details of recursive encodings have little impact on average; diagonal symmetry breaking also performs differently relative to row 1 for n = 9 and n = 10.Source: §3.1 · p. 8
3.2 Symmetry Breaking
- For n = 9, plus symmetry breaking is best and cross is close; for n = 10, row 5 is better on average than row 1 because row 1 has a longer runtime tail.Across encoding settings, within-cell choices form clearer runtime clusters than between-cell choices; exactly-one encodings account for an order of magnitude in runtime differences at n = 10.Source: §3.2 · pp. 8, 11, Figure 3 · p. 8, Figure 4 · p. 11
3.3 Clique Hints
- For n = 9 with pairwise between-cell and exactly-one pairwise within-cell constraints, runtime decreases exponentially as the probability of including clique hints increases.The experiment varied the inclusion probability independently for each clique hint.Source: §3.3 · p. 12, Figure 5 · p. 12
3.4 On Brittleness
- Without clique hints, auxiliary placement has large instance-specific effects despite being statistically insignificant on average: linear versus pooled variants took 216 versus 366 seconds with row 1, and 34 versus 95 seconds with plus symmetry breaking.The Kissat flags --forcephase=1 --phase=0 also had a significant impact in these instances, unlike across the full dataset.Source: §3.4 · p. 12, Table 3 · p. 13
- For n = 10, vertically complementary row constraints yield isomorphic formulas, yet clause shuffling improves row 1 and worsens row 9; without scranfilizing, runtimes are even less symmetric.In these experiments, the bottom five rows were roughly equivalent without scranfilizing.Source: §3.4 · p. 13, Figure 6 · p. 13
4 Conclusion and Future Directions
The authors offer practical advice for encoding graph-coloring problems into SAT and argue that studying encodings at scale may improve understanding more generally. They identify fixed solver settings and the lack of a framework for explaining or predicting runtime differences as limitations and suggest experiments across domains.
4 Conclusion and Future Directions
- The empirical methodology of studying SAT encodings at scale may improve understanding of encodings more generally.The authors say similar experiments across different domains would be fruitful.Source: §4 · p. 13
- The analysis keeps SAT solver settings fixed, although those settings can matter for some problems and may interact with encoding choices.Source: §4 · p. 14
- The authors lack a framework for predicting or explaining how encoding differences affect runtimes, including why symmetry-breaking methods change relative order between n = 9 and n = 10.Source: §4 · p. 14