Guided Labs

Complete five offline labs implementing eight graph operations with verifiable outputs. Budget 21–30 focused hours including proof, debugging and evidence. Download the Python lab package.

Extract the archive, open its graph-algorithms folder, and use Python 3.10+:

python check.py --module reference
python run_labs.py --module reference --output results-reference.json

Implement starter.py, then repeat with --module starter. The untouched starter deliberately fails. The README specifies types, errors, edge identity, numeric domains, output semantics, allowed primitives and complete cost models. Everything runs offline with the standard library.

Lab	Required implementation	Evidence	Time
A: structure	BFS, iterative Kosaraju, Kahn order	Parent edge paths, SCC partition, edge-respecting permutation or cycle failure	5–7 h
B: routes	Dijkstra and Bellman–Ford	Finite path witnesses and precise unreachable/unbounded statuses	5–7 h
C: connection	Kruskal minimum spanning forest	Edge identities, connectivity, acyclicity and optimum weight	3–5 h
D: capacity	Edmonds–Karp	Feasible per-edge flow and equal-value residual cut	5–7 h
E: reduction	Bipartite maximum matching	Distinct endpoints, allowed pairs, optimal cardinality and two-way proof	3–4 h

Fixture interpretation

The deterministic report gives BFS distances [0,1,2,3,null]; SCCs [[0,1],[2],[3],[4]]; no topological order for the cyclic fixture; Dijkstra distances [0,2,1,4]; Bellman–Ford [0,"unbounded","unbounded","unbounded",7,null]; forest total 1; flow value 2; and matching pairs (0,1),(1,0). Other fixtures and tests check edge cases. Alternative valid witnesses need not match the reference, but two runs of the same implementation should reproduce their report.

Falsification and repair

Try deliberate faults: omit transpose in SCC; conflate first discovery with shortest distance; mark all reachable vertices unbounded after any negative cycle; accept cycles in a forest; omit reverse residual updates; choose a greedy maximal matching. Preserve the smallest failing graph and explain the violated invariant, then restore the correct implementation and test a fresh case.

Small exhaustive/seeded oracles and output certificates are independent feedback, not complexity proofs. Source review must establish iterative traversal semantics, heap handling, union-find bookkeeping and residual updates. A library graph call is not an implementation of the learning task; deque, heapq and sorting edge IDs are permitted primitives. Certificates and Engineering Contracts explains the proof obligations. Submit the included evidence template.