Automated Reasoning in Linear Arithmetic

Automated Reasoning über quantifizierte Formeln mit linearer Arithmetik stellt ein fundamentales Problem in der automatischen Verifikation von Hard- und Software, der Programmsynthese, der Verifikation neuronaler Netze und vielen weiteren Anwendungsbereichen dar. Dennoch bleibt es aufgrund der Quantoren und arithmetischen Theorien eine große Herausforderung. Diese Arbeit bietet einen umfassenden Überblick sowie eine detaillierte Literaturanalyse und vergleicht drei Familien von Ansätzen: superpositionsbasierte Kalküle, instantiierungsbasierte Frameworks und algebraische Methoden der Quantoreneliminierung. Die Ergebnisse zeigen, dass superpositionsbasierte Verfahren insbesondere bei Problemen, die Arithmetik mit uninterpretierten Funktionen kombinieren, sehr effektiv sind, während Instantiierungsmethoden bei wenigen Quantorenalternationen besonders stark abschneiden. Approximative Quantoreneliminierung hingegen erreicht eine gute Skalierbarkeit, allerdings auf Kosten der Vollständigkeit. Diese Erkenntnisse verdeutlichen, dass ein einzelner Ansatz nicht alle Problemklassen dominiert, weshalb hybride Architekturen den vielversprechendsten Weg für zukünftige Entwicklungen darstellen.