EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability

TL;DR

EduSAT is an educational tool designed to facilitate learning and understanding of SAT and SMT solving techniques through interactive algorithms, problem solvers, and comprehensive tutorials, enhancing pedagogical approaches in formal methods.

Contribution

The paper introduces EduSAT, a novel pedagogical platform with implementations of key SAT/SMT algorithms, solver abstractions for NP-complete problems, and user-friendly features for educational purposes.

Findings

Achieves 100% correctness in SAT and SMT solvers.

Provides comprehensive tutorials and natural language interface.

Supports experimentation with multiple NP-complete problems.

Abstract

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.