Reducing into a satisfiability (SAT) formulation has been proven effective in solving certain NP-hard problems. In this work, we extend this research by presenting a novel SAT formulation for computing the double-cut-and-join (DCJ) distance between two genomes with duplicate genes. The DCJ distance serves as a crucial metric in studying genome rearrangement. Previous work achieved an exact solution by transforming it into a maximum cycle decomposition (MCD) problem on the corresponding adjacency graph of two genomes, followed by reducing this problem into an integer linear programming (ILP) formulation. Using both simulated datasets and real genomic datasets, we firmly conclude that the SAT-based method scales much better and runs faster than using ILP, being able to solve a whole new range of instances which the ILP-based method cannot solve in a reasonable amount of time. This underscores the SAT-based approach as a versatile and more powerful alternative to ILP, with promising implications for broader applications in computational biology.