Komplexitätsmaße für die Lösung von aussagenlogischen Formeln.

• Antragsteller: Professor Dr. Jacobo Torán
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 430150230

Das Erfüllbarkeitsproblem der Aussagenlogik, SAT, ist das am besten bekannte NP-vollständige Problem und wird als solches als ein sehr schwer zu lösendes Problem angesehen. In den letzten Jahrzehnten waren jedoch einige beeindruckende Fortschritte in der Entwicklung von Programmen zur Lösung von SAT-Instanzen zu beobachten, wodurch heutzutage reale Anwendungen mit hunterttausenden Variablen gelöst werden können.Wir haben vor, ein besseres Verständnis für diese Lücke zwischen Praxis und Theorie zu erlangen. Dabei fokussieren wir uns darauf, wie mehrere Komplexitätsmaße für die grundlegenden Beweissysteme moderner SAT-Solver (hauptsächlich Resolution) in Schätzungen bezüglich Laufzeit und Suchstrategien von SAT Programmen übersetzt werden können.Wir beabsichtigen die Zusammenhänge und trade-offs zwischen den verschiedenen Komplexitätsmaßen für Resolution zu untersuchen, als auch ein besseres Verständnis über Formeln zu erlangen, auf denen SAT-Solver gute Leistungen erziehlen. Wir haben auch vor, probabilistische local search Algorithmen für unerfüllbare Formeln zu entwickeln und die Zusammenhänge zwischen deren Analyse und der Untersuchung von Platzkomplexitätaßen für Resolution zu erforschen. Wir werden auch die klassische und parametrisierte Komplexität von mehreren Beweiskomplexitätsfragen untersuchen.

• DFG-Verfahren: Sachbeihilfen