Queen Domination by SAT Solving

The queen domination problem asks for the minimum number of queens needed to attack all squares on an n n chessboard. Once this optimal number is known, determining the number of distinct solutions up to isomorphism has also attracted considerable attention. Previous work has introduced specialized and highly optimized search procedures to address open instances of the problem. While efficient in terms of runtime, these approaches have not provided proofs that can be independently verified by third-party checkers. In contrast, this paper aims to combine efficiency with verifiability. We reduce the problem to a propositional satisfiability problem (SAT) using a straightforward encoding, and solve the resulting formulas with modern SAT solvers capable of generating proof certificates. By improving the SAT encoding with a novel literal ordering strategy, and leveraging established techniques such as static symmetry breaking and the Cube-and-Conquer paradigm, this paper achieves both performance and trustworthiness. Our approach discovers and corrects a discrepancy in previous results for n=16 and resolves the previously open case n=19.