Wörz, FlorianReischuk, Rüdiger2024-10-022024-10-022024978-3-88579-982-5https://dl.gi.de/handle/20.500.12116/44731Beweiskomplexität ist ein Forschungsgebiet im Spannungsfeld zwischen Logik, Algorithmik und Komplexitätstheorie. Es untersucht die Ressourcen (z. B. Zeit oder Platz), die benötigt werden, um Aussagen mittels sogenannter Beweissysteme zu beweisen. Da jeder SAT-Solver implizit ein Beweissystem definiert, lassen sich Resultate in der Beweiskomplexität in Analysen von SAT-Solvern übersetzen. In der Dissertation [Wö23] des Autors werden zahlreiche neuen Verbindungen zwischen kombinatorischen Murmelspielen und Komplexitätsmaßen für aussagenlogische Beweissysteme bewiesen. Diese neuartigen Analysewerkzeuge ermöglichen es erstmals, den Speicherverbrauch verschiedener SAT-Solver-Paradigmen systematisch und mathematisch formal miteinander zu vergleichen. Zudem erlauben die Verbindungen die Analyse von Graphenisomorphieformeln mit Hilfe von Werkzeugen aus der endlichen Modelltheorie, genauer gesagt der deskriptiven Komplexitätstheorie. Diese Querverbindungen ermöglichen den Beweis von zahlreichen oberen und unteren Schranken der Größe von Widerlegungen von Graphenisomorphie. Insbesondere wird für verschiedenartige Graphenklassen (z. B. planare Graphen und Graphen mit verbotenen Minoren) gezeigt, dass diese kurze Beweise im geometrischen Schnittebenenverfahren besitzen. Für das Beweissystem Resolution entwerfen wir sogar Automatisierbarkeitsalgorithmen, die kurze Graphenisomorphiebeweise von speziellen Graphenklassen in polynomieller Zeit konstruieren.de10.18420/Diss2023-33