Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles

TL;DR

This paper compares the performance of modern SMT solvers with traditional SAT solvers on large, complex Sudoku puzzles, demonstrating SMT solvers' superior efficiency in handling large-scale constraint satisfaction problems.

Contribution

It provides an empirical evaluation of SMT versus SAT solvers on large Sudoku puzzles, highlighting the advantages of advanced theory reasoning techniques.

Findings

SMT solvers outperform SAT solvers on large Sudoku puzzles

Advanced theory reasoning improves solver efficiency

Modern SMT solvers handle large-scale problems better

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.