6. Pipeline Architecture

6.1 The components

The pipeline is the executable counterpart of all the preceding theory. Its pieces, and which theoretical notion each one corresponds to:

Component	Role	Corresponds to
Typed instances	represent $x \in \Sigma^*$ for each problem (`ThreeSAT`, `IndependentSet`, `VertexCover`, `Clique`, `SubsetSum`)	the language $L$ (1.1)
Per-type verifier	`Verify(instance, certificate) -> bool`, one per problem	the verifier $V$ (1.3)
Reduction $f$	a pure function `InstanceA -> InstanceB`	the witness of $A \le_p B$ (3.1)
Certificate map $g$	a pure function `CertificateB -> CertificateA`	the constructive direction of the biconditional (1.3, 5.4)
SAT oracle	decides `ThreeSAT` for real, in practical time	the reference algorithm the chain is anchored to (5.3)
Brute-force oracle	decides every other problem by enumerating candidates and calling `Verify`	the “naive” algorithm implicit in the definition of NP (1.3)
Instance generator	produces random `ThreeSAT` instances (property test)	the sampling that empirically corroborates the invariant (5.4)

Only ThreeSAT needs a generator and an efficient oracle: it is the only problem that appears as the source in every reduction of the chain (5.3), so it is the only one for which the project needs to handle instances of realistic size. Every other instance type in the pipeline is always born as the image of a reduction ($y = f(x)$) — it is never generated directly — and so stays as small as $x$ is.

6.2 Why two different oracles, not one

The choice to have a “real” oracle only for ThreeSAT, and a brute-force oracle for everything else, is not a shortcut: it is a direct consequence of the definition of NP given in 1.3.

For ThreeSAT, the project uses a real SAT solver (gophersat) because that is the task the project has stated from the very beginning — “verified end-to-end against a real SAT solver” — and it is also the only point in the pipeline where the oracle’s efficiency actually matters, since it is the only instance type generated directly and therefore potentially not tiny.
For every other problem (IndependentSet, VertexCover, …), an oracle based on exhaustive enumeration of candidate certificates, filtered by Verify, is correct by definition — it is literally the “try every $y$ with $|y| \le p(|x|)$” algorithm that NP’s certificate definition (1.3) guarantees to be correct, even if not efficient. No second industrial-strength solver is needed: it is enough that the instance stays small, which is guaranteed by the previous point (6.1).

This asymmetry also makes it clearer what the project is actually testing when it runs a property test: it is not testing whether gophersat is correct (that is taken as given — it is a third-party library), and it is not testing whether the brute-force oracle is correct (it is, by construction, being the direct enumeration of the definition). It is testing $f$ and $g$ — the only code written by this project in this chain — using the two oracles as a fixed reference point, independent of both sides of the reduction.

6.3 Data flow for a single test case

flowchart LR
    X["x : ThreeSAT — generated by rapid"] -->|DIMACS| S["solver oracle — gophersat"]
    S -->|"satOK, cert_A"| INV{"satOK == isOK ?"}
    X -->|"f — reduction under test"| Y["y = f(x) : IndependentSet"]
    Y --> BF["brute-force oracle — Verify on every candidate"]
    BF -->|"isOK, cert_B"| INV
    BF -->|"cert_B (if isOK)"| G["g(cert_B) = cert_A'"]
    G --> CV{"Verify(x, cert_A') ?"}

A single case generated by the property test goes through four checks, not one:

Construction: $y = f(x)$ — no check here, just execution of the reduction.
Double decision: the SAT oracle decides $x$, the brute-force oracle decides $y$, independently of each other.
Invariant $A(x) = B(f(x))$: the two boolean decisions (satOK, isOK) must agree — this is the verification of $f$’s correctness as a map that preserves the yes/no answer (Section 3.1).
Certificate: if isOK, $g$ is applied to the certificate found by the brute-force oracle and the result is verified directly on $x$, with ThreeSAT’s own verifier — this is a check independent from the third: a bug in $g$ that produces a wrong certificate would not make the invariant in point 3 fail (that one only concerns yes/no), but it would make this check fail. The two checks catch different classes of bugs, which is why they are kept separate instead of being collapsed into a single assertion.

If a case fails either check, rapid automatically shrinks the instance to a minimal counterexample, so the $x$ that ends up in the failure report is already the smallest one that breaks the invariant.

6.4 The DIMACS boundary

The DIMACS CNF format is the only point of contact between the project’s typed world and the solver — and this is a literal architectural commitment, not just a narrative framing: ThreeSAT does not hand gophersat its own native problem struct, it serializes to a DIMACS string and hands gophersat that, the same interface any other DIMACS-reading solver would accept. Serialization happens exclusively for ThreeSAT instances (the only type the solver needs to be able to read), in one direction only (instance → text), never having to deserialize CNF back into a data structure. This choice keeps the oracle swappable — any DIMACS-compatible solver could replace gophersat behind this one boundary, without touching a single reduction — and it is also the most literal boundary of the “reduction as compilation” metaphor adopted from the start: every reduction $f$ is a compilation between the project’s internal representations, while DIMACS emission is the only true “object code emission” toward an external tool.

6.5 Realization note in Go

The entire description above is language-independent (it was designed that way, even before deciding between Go and R). Its concrete realization, given that the choice landed on Go:

every typed instance is a dedicated Go struct (see Section 3, Clause3 [3]Literal included);
every reduction $f$ and every map $g$ is a free function with an explicit signature func(A) B;
the SAT oracle is gophersat, called in-process via its DIMACS-reading entry point — the DIMACS string built from ThreeSAT is handed straight to gophersat’s parser in memory, no subprocess and no temporary file, so “in-process” means same binary, not native struct API; the brute-force oracle is a single generic function (Go generics) parameterized over the instance type and the certificate type, reused for every problem other than ThreeSAT;
the generator and the test orchestration are a rapid.Check per reduction in the chain, following the scheme shown in 6.3.

6.6 Closing

With this section the report has completed the full circle announced at the start of the project: every reduction function in the code is a witness of $\le_p$ (Section 3); every property test comparing the two oracles is the correctness condition of Section 3.1 made executable; every map $g$ is the constructive direction of NP’s certificate definition (Section 1.3); and the entire chain rests, by transitivity (Section 4.3), on a single fixed point that is cited but not re-proved — Cook–Levin (Section 5). Theory and code remain two views of the same object, not two parallel projects.

#1 — #2 — #3 — #4 — #5 — #6