Automated Reasoning in Linear Arithmetic

Abstract

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.

Automated Reasoning involving quantified formulas over linear arithmetic is a fundamental problem in automated verification of hardware and software, program synthesis, neural network verification and many more other areas. Nevertheless it remains highly challenging due to the interaction of quantifiers and arithmetic theories. This thesis provides a comprehensive and detailed study with a thorough literature search and comparison between three families of approaches: superposition-based calculi, instantiation-based frameworks, and algebraic quantifier elimination methods. The results show that superposition-based lifting is particularly effective on problems involving arithmetic with uninterpreted functions, instantiation methods perform strongly on few quantifier alternations, and approximative quantifier elimination achieves good scalability at the cost of completeness. These findings indicate that no single approach is outstanding across all problem classes, and suggests implying that hybrid architectures offer the most promising path forward.