SMT Arithmetic Reasoning Techniques

• Applicant: Professorin Dr. Erika Ábrahám
• Subject Area: Theoretical Computer Science
• Term: since 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 531314152

The use of advanced methods to solve practical and industrially relevant problems by computers has a long history. A recent development is to encode practical problems as first-order logic formulas and use automated methods for their solution. Satisfiability checking techniques implemented in SAT and SMT (satisfiability modulo theories) solvers offer tools for this purpose. SAT solvers support propositional logic, whereas SMT solvers cover different theories. Arithmetic theories, which are in the focus of this proposal, are embedded in many SMT solvers, among them SMT-RAT developed in Aachen, and veriT in Liège. Satisfiability checking is a relatively young research area, but with impressively fast development. There are extremely powerful solvers for a number of theories, including (quantifier-free) linear real, integer and mixed integer-real arithmetic (LRA, LIA resp. LIRA), i.e. on formulas that are Boolean combinations of linear constraints. Adding multiplication leads to the respective non-linear arithmetic theories NRA, NIA and NIRA, the latter two being undecidable even in the quantifier-free case. SMT techniques for linear arithmetic are quite mature, even though there remain some unexplored but promising aspects, that we address in this proposal. In contrast to the linear case and despite exciting recent developments, current SMT solutions for the decidable theory of non-linear real arithmetic (NRA) are still not satisfactory. The first objective of this proposal is to increase efficiency by improving existing decision procedures and developing new satisfiability checking algorithms for arithmetic theories. For non-linear arithmetic, we mainly focus on reals due to the undecidability of the integer case. SMT solvers are frequently used, e.g., for verification, in proof assistants or in explainable AI, where the correctness of the answers is critical. To provide evidence, recent developments make SMT solvers deliver not only models for satisfiable problems but also certificates in the form of unsatisfiability proofs that can be checked externally. However, arithmetic, especially the non-linear case, is not yet comprehensively covered by this development. In this project we furthermore aim to consolidate the concept of certificates and models for linear arithmetic and pave the way for certificates for non-linear arithmetic. Rooted in mathematical logic and symbolic computation, decision procedures for arithmetic theories have a long history. Despite this fact, different aspects are still not fully understood. There is further effort needed to better understand the sources of complexity. For example, only one complete method is available for checking LRA constraint sets with polynomial effort, and there is still no method that implements the singly-exponential complexity bound for NRA. A further objective is to provide a deeper understanding of the nature of arithmetic problems, their complexity and the structure of their solution sets.

• DFG Programme: Research Grants
• International Connection: Belgium
• Partner Organisation: Fonds National de la Recherche Scientifique - FNRS
• Cooperation Partner: Professor Dr. Pascal Fontaine