= Conclusion
In this thesis, a novel approach to @dd\-based quantum circuit equivalence checking was developed.
This approach uses the fact that a system matrix multiplied by its inverse produces the identity.
Gates from either circuit are sequentially applied to the @dd, which is reduced to the identity if the circuits are equivalent.
Using solutions to the @lcs problem, commonly known as diff algorithms, a scheme was developed that seeks to keep the system's @dd as close to the identity as possible by exploiting structural similarities in the circuits.

Over the course of the work, Djikstra's algorithm, Myers' algorithm and the patience algorithm were analysed and implemented.
The functionality of these algorithms and their applicability to quantum circuits represented as sequences of gates was demonstrated using a visualisation tool.
This also highlights the structural relationship between circuits at different stages of compilation.
Myers' algorithm and the patience algorithm were subsequently integrated into @mqt @qcec and successfully applied to the equivalence checking problem.
Finally, a specialised benchmarking tool was developed for @mqt @qcec to compare application schemes using benchmark instances generated by @mqt Bench.

The extensive exploration carried out in this work shows both the possible advantages of using a heuristic based on diff algorithms, as well as the limits of this approach.
While significant speed ups are demonstrated, many of the explored approaches tend to cause regressions in the run time of the equivalence checking procedure.

Specifically, the proposed application scheme based on a processed edit script produced by the Myers' algorithm can speed up equivalence checking by almost 60% in the right circumstances.
In many other cases, however, it fails to provide any meaningful speed-up or even reduces the speed of computation by a factor of up to 400%.
While there is no apparent correlation between the easily analysable properties of the circuits and the run time improvement of using a diff-based application scheme, a heuristic based on the gate equivalence rate of the two circuits manages to filter out most bad instances.

The culmination of this work is an application scheme that can be applied selectively to accomplish an average speed-up of 7.09% compared to the state-of-the-art application scheme.
Additionally, the developed open-source tooling will certainly prove useful to further research on quantum circuit verification.
@mqt @qcec Bench is especially significant as it greatly simplifies further large-scale tests of methodologies in @qcec.

