Queen Domination by SAT Solving
Taha Rostami, Curtis Bright

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 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSocioeconomic Development in MENA
