评估大规模数独谜题中 SAT 与 SMT 求解器的性能
人工智能
2025-01-16 v1 计算机科学中的逻辑
摘要
现代 SMT 求解器通过集成先进的理论推理和编码技术，彻底革新了约束满足问题的求解方法。本文评估了 Z3、CVC5 和 DPLL(T) 等现代 SMT 求解器相对于标准 SAT 求解器（DPLL）的性能。通过在我们改进的数独生成器创建的新型多样化 25×25 数独谜题上进行基准测试，我们检验了先进理论推理和编码技术的影响。我们的发现表明，现代 SMT 求解器显著优于经典 SAT 求解器。这一工作凸显了逻辑求解器的演化，并体现了 SMT 求解器在解决大规模约束满足问题中的实用性。
引用
@article{arxiv.2501.08569,
title = {Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles},
author = {Liam Davis and Tairan Ji},
journal= {arXiv preprint arXiv:2501.08569},
year = {2025}
}