✅ SAT Solver

Boolean satisfiability via the DPLL algorithm

Overview

A SAT solver determines whether a Boolean formula in conjunctive normal form (CNF) has a satisfying assignment. This is the canonical NP-complete problem — the first problem proven NP-complete (Cook–Levin, 1971). Despite worst-case exponential time, modern SAT solvers handle millions of variables using clever heuristics.

This implementation uses the DPLL (Davis–Putnam–Logemann–Loveland) algorithm with unit propagation, pure literal elimination, and backtracking. Includes support for DIMACS CNF parsing and solution verification.

Concepts Demonstrated

Algebraic data types — literals as Pos | Neg variants
Pattern matching — clause evaluation and propagation
Backtracking search — systematic exploration of variable assignments
Unit propagation — forced assignments from unit clauses
Pure literal elimination — variables appearing in only one polarity
Immutable maps — persistent assignment tracking for backtracking
NP-completeness — the foundation of computational complexity

The DPLL Algorithm

(* CNF formula: (a ∨ ¬b) ∧ (b ∨ c) ∧ (¬a ∨ ¬c) *)
let formula = [
  [Pos 1; Neg 2];       (* a ∨ ¬b *)
  [Pos 2; Pos 3];       (* b ∨ c  *)
  [Neg 1; Neg 3];       (* ¬a ∨ ¬c *)
]

(* DPLL proceeds by:
   1. Unit propagation — if a clause has one unset literal, force it
   2. Pure literal elim — if a var appears only positive (or only
      negative), assign it to satisfy all those clauses
   3. Choose — pick an unassigned variable, try true then false
   4. Backtrack — if a conflict is found, undo and try the other branch
*)

match solve formula with
| Some assignment -> (* satisfying assignment found *)
| None            -> (* formula is unsatisfiable *)

Key Functions

Function	Description
`solve formula`	Find satisfying assignment or return None
`unit_propagate`	Find and propagate unit clauses (single-literal)
`pure_literal_elim`	Assign variables appearing in only one polarity
`simplify`	Remove satisfied clauses and falsified literals
`variables`	Collect all variables in a formula
`eval_clause`	Evaluate clause under partial assignment
`eval_formula`	Evaluate entire formula under assignment
`parse_dimacs`	Parse standard DIMACS CNF format
`verify`	Verify a solution against the original formula

DPLL Optimizations

Technique	Effect
Unit propagation	Forced deductions — dramatically prunes the search tree
Pure literal elimination	Variables that only appear positive (or negative) can be set freely
Early termination	Stop as soon as a clause is falsified (no need to check the rest)
Immutable assignments	Backtracking is free — just discard the current map

Applications of SAT Solving

Hardware verification — checking circuit correctness (Intel, AMD)
Software verification — bounded model checking for bug finding
Planning & scheduling — encoding constraints as Boolean formulas
Cryptanalysis — attacking ciphers by encoding as SAT
Package managers — dependency resolution (apt, opam)
Sudoku & puzzles — constraint satisfaction via CNF encoding

CNF Format

(* DIMACS CNF — standard interchange format *)
(* p cnf <num_vars> <num_clauses> *)
(* Each line: space-separated literals, 0-terminated *)
(* Positive int = positive literal, negative = negation *)

p cnf 3 3
1 -2 0       (* a ∨ ¬b *)
2 3 0        (* b ∨ c  *)
-1 -3 0      (* ¬a ∨ ¬c *)

(* Parse with: parse_dimacs input_string *)