Sequential logic synthesis expands the solution space compared to combinational logic synthesis by reasoning about the reachable states of memory elements, leading to better Power-Performance-Area (PPA) outcomes. As gate costs continue to rise in advanced technologies, sequential logic synthesis is gaining significant traction within the EDA community as a powerful alternative. This paper introduces a scalable algorithm for don’t-care-based sequential logic synthesis, leveraging sequential k-step induction to perform redundancy removal and resubstitution under Sequential Observability Don’t Cares (SODCs). SODCs generalize Observability Don’t Cares (ODCs) by explicitly considering reachable states, making SODC-based optimization a challenging problem due to dependencies and alignment issues between the base case and inductive case in k-step induction. Our approach overcomes these challenges, fully utilizing the potential of SODCs without limiting the solution space. We rigorously prove the correctness of our approach, discuss some limitations arising from bounded-step induction, and analyze how our approach can effectively be used in practice to exploit obscure optimization opportunities. Implemented as part of an industrial tool, our algorithm achieves an average -6.9% area improvement after technology mapping compared to state-of-the-art sequential synthesis methods, and further provides 3.16% and 1.06% reductions in combinational and sequential areas, respectively, in post place-and-route results. Furthermore, all optimizations are efficiently verified using industrial sequential verification tools.