Karp All-Reductions Pipeline
An explicit, typed pipeline of reductions between NP-complete problems, verified end-to-end against a real SAT solver — “reduction as compilation”. The name is Richard Karp’s, the author of the polynomial many-one reductions this project implements and of the 21 NP-complete problems that they connect.
What it is
Every reduction between two NP-complete problems (e.g. 3-SAT → Independent Set) is implemented as a pure function f: InstanceA -> InstanceB, paired with an inverse map on certificates g: CertificateB -> CertificateA. Correctness is not just claimed: it is put to the test with property-based testing, comparing on randomly generated instances the answer of a real SAT solver (for 3-SAT) against a reference oracle for the reduced problem, and checking that g always reconstructs a valid certificate.
The reduction chain (deliberately small, to stay a self-contained project — see Project status below for how much of it is actually built so far):
| From | To | Note |
|---|---|---|
| 3-SAT | Independent Set | |
| Independent Set | Vertex Cover | set complement: same graph, S ↔ V∖S |
| Independent Set | Clique | graph complement: same S, in Ḡ |
| 3-SAT | Subset Sum |
Vertex Cover and Clique are both one step from Independent Set, not from each other: Vertex Cover complements the vertex set (k' = |V| − k); Clique complements the graph and keeps the same set and k. The two g certificate maps are correspondingly different (set-complement vs. identity).
3-SAT is taken as the root of the chain — its NP-completeness is cited (the Cook–Levin theorem) and assumed, not re-proved in code.
Language: Go. Chosen over R after a direct comparison on three axes: static types make each reduction’s structural invariants (e.g. a clause has exactly 3 literals) checked by the compiler instead of at runtime; rapid’s property-testing generators are plain imperative Go code with automatic shrinking, versus the more combinator-heavy style the same thing needs in R’s hedgehog; and the only in-process SAT binding available for R, rpicosat, has been archived from CRAN since 2022 — installable only from source, a maintenance risk this project prefers not to carry rather than a hard blocker on its own.
Project status
- Theoretical report (sections 1–6)
- Types and verifiers for 3-SAT and Independent Set
- Reduction 3-SAT ≤p Independent Set (
fand its certificate mapg) - Brute-force reference oracle
- Real SAT oracle (
gophersat, via DIMACS) - Property-based test for 3-SAT → Independent Set
- Reduction Independent Set ≤p Vertex Cover
- Reduction Independent Set ≤p Clique
- Reduction 3-SAT ≤p Subset Sum
- Property tests for the three reductions above
Project layout
| File | What it is |
|---|---|
go.mod, go.sum |
Go module definition (github.com/matteogiorgi/karp) and its two dependencies, gophersat and rapid. |
doc.go |
Package-level doc comment: what the package is, and how to read it alongside docs/. |
threesat.go |
Types and verifier for 3-SAT — Literal, Clause3, ThreeSAT, Assignment — the root problem of the reduction chain. |
threesat_test.go |
Table-driven tests for ThreeSAT.Verify, including the duplicate-literal case a padded clause produces. |
independent_set.go |
Types and verifier for Independent Set — Graph, IndependentSet, VertexSet — the first problem reduced from 3-SAT. |
independent_set_test.go |
Table-driven tests for IndependentSet.Verify. |
threesat_to_independent_set.go |
The reduction f = ThreeSATToIndependentSet (3-SAT ≤p Independent Set) and its certificate map g = CertificateToAssignment. |
threesat_to_independent_set_test.go |
Structural test of the graph f builds, plus a hand-worked round trip through f, g, and both Verify methods. |
oracle.go |
The generic brute-force reference oracle BruteForceOracle (enumerate every candidate certificate, call Verify), and SolveIndependentSet, its instantiation for IndependentSet. |
oracle_test.go |
Tests for both the “yes” and “no” sides of the oracle, the universe-size safety cap, and its agreement with ThreeSATToIndependentSet end to end. |
threesat_oracle.go |
DIMACS, the literal boundary to the solver, and SolveThreeSAT, the real SAT oracle — gophersat called in-process via its DIMACS-reading entry point. |
threesat_oracle_test.go |
The exact DIMACS text for a hand-picked formula, the “yes” and “no” sides of the real oracle, and end-to-end agreement with the reduction and the brute-force oracle. |
property_test.go |
genThreeSAT, the one rapid generator this project needs, and the property test running the four-check pipeline of docs/06-pipeline-architecture.md, §6.3 on hundreds of random instances. |
docs/ |
The theoretical report — see Theoretical report below for the section-by-section index. |
DEVLOG.md |
A running record of concrete bugs and design gaps found while building this project, and what was done about them — both in the GitHub Pages rendering pipeline and in the Go implementation. |
Theoretical report
- Decision Problems, P and NP — languages, the class P, NP via verifier+certificate, the equivalence with nondeterministic Turing machines, and the NP/co-NP asymmetry.
- What Complexity Classes Are For — they classify the problem not the algorithm, they are robust with respect to the model of computation, they give a common vocabulary across domains, they transfer negative results.
- Polynomial Many-One Reductions — Karp’s definition, and why the project uses only that (and not the more general Turing/Cook reductions).
- What Reductions Are For — transferring difficulty in both directions, the order induced by
≤p, and the notion of completeness. - Cook–Levin and Practice — the Cook–Levin theorem as the root, the SAT → 3-SAT normalization, and the two-step recipe used by every subsequent reduction.
- Pipeline Architecture — the code’s components (typed instances, reductions, oracles, the DIMACS boundary) and their one-to-one correspondence with the sections above.