Textdokument
Kombinatorische Spiele als Schlüssel in der Komplexitätsanalyse aussagenlogischer Formeln
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Zusatzinformation
Datum
2024
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
Beweiskomplexitä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.