This paper introduces a novel SAT-based approach called SAT Modulo Symmetries (SMS) for generating and enumerating graphs. The approach combines a Conflict-Driven Clause Learning (CDCL) SAT solver with a special symmetry propagator that checks partially generated graphs for minimality with respect to a lexicographic ordering during the solving process. This method offers several advantages over static symmetry breaking: (i) symmetries are detected early in the generation process, (ii) symmetry breaking is seamlessly integrated into the CDCL procedure, and (iii) the propagator performs a complete symmetry breaking without causing a prohibitively large initial encoding. The approach is instantiated by generating extremal graphs with certain restrictions in terms of forbidden subgraphs and diameters. The paper confirms the Murty–Simon Conjecture (1979) on diameter-2-critical graphs for graphs up to 19 vertices and proves the exact number of Ramsey graphs R(3,5,n) and R(4,4,n). The paper discusses the use of SAT solving for graph generation and enumeration, emphasizing the importance of dynamic symmetry breaking. It introduces the concept of partially defined graphs and the algorithm MINCHECK, which checks their minimality. The algorithm MINCHECK is integrated into the CDCL solver to detect and handle symmetry breaking dynamically. The paper also presents a procedure for constructing obstructions, which are used to block certain graphs during the search. The approach is tested on three prominent problems in Extremal Graph Theory, including graphs with a prescribed minimum girth, diameter-2-critical graphs, and Ramsey numbers. The results show that SMS performs well, particularly on unsatisfiable instances, and can generate proofs for the generated graphs. The paper concludes that SMS is an effective approach for generating and enumerating graphs, offering a dynamic symmetry breaking method that is more efficient and effective than static symmetry breaking. The method is implemented and tested, demonstrating its effectiveness in solving complex graph generation problems.This paper introduces a novel SAT-based approach called SAT Modulo Symmetries (SMS) for generating and enumerating graphs. The approach combines a Conflict-Driven Clause Learning (CDCL) SAT solver with a special symmetry propagator that checks partially generated graphs for minimality with respect to a lexicographic ordering during the solving process. This method offers several advantages over static symmetry breaking: (i) symmetries are detected early in the generation process, (ii) symmetry breaking is seamlessly integrated into the CDCL procedure, and (iii) the propagator performs a complete symmetry breaking without causing a prohibitively large initial encoding. The approach is instantiated by generating extremal graphs with certain restrictions in terms of forbidden subgraphs and diameters. The paper confirms the Murty–Simon Conjecture (1979) on diameter-2-critical graphs for graphs up to 19 vertices and proves the exact number of Ramsey graphs R(3,5,n) and R(4,4,n). The paper discusses the use of SAT solving for graph generation and enumeration, emphasizing the importance of dynamic symmetry breaking. It introduces the concept of partially defined graphs and the algorithm MINCHECK, which checks their minimality. The algorithm MINCHECK is integrated into the CDCL solver to detect and handle symmetry breaking dynamically. The paper also presents a procedure for constructing obstructions, which are used to block certain graphs during the search. The approach is tested on three prominent problems in Extremal Graph Theory, including graphs with a prescribed minimum girth, diameter-2-critical graphs, and Ramsey numbers. The results show that SMS performs well, particularly on unsatisfiable instances, and can generate proofs for the generated graphs. The paper concludes that SMS is an effective approach for generating and enumerating graphs, offering a dynamic symmetry breaking method that is more efficient and effective than static symmetry breaking. The method is implemented and tested, demonstrating its effectiveness in solving complex graph generation problems.