tr-announce

Download

tr-announce@lists.rwth-aachen.de

June 2020

1 participants
1 discussions

2020-04: Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems
by Hensel, Jera 18 Jun '20

18 Jun '20

The following technical report is available from http://aib.informatik.rwth-aachen.de: Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems Gereon Kremer AIB 2020-04 Satisfiability modulo theories solving is a technology to solve logically encoded problems for many applications like verification, testing, or planning. Among the many theories that are considered within this logical framework, nonlinear real arithmetic stands out as particularly challenging, yet decidable and sufficiently well understood from a mathematical perspective. The most prominent approach that can decide upon nonlinear real questions in a complete way is the cylindrical algebraic decomposition method. We explore the usage of the cylindrical algebraic decomposition method for satisfiability modulo theories solving, both theoretically and experimentally. This method is commonly understood as an almost atomic procedure that gathers information about an algebraic problem and then allows to answer all kinds of questions about this algebraic problem afterward. We essentially break up this method into smaller components that we can then process in varying order to derive the particular piece of information - whether the problem is satisfiable or unsatisfiable - allowing to avoid some amount of computations. As this method often exhibits doubly exponential running time, these savings can be very significant in practice. We furthermore embed this method in the regular satisfiability modulo theories framework where the cylindrical algebraic method is faced with a sequence of problems that are "related" in the sense that they usually share large parts of their problem statements. We devise different approaches to retain information from a previous run so that it can be reused when the problem is only "extended" as well as purging now obsolete information if the problem is "reduced". These variants change in how much information can be reused, the granularity of the information that is removed, and how much bookkeeping needs to be done. This integration is then enhanced with techniques that are more or less well-known in the computer algebra community, for example, different projection operators, equational constraints, or employing the so-called resultant rule. Furthermore, we present novel features necessary for an efficient embedding in the satisfiability modulo theories framework like infeasible subset computations and early termination as well as extensions to integer problems and optimization problems. We then turn to an alternative approach to satisfiability modulo theories solving that is commonly called model-constructing satisfiability calculus. The core idea of this framework is to integrate the theory reasoning, in particular the construction of a theory model, tightly with the Boolean reasoning. The most popular theory reasoning engine is again based on the cylindrical algebraic decomposition method, though we focus on the overall framework here. We start with our own variant of the model-constructing satisfiability calculus and discuss some general insights and changes compared to current implementations. We then proceed to present a whole series of reasoning engines for arithmetic problems and show how a proper (though still naive) combination of those serves to significantly improve a practical solver. We also show how the tight integration into the Boolean reasoning allows for novel strategies for notoriously hard problems like the theory variable ordering or expedient cooperation between the Boolean and the theory reasoning. Finally, we consider the theoretical relation of the model-constructing satisfiability calculus to other proof systems, in particular, the aforementioned regular satisfiability modulo theories solving. Under certain assumptions - that turn out to be instructive in and of themselves - we show that they are equivalent with respect to their proof complexity and even establish what we call "algorithmic equivalency" afterward.

1 0