Die Ausnutzung von Symmetrien hat einen großen Einfluss auf die Effizienz praktischer Algorithmen in vielen verschiedenen Bereichen. Egal wo und wie Symmetrien verwendet werden, wird eine effiziente Möglichkeit benötigt, um Symmetrien zunächst zu berechnen. Dafür werden kombinatorische Strukturen in der Praxis üblicherweise als Graphen modelliert. Die Automorphismengruppe dieses Modellgraphen entspricht dann den Symmetrien der kombinatorischen Struktur. Ein Graphisomorphie-Algorithmus wird anschließend verwendet, um die Automorphismengruppe des Modellgraphen zu berechnen. Praktische Graphisomorphie-Algorithmen werden seit über 50 Jahren entwickelt. Obwohl alle modernen praktische Algorithmen auf demselben Prinzip basieren, nämlich dem Individualization-Refinement (IR) Paradigma, gibt es dennoch große Unterschiede zwischen den Implementierungen. Dies wiederum führt zu großen Leistungsunterschieden zwischen den Algorithmen. Obwohl die praktische Graphisomorphie schon oft als "gelöst" bezeichnet wurde, ist in der Tat kein einziger praktischer Algorithmus in der Lage, alle Graphen aus den verschiedenen Anwendungsbereichen effizient zu lösen. Es gibt sogar einzelne Anwendungen, in denen es keiner der Algorithmen schafft, alle Graphen effizient zu lösen. Idealerweise gäbe es einen einzigen Algorithmus, der auf allen Graphen schnell ist.

Die vorliegende Arbeit beschäftigt sich mit dem Entwurf eines neuen Algorithmus, dejavu, für die Erkennung von Symmetrien auf Graphen. Anstatt ad-hoc nach einer besseren Implementierung zu suchen, führen wir eine theoretische Analyse der wesentlichen algorithmischen Bestandteile des IR Paradigmas durch. Ein zentrales Ergebnis ist ein theoretisches Modell für die Backtracking-Strategien moderner praktischer Algorithmen. Wir beweisen, dass ein bestimmter Monte-Carlo Algorithmus innerhalb des Modells optimal bis auf logarithmische Faktoren ist. Ein Monte-Carlo Algorithmus kann Zufall in Berechnungen miteinbeziehen, und darf mit einer begrenzten Wahrscheinlichkeit Fehler machen. Insbesondere beweisen wir, dass in unserem Modell probabilistische Strategien beweisbar besser sind als deterministische. Die Monte-Carlo Strategie ist asymptotisch schneller als alle anderen Strategien, die in der Praxis verwendet werden. Weitere theoretische Resultate beinhalten eine konstruktive Charakterisierung der Backtracking-Bäume, sowie eine Analyse von Design-Entscheidungen im sogenannten Color Refinement Algorithmus.

Das Design von dejavu basiert auf unseren neuen theoretischen Erkenntnissen. Insbesondere verwendet dejavu eine Monte-Carlo Backtracking-Strategie. Darüber hinaus besteht der Solver aus vielen weiteren praktischen Komponenten, die dafür entwickelt wurden, die Monte-Carlo Strategie zu unterstützen. Eine dieser Komponenten ist ein Preprocessor, der auch mit allen anderen modernen Implementierungen verwendet werden kann. Eine experimentelle Analyse auf einer weitreichenden Kollektion von Graphen demonstriert anschließend, dass dejavu auf der großen Mehrheit der Graphklassen signifikant schneller ist als alle anderen Implementierungen.