rmpca 0.1.1

Enterprise-grade route optimization engine — Chinese Postman Problem solver with Eulerian circuit detection, Lean 4 FFI boundary, and property-based testing
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

//! Strongly connected component filtering for directed graphs.
//!
//! // Aligns with Lean4: theorem `scc_retain_largest_preserves_connectivity`

use crate::optimizer::error::RouteError;
use crate::optimizer::types::Node;
use petgraph::graph::{DiGraph, NodeIndex};
use petgraph::algo::kosaraju_scc;
use petgraph::visit::EdgeRef;
use std::collections::HashMap;

/// Utility for filtering graphs to their strongly connected components.
pub struct SccFilter;

impl SccFilter {
    /// Retain only the largest strongly connected component in a directed graph.
    ///
    /// # Errors
    /// Returns `RouteError::NoStronglyConnectedComponent` if the graph has no SCCs.
    ///
    /// // Aligns with Lean4: theorem `retain_largest_preserves_reachability`
    pub fn retain_largest<E: Clone>(
        graph: &DiGraph<Node, E>
    ) -> Result<DiGraph<Node, E>, RouteError> {
        if graph.node_count() == 0 {
            return Ok(DiGraph::new());
        }

        // Find all SCCs using Kosarajus algorithm
        let sccs = kosaraju_scc(graph);
        
        // Find the largest SCC
        let largest_scc = sccs.into_iter()
            .max_by_key(Vec::len)
            .ok_or(RouteError::NoStronglyConnectedComponent)?;

        // Rebuild graph with only nodes in the largest SCC
        let mut new_graph = DiGraph::new();
        let mut old_to_new: HashMap<NodeIndex, NodeIndex> = HashMap::with_capacity(largest_scc.len());

        // Add nodes
        for &old_idx in &largest_scc {
            let node = graph[old_idx].clone();
            let new_idx = new_graph.add_node(node);
            old_to_new.insert(old_idx, new_idx);
        }

        // Add edges
        for &old_idx in &largest_scc {
            let new_from = old_to_new[&old_idx];
            for edge in graph.edges(old_idx) {
                if let Some(&new_to) = old_to_new.get(&edge.target()) {
                    new_graph.add_edge(new_from, new_to, edge.weight().clone());
                }
            }
        }

        Ok(new_graph)
    }
}