SMT Techniken für arithmetische Theorien

• Antragstellerin: Professorin Dr. Erika Ábrahám
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 531314152

Der Einsatz von Computern zum Lösen industriell relevanter Probleme ist schon lange etabliert. Eine aktuelle Entwicklung ermöglicht es, Probleme als logische Formeln erster Ordnung zu kodieren und diese automatisiert zu Lösen. SAT- und SMT-Solver (Satisfiability Modulo Theories) bieten hierzu Werkzeuge zur Überprüfung der Erfüllbarkeit dieser Formeln. SAT-Solver unterstützen Aussagenlogik, während SMT-Solver verschiedene Theorien beherrschen. Arithmetische Theorien sind im Fokus dieses Antrags und sind in diversen SMT-Solvern implementiert, darunter SMT-RAT, entwickelt von der RWTH, und veriT von der ULiège. Erfüllbarkeitsüberprüfung ist ein junges und sich schnell entwickelndes Forschungsgebiet. Es gibt sehr effiziente Solver für eine Menge von Theorien, einschließlich (quantorenfreier) linearer reeller, ganzzahliger und gemischt ganzzahlig-realer Arithmetik (LRA, LIA bzw. LIRA), d.h. für Formeln, die boolesche Kombinationen von linearen Bedingungen sind. Die Erweiterung um die Multiplikation ergibt die entsprechenden nichtlinearen arithmetischen Theorien NRA, NIA und NIRA, wobei die beiden letzteren im quantorenfreien Fall unentscheidbar sind. SMT-Techniken für lineare Arithmetik sind ausgereift, auch wenn es noch einige unerforschte, aber interessante Aspekte gibt, die wir in diesem Antrag adressieren. Im Gegensatz zum linearen Fall und trotz vielversprechender Entwicklungen sind die derzeitigen Algorithmen für NRA noch nicht zufriedenstellend. Ziel dieses Antrags ist die Verbesserung bestehender und die Entwicklung neuer Algorithmen für arithmetische Theorien. Bei der nichtlinearen Arithmetik konzentrieren wir uns aufgrund der Unentscheidbarkeit des ganzzahligen Falls hauptsächlich auf den reellen Fall. SMT-Solver werden auch in Bereichen eingesetzt, wo die Korrektheit der Antworten unerlässlich ist, z.B. zur Verifikation, in Beweis-Assistenten oder in der erklärbaren KI. Jüngste Entwicklungen erweitern SMT-Solver, sodass diese nicht nur Modelle für erfüllbare Probleme liefern, sondern auch Beweise für Unerfüllbarkeit, die extern verifiziert werden können. Allerdings wird dies für die Arithmetik noch nicht vollständig unterstützt. In diesem Projekt wollen wir das Konzept der Zertifikate und Modelle für die lineare Arithmetik konsolidieren und den Weg für Zertifikate für die nichtlineare Arithmetik ebnen. Trotz der jahrelangen Erforschung auch im Bereich der mathematischen Logik und symbolischen Rechnen sind verschiedene Aspekte der Algorithmen für Arithmetik noch nicht vollständig verstanden. Es gibt weiteren Forschungsbedarf zum Verständnis der Komplexität. So gibt es zum Beispiel nur eine vollständige Methode für LRA-Bedingungen mit polynomialem Aufwand, und es gibt immer noch keine Methode, die die einfach-exponentielle Komplexitätsgrenze für NRA implementiert. Ein weiteres Ziel ist es, ein tieferes Verständnis für die Natur der arithmetischen Probleme, ihrer Komplexität und die Struktur ihrer Lösungsmengen zu schaffen.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Belgien
• Partnerorganisation: Fonds National de la Recherche Scientifique - FNRS
• Kooperationspartner: Professor Dr. Pascal Fontaine