Mini Proof Complexity

A collection of from-scratch, zero-dependency C implementations of propositional proof complexity theory. Each module maps to MIT and other top-tier university courses, implementing proof systems, lower-bound constructions, and SAT search algorithms in runnable C code.

Sub-Modules

Sub-Module	Topics	Key Courses
mini-algebraic-proof-systems	Gröbner basis, Nullstellensatz refutations, polynomial calculus, degree lower bounds, clause-to-polynomial translation over GF(2)	MIT 6.841, Princeton COS 551
mini-clique-coloring-tautologies	Clique-coloring CNF encoding, Bonet-Pitassi-Raz exponential lower bounds, monotone interpolation, size-width tradeoffs	MIT 6.841, Stanford CS254, Berkeley CS278
mini-cutting-planes-proofs	Cutting Planes proof system, Chvátal-Gomory cuts, CP proof DAG, Pudlák lower bounds, pseudo-Boolean constraints	Princeton COS 551, CMU 15-855, Cambridge Part III
mini-frege-extended-frege	Frege systems, Extended Frege, axiom schemas, substitution, Reckhow's p-equivalence theorem, proof checking	MIT 6.841, Stanford CS358, Cambridge Part III
mini-pigeonhole-principle	PHP encoding (at-least-one + at-most-one), Haken's exponential resolution lower bound, width-size tradeoffs, weak PHP	MIT 6.841, Stanford CS254, Berkeley CS278
mini-proof-search-algorithms	DPLL backtracking, CDCL clause learning, VSIDS branching heuristic, restarts, preprocessing, implication graph analysis	MIT 6.841, Stanford CS254, Berkeley CS278
mini-resolution-lower-bounds	Resolution proof DAG, width-size tradeoffs (Ben-Sasson–Wigderson), feasible interpolation, random restrictions, proof graph analysis	MIT 6.841, Stanford CS254, Princeton COS 522
mini-tseitin-formulas	Tseitin transformation (circuit→equisatisfiable CNF), Tseitin tautologies on expander graphs, Urquhart lower bounds, GF(2) linear systems	MIT 6.841, Stanford CS254, CMU 15-855, Princeton COS 551

Design Philosophy

• Zero external dependencies — pure C (C99/C11), only libc and libm
• Self-contained modules — each directory has its own Makefile, include/, src/, examples/, demos/, tests/
• Theory-to-code mapping — every module includes docs/ with course-alignment notes and proof-complexity references
• Executable lower bounds — proof-size experiments, hardness analysis, and SAT solver benchmarks that run on real formulas

Building

Each module is standalone. Navigate to a module directory and run:

cd mini-algebraic-proof-systems
make all    # build everything
make test   # run tests

Requires GCC and GNU Make.

Project Structure

mini-proof-complexity/
├── mini-algebraic-proof-systems/   # Gröbner basis, Nullstellensatz, polynomial calculus
├── mini-clique-coloring-tautologies/ # Clique-coloring formulas & lower bounds
├── mini-cutting-planes-proofs/     # Cutting Planes proof system & Chvátal-Gomory cuts
├── mini-frege-extended-frege/      # Frege and Extended Frege proof systems
├── mini-pigeonhole-principle/      # PHP encoding & Haken's exponential lower bound
├── mini-proof-search-algorithms/   # DPLL, CDCL, branching heuristics, restarts
├── mini-resolution-lower-bounds/   # Resolution proof DAG, width-size tradeoffs
└── mini-tseitin-formulas/          # Tseitin transformation & expander lower bounds

License

MIT