MiniPyDPLL: A Python Implementation of the DPLL Algorithm Inspired by MiniSAT

Abstract

MiniSAT, a renowned CDCL solver developed in C++, is lauded for its minimalist style, making it a great educational tool for efficient CDCL solver development. However, its comprehensive feature set, strict input parsing rules, extensive statistics reporting, and advanced techniques can make it challenging for beginners to grasp. In contrast, PyMiniDPLL is a simplified, Python-based implementation of the DPLL algorithm, inspired by MiniSAT's source code. It aims to serve as an educational tool for students and newcomers to the field of SAT solvers. This implementation excludes non-essential components for DPLL, thereby reducing complexity and focusing on core concepts like watched literals and variable heaps. The initial version assumes well-formed CNF inputs, prioritizing code clarity and instructional value over robustness. PyMiniDPLL serves as a stepping stone towards understanding and developing efficient CDCL solvers, providing a smoother learning curve compared to more complex solvers like MiniSAT. Future work includes creating detailed tutorials and potentially extending the implementation to cover CDCL solvers, offering a comprehensive educational pathway from DPLL to CDCL.