In graph theory, a vertex cover is a set of vertices that includes at least one endpoint of every edge in a graph — for street cameras, that means the smallest set of intersections that still watches every street segment. Calculating the minimum vertex cover is NP-hard, which is what made this one a doozy to write.
Street database — Python
A Python process adds street names and segments to a database, then computes every vertex and edge from what's been entered.
Shortest path — C++
Converts the edge list into an adjacency list and runs a DFS to find the shortest path between two vertices in the street database.
Encoding into SAT — C++
The actual minimum-vertex-cover step: encoding the database's intersections and edges into a propositional formula in CNF, solved with Minisat 2.
Driver program — C++
Runs the programs above as forked processes, piping inputs and outputs between them. It includes a random street generator that feeds the Python process, which in turn feeds the shortest-path and SAT programs.
Optimized SAT encoding — C++
Two additional approximation algorithms alongside a 3-SAT reduction, run on multiple threads concurrently, to improve on the runtime of the original SAT encoding.