Queen Domination by SAT Solving

TL;DR

This paper presents a SAT-based approach to the queen domination problem that combines efficiency with verifiability, solving open cases and correcting previous results using modern SAT solvers with proof generation.

Contribution

It introduces a novel SAT encoding with a new literal ordering, integrating symmetry breaking and Cube-and-Conquer techniques for reliable and efficient solutions.

Findings

Corrected previous results for n=16

Solved the open case n=19

Demonstrated verifiable solutions with proof certificates

Abstract

The queen domination problem asks for the minimum number of queens needed to attack all squares on an $n\times 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$.