The paper introduces a novel SAT-based approach to graph generation and enumeration, termed SAT Modulo Symmetries (SMS). SMS leverages the interaction between a Conflict-Driven Clause Learning (CDCL) SAT solver and a symmetry propagator to dynamically check the minimality of partially defined graphs during the solving process. This approach offers several advantages over static symmetry breaking, including early detection of symmetries, seamless integration into the CDCL procedure, and complete symmetry breaking without a prohibitively large initial encoding. The authors implement SMS to generate extremal graphs with specific restrictions, such as forbidden subgraphs and diameter. They confirm the Murty–Simon Conjecture on diameter-2-critical graphs for graphs up to 19 vertices and prove the exact number of Ramsey graphs $\mathcal{R}(3, 5, n)$ and $\mathcal{R}(4, 4, n)$. The experimental results show that SMS performs well, particularly on unsatisfiable instances, and significantly reduces the time spent on SAT solving compared to static symmetry breaking. The paper also provides a detailed theoretical foundation, including definitions of graphs, satisfiability, and static symmetry breaking. It outlines the integration of SMS into the CDCL algorithm and introduces the concept of partially defined graphs, along with algorithms for finding indicator pairs and constructing obstructions. The correctness and efficiency of the proposed methods are demonstrated through various examples and theoretical proofs.The paper introduces a novel SAT-based approach to graph generation and enumeration, termed SAT Modulo Symmetries (SMS). SMS leverages the interaction between a Conflict-Driven Clause Learning (CDCL) SAT solver and a symmetry propagator to dynamically check the minimality of partially defined graphs during the solving process. This approach offers several advantages over static symmetry breaking, including early detection of symmetries, seamless integration into the CDCL procedure, and complete symmetry breaking without a prohibitively large initial encoding. The authors implement SMS to generate extremal graphs with specific restrictions, such as forbidden subgraphs and diameter. They confirm the Murty–Simon Conjecture on diameter-2-critical graphs for graphs up to 19 vertices and prove the exact number of Ramsey graphs $\mathcal{R}(3, 5, n)$ and $\mathcal{R}(4, 4, n)$. The experimental results show that SMS performs well, particularly on unsatisfiable instances, and significantly reduces the time spent on SAT solving compared to static symmetry breaking. The paper also provides a detailed theoretical foundation, including definitions of graphs, satisfiability, and static symmetry breaking. It outlines the integration of SMS into the CDCL algorithm and introduces the concept of partially defined graphs, along with algorithms for finding indicator pairs and constructing obstructions. The correctness and efficiency of the proposed methods are demonstrated through various examples and theoretical proofs.