Alterierende Suche in der Kombinatorik mit SAT (ASK-SAT)

Viele ungelöste Probleme der diskreten Mathematik und extremalen Kombinatorik lassen sich als Frage formulieren, ob ein kombinatorisches Objekt mit einer bestimmten Eigenschaft und Größe existiert. Das Projekt erforscht neue Methoden zur Beantwortung solcher Fragen unter Verwendung des innovativen SAT Modulo Symmetries (SMS) Ansatzes. Dieser Ansatz weicht von traditionellen Suchstrategien ab, indem er systematisch redundante Teilkonfigurationen dynamisch identifiziert und ausschließt. Als zentrales Werkzeug werden mächtige Solver für das aussagenlogische Erfüllbarkeitsproblem (SAT) eingesetzt. Das Projekt zielt darauf ab, die Fähigkeiten von SMS zu erweitern, um effektiv die Existenz von Objekten zu entscheiden, deren definierende Eigenschaft Quantorenalternierungen erfordert, was über den Anwendungsbereich konventioneller SAT-Methoden hinausgeht. Dies beinhaltet die Integration fortgeschrittener computergestützter Werkzeuge wie quantifizierte Boolesche Formeln und Techniken zur Symmetriebrechung. Durch diese Forschung strebt das Projekt an, die Bereiche des automatisierten Schließens und der diskreten Mathematik voranzutreiben.