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

要約

ブール満足度 (SAT) と満足度モジュロ理論 (SMT) は自動検証で広く使用されていますが、この分野では教育目的で設計された対話型ツールが不足しています。
このギャップに対処するために、SAT および SMT 解決の学習と理解をサポートするために特別に開発された教育ツールである EduSAT を紹介します。
EduSAT は、SAT を解くための Davis-Putnam-Logemann-Loveland (DPLL) アルゴリズムや Reduced Order Binary Decision Diagram (ROBDD) などの主要なアルゴリズムの実装を提供します。
さらに、EduSAT は、SAT と SMT を超えた 5 つの NP 完全問題に対するソルバー抽象化を提供します。
ユーザーは、SAT および SMT の解決手法を実験、分析、理解していることを検証することで、EduSAT の恩恵を受けることができます。
私たちのツールには、包括的なドキュメントとチュートリアル、広範なテスト、自然言語インターフェイスや SAT および SMT の数式ジェネレーターなどの実践的な機能が付属しており、学習者が理解を深められる貴重な機会としても役立ちます。
EduSAT の評価では、実装されたすべての SAT および SMT ソルバーにわたって 100% の正確性を達成し、その精度が高いことが実証されました。
EduSAT は .whl ファイルの Python パッケージとしてリリースされており、ソースは https://github.com/zhaoy37/SAT_Solver で確認できます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google