SMT-ART (Satisfiability Modulo Theories Arithmetic Reasoning Techniques) is a collaborative project involving Prof. Dr. Dr. h.c. Erika Ábrahám from RWTH Aachen University and Prof. Dr. Pascal Fontaine from the University of Liège (Belgium). It is funded by the German Research Foundation (DFG), under project number 531314152.
About the Project
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.
Team
RWTH Aachen University, Germany
Erika Ábrahám
Valentin Promies
University of Liège, Belgium
Pascal Fontaine
Alexis Bertrand
Publications
- Valentin Promies, Erika Ábrahám: A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic. FM (1) 2024: 131-148
- Valentin Promies, Jasper Nalbach, Erika Ábrahám: Under-Approximation of a Single Algebraic Cell (Extended Abstract). PAAR+SC²@IJCAR 2024: 132-136
- Jasper Nalbach, Erika Ábrahám: Merging Adjacent Cells During Single Cell Construction. CASC 2024: 252-272