Measuring Sudoku Difficulty: Formulation, Propagation and Uniqueness Certification

Aled Williams

Home/Archive/arXiv

arXiv · 2610.37411

Measuring Sudoku Difficulty: Formulation, Propagation and Uniqueness Certification

Aled Williams

View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

math.OC

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Aled Williams. 2026-10-27. Measuring Sudoku Difficulty: Formulation, Propagation and Uniqueness Certification. https://arxiv.org/abs/2610.37411

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

NAG-GS: A Semi-Implicit Stochastic Optimizer with Large-Step Stability

Stochastic first-order methods are widely used for large-scale optimization and machine learning, where their performance often depends on the learning rate. We study NAG-GS, a stochastic momentum method based on a semi-implicit Gauss--Seidel discretization of a Nesterov-type flow. For strongly convex quadratics, we determine the exact range of stable step sizes for fixed damping and the step size that minimizes the worst-case spectral radius. When the damping equals the strong-convexity parameter, the method recovers the accelerated asymptotic factor $(\sqrtκ-1)/(\sqrtκ+1)$, where $κ$ is the condition number. We also prove that the quadratic iteration converges linearly with dynamic damping when its limiting fixed-damping iteration is stable. For general strongly convex, possibly nonsmooth objectives, we establish an $O(1/k)$ bound on the expected objective gap of the last iterate, using a conditionally unbiased stochastic first-order oracle with bounded second moment. The result holds with dynamic damping from any $γ_0>0$. We show that NAG-GS can also be written as a Heavy-Ball iteration with explicitly determined step sizes and momentum coefficients. We test the stochastic result on nonsmooth hinge-loss classification problems, and further evaluate NAG-GS on quadratic problems, logistic regression, convolutional neural networks, RoBERTa, and Vision Transformers. The experiments show that NAG-GS can remain effective at learning rates where standard optimizers become unstable or lose accuracy.

math.OC↗

arXiv2026

A Search-Based Algorithm for Multistage Robust Discrete Linear Optimization and its Implementation

Robust optimization models that allow decisions to adapt to newly revealed information remain computationally challenging and are often limited to two decision stages or are addressed heuristically or via approximation schemes. This challenge is further amplified when uncertainty sets depend on earlier decisions. Conventional approaches to such problems often require problem-specific reformulations and tailored algorithms, highlighting the need for an exact model-and-run approach. We address this gap by presenting an algorithmic framework for solving multistage robust discrete linear optimization problems. This exact approach adapts and integrates ideas from game-tree search, quantified conflict-driven clause learning, and integer linear programming to explore the minimax tree and is implemented in the open-source solver Yasol. The solver supports discrete decision variables across multiple stages, discrete uncertainty sets with polyhedral or decision-dependent structure, and mixed-integer recourse in the final stage. It can be used as a standalone executable or through a C++ library interface, allowing it to serve as a reference solver for exact methods in multistage robust discrete linear optimization. In an extensive computational study, we demonstrate the capabilities of our solver. The results show competitive performance against a reference approach from the literature for a protection-interdiction problem, as well as strong performance on bilevel benchmark instances. For a multistage cutting-stock problem, we demonstrate the substantial loss in solution quality that can arise from neglecting the multistage structure and show that our solver significantly outperforms decision-rule approximations in terms of computational efficiency while certifying the true multistage optimum.

math.OC↗

arXiv2026

Logic-Based Benders Decomposition for Time Slot Management with Mixed Logit Demand

This paper develops an exact solution framework for the choice-based time slot management problem under mixed logit demand in attended home delivery systems. The problem jointly optimizes delivery slot offerings, price discounts, and routing decisions, with customer choices endogenously modeled through a simulation-based mixed logit formulation embedded via sample average approximation, resulting in a large-scale stochastic mixed-integer program. To address this complexity, we propose a logic-based Benders decomposition (LBBD) that separates strategic assortment and pricing decisions, together with customer choice, from scenario-specific vehicle routing subproblems. We derive problem-specific optimality cuts that exploit the routing structure to provide stronger bounds than generic cuts, and establish their validity. To enhance computational performance, we introduce and systematically evaluate several strengthening strategies, including relaxation-based cut generation and capacity- and flow-based valid inequalities. We further compare two equivalent encodings of the embedded choice model and show that the relative value of each strengthening strategy depends on the strength of the master formulation it complements. Computational experiments on benchmark instances show that the proposed framework significantly extends the range of solvable instances compared to direct MILP approaches. The framework is exact: it converges to a proven optimal solution given sufficient time, and the bounds it produces at intermediate iterations are valid. Within a 12-hour limit, proven optimality is reached for instances with up to 10 customers, and valid bounds are obtained up to 40 customers, including sizes at which the direct MILP formulation returns no feasible solution.

math.OC↗