We introduce a graph coloring challenge benchmark based on the
problem of completing Latin squares. We show how the hardness
of the instances can be finely controlled by varying the
fraction of pre-colored squares. We compare three
complete (exact) solution strategies on this benchmark:
(1) a Constraint Satisfaction (CSP) based approach,
(2) a hybrid Linear Programming / CSP approach, and
(3) a Boolean Satisfibility (SAT) approach.
None of these methods uniformly dominates the others on
this domain. The CSP and hybrid approaches lead to more
compact encodings. The hybrid approach uses a randomized
rounding LP based approximation that considerably
boosts the performance of the CSP strategy on hard instances.
However, the SAT-based approach can solve some of the hardest
problem instances, provided the SAT encoding remains manageable.
We discuss the various tradeoffs between these approaches
in detail.
