Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) are widely used in automated verification, but there is a lack of interactive tools designed for educational purposes in this field. To address this gap, we present EduSAT, a pedagogical tool specifically developed to support learning and understanding of SAT and SMT solving. EduSAT offers implementations of key algorithms such as the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and the Reduced Order Binary Decision Diagram (ROBDD) for SAT solving. Additionally, EduSAT provides solver abstractions for five NP-complete problems beyond SAT and SMT. Users can benefit from EduSAT by experimenting, analyzing, and validating their understanding of SAT and SMT solving techniques. Our tool is accompanied by comprehensive documentation and tutorials, extensive testing, and practical features such as a natural language interface and SAT and SMT formula generators, which also serve as a valuable opportunity for learners to deepen their understanding. Our evaluation of EduSAT demonstrates its high accuracy, achieving 100% correctness across all the implemented SAT and SMT solvers. We release EduSAT as a python package in .whl file, and the source can be identified at https://github.com/zhaoy37/SAT_Solver.

翻译：布尔可满足性（SAT）与可满足性模理论（SMT）在自动化验证领域得到广泛应用，但目前该领域缺乏面向教学目的的交互式工具。为填补这一空白，我们提出EduSAT——一款专为支持SAT与SMT求解学习与理解而开发的教学工具。EduSAT实现了SAT求解中的关键算法，如Davis-Putnam-Logemann-Loveland（DPLL）算法与简化有序二元决策图（ROBDD）。此外，EduSAT还为SAT与SMT之外的五个NP完全问题提供了求解器抽象。用户可通过实验、分析与验证对SAT及SMT求解技术的理解，从而受益于EduSAT。我们的工具配备了全面的文档与教程、广泛测试以及自然语言界面、SAT和SMT公式生成器等实用功能，这亦为学习者深化理解提供了宝贵机会。对EduSAT的评估表明其具有高精度，在所有已实现的SAT与SMT求解器中达到100%正确率。我们以.whl文件形式发布EduSAT的Python软件包，源代码可在https://github.com/zhaoy37/SAT_Solver 获取。