Network modularity is central to understanding phenomena in diverse domains, from biology and social science to engineering and computational physics. However, computing the optimal modularity—an NP-hard measure quantifying community strength—has remained computationally intractable at large scales. Most approaches resort to heuristics without formal optimality guarantees. This paper contributes to the computational science of complex systems by introducing a novel MaxSAT-based framework that can compute optimal network modularity values for larger networks than previously possible. Leveraging this new capability, we extensively evaluate heuristic solutions and, for the first time, include the state-of-the-art memetic graph clustering heuristic VieClus. Remarkably, VieClus identifies optimal modularity values for all tested networks, ranging from 103 previously studied instances to 52 new, larger ones, and does so in seconds. This result contrasts with earlier conclusions that heuristics frequently fail to find the optimal modularity. By combining a powerful MaxSAT encoding, which supports proof logging for verification, with a fast and effective heuristic, we demonstrate that even intricate network structures can be tackled efficiently. This synergy brings us closer to making complex network analysis and community detection tractable, robust, and verifiable—a goal firmly aligned with the core mission of computational science.