An exploration of the DPLL SAT solver and its behavior around the phase transition in random 3-SAT instances.
This project implements the DPLL (Davis–Putnam–Logemann–Loveland) backtracking algorithm and examines phase transitions in SAT solving. It includes both a baseline implementation and a variant using the MOMS (Maximum Occurrences in Minimum-size clauses) heuristic for comparison.
- Grammar — Formal grammar specification for the SAT instances
- Research Paper — Full analysis and findings
Requires Python 3.13.2. Install dependencies:
pip install -r requirements.txtRun the solver:
python main.py -n 20 -l 85Options:
-n— Number of variables (default: 20)-l— Number of clauses (default: 85)--heuristic— Use MOMS heuristic
Run tests:
pytest tests/src/solver.py— DPLL solver implementationsrc/generator.py— Random 3-SAT instance generatorsrc/parser.py— Parsing utilitiesanalysis.ipynb— Analysis and experimental results