对比大尺度数独题，SMT求解器比传统SAT更高效。
Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles
- 用改进生成器构造25×25数独，测试不同求解器表现。
- SMT求解器在各类难度下均显著快于经典SAT求解器。
- 适合对逻辑求解器性能评估或约束求解感兴趣的读者。
现代SMT求解器通过融合高级理论推理与编码技术，彻底改变了约束满足问题的求解方式。本文评估了Z3、CVC5和DPLL(T)等现代SMT求解器与经典DPLL SAT求解器在我们改进的数独生成器所创建的多样化25×25数独上的表现。这些数独涵盖多种难度级别，用于检验先进理论推理与编码技术的影响。结果表明，现代SMT求解器在处理大规模约束问题时显著优于传统SAT求解器。本研究展示了逻辑求解器的演进，并凸显了SMT求解器在解决大规模约束满足问题中的实际价值。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。