Measuring Sudoku Difficulty: Formulation, Propagation and Uniqueness Certification
Abstract
Finding a Sudoku completion and proving that the completion is unique are different computational tasks. Despite both concerning the same puzzle, their computational effort need not be closely related. In this paper, we investigate how this relationship depends on the mathematical formulation, solver and measure of computational effort. Using 32,000 uniquely solvable puzzles and 64 harder instances, we compare integer programming formulations and CP-SAT. Further, we prove that the raw natural formulation has an extremely weak linear programming relaxation, even with uniqueness exclusions. Computational experiments show that the relationship between completion and certification effort depends on the formulation, puzzle population, solver and effort measure, rather than on the puzzle alone.
Related
- Comparative Analysis of Machine Learning Algorithms for Predicting Difficulty Disengaging from Social Media Among Students
- The Certification Exponent: Instance-Optimal Sequential Certification of Policy Improvement from History Dependent Logs
- SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
- \textit{In situ} certification of multiparticle indistinguishability in a generic interferometer
- Exact certification for conic optimization over quadratic modules: partitions of unity and recession directions
BibTeX
@misc{williams2026measuring,
title = {{Measuring Sudoku Difficulty: Formulation, Propagation and Uniqueness Certification}},
author = {Aled Williams},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.37411},
eprint = {2610.37411},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.37411},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Measuring Sudoku Difficulty: Formulation, Propagation and Uniqueness Certification
AU - Aled Williams
PY - 2026
DA - 2026/10/27
PB - arXiv
DO - 10.48550/arxiv.2610.37411
UR - https://arxiv.org/abs/2610.37411
AB - Finding a Sudoku completion and proving that the completion is unique are different computational tasks. Despite both concerning the same puzzle, their computational effort need not be closely related. In this paper, we investigate how this relationship depends on the mathematical formulation, solver and measure of computational effort. Using 32,000 uniquely solvable puzzles and 64 harder instances, we compare integer programming formulations and CP-SAT. Further, we prove that the raw natural formulation has an extremely weak linear programming relaxation, even with uniqueness exclusions. Computational experiments show that the relationship between completion and certification effort depends on the formulation, puzzle population, solver and effort measure, rather than on the puzzle alone.
ER -