Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles

TL;DR

This study benchmarks modern SMT solvers against a classical SAT/DPLL approach on large-scale $25\times25$ Sudoku puzzles generated by a dedicated tool. By implementing a baseline DPLL solver, a DPLL(T) hybrid, and SMT solvers Z3 and CVC5 within a unified Python benchmarking framework, the work assesses how theory reasoning, CNF encodings, and Sudoku-specific constraints influence performance. Results show that Z3 and CVC5 solve all puzzles with substantially lower solve times and propagation counts, while DPLL-based methods falter on a subset of instances, highlighting the scalability and effectiveness of SMT Techniques for large constraint satisfaction problems. The findings underscore the value of advanced theory integration and encoding strategies, and point to promising directions in solver fine-tuning, hybrid architectures, and machine-assisted theorem proving for broader applicability.

Abstract

Modern SMT solvers have revolutionized the approach to constraint satisfaction problems by integrating advanced theory reasoning and encoding techniques. In this work, we evaluate the performance of modern SMT solvers in Z3, CVC5 and DPLL(T) against a standard SAT solver in DPLL. By benchmarking these solvers on novel, diverse 25x25 Sudoku puzzles of various difficulty levels created by our improved Sudoku generator, we examine the impact of advanced theory reasoning and encoding techniques. Our findings demonstrate that modern SMT solvers significantly outperform classical SAT solvers. This work highlights the evolution of logical solvers and exemplifies the utility of SMT solvers in addressing large-scale constraint satisfaction problems.

Figures (3)

• Figure 1: Average Solving Time for Each Solver
• Figure 2: Scatter Plots of Solve Times Across Solvers
• Figure 3: Average Propagations