SAT Solver

A Python implementation of a SAT (Boolean Satisfiability) solver using well-known optimization techniques. This solver determines whether a formula in Conjunctive Normal Form (CNF) is satisfiable.

Overview

This project implements practical SAT-solving techniques including:

• Unit Propagation: Simplifies the formula by assigning values to unit clauses
• Pure Literal Elimination: Assigns values to literals that appear only in one polarity
• DPLL Branching: Systematic search with backtracking on partial truth assignments
• Performance Optimization: Multiple optimization iterations improving runtime by several orders of magnitude over the initial naive implementation

Why This Project Matters

SAT solving is fundamental to computational logic and has practical applications in:

• Hardware Verification: Testing correctness of circuit designs
• Constraint Satisfaction: Solving complex combinatorial problems
• Planning & Scheduling: Automated reasoning for logistics

This project demonstrates how careful algorithm implementation and optimization can dramatically improve performance on NP-complete problems.

How to Run

Prerequisites

• Python 3.6+

Run the Solver

Each question file (q4 through q8) implements increasingly complex solver variants:

python q8.py

The q8.py file contains the complete, optimized solver implementation.

Input Format

The solver accepts formulas in CNF format. See the input/ directory for example test cases.

Project Structure

.
├── q4.py                    # Basic SAT solver implementation
├── q5.py                    # Solver with unit propagation
├── q6.py                    # Pure literal elimination added
├── q7.py                    # Optimized branch selection
├── q8.py                    # Final, fully optimized solver
├── input/                   # Test case CNF formulas
├── planning/                # Design notes and algorithm documentation
├── CT_coursework_2023.pdf   # Coursework specification and theory
└── Logic coursework Q&A.txt # Q&A on solver design

Skills Demonstrated

• Algorithm Design: Implementing DPLL and SAT-solving techniques from first principles
• Performance Optimization: Profiling and iterative optimization achieving exponential speedup
• Python: Clean code structure with functional decomposition
• Theoretical Computer Science: Understanding NP-completeness and satisfiability

Notes

This was completed as university coursework but is structured as a legitimate algorithm implementation. The progression from q4–q8 demonstrates optimization thinking: each version adds a technique that substantially improves performance.