Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles
This work addresses constraint satisfaction problems for researchers and practitioners, but it appears incremental as it benchmarks existing solvers on new data.
The paper tackled the performance of modern SMT solvers compared to classical SAT solvers on large-scale Sudoku puzzles, finding that SMT solvers significantly outperform SAT solvers, though no concrete numbers are provided.
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.