Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Extensions of the Cylindrical Algebraic Covering Method for Quantifiers

Jasper Nalbach, Gereon Kremer

TL;DR

This work extends the cylindrical algebraic covering (CAlC) method to decide arbitrary quantified non-linear real arithmetic formulas and perform quantifier elimination. It introduces implicants and truth-invariant cells to integrate Boolean structure directly into the algebraic reasoning, and develops a projection-based approach tailored for coverings, including a formal proof system for certificates. The authors provide an implementation within SMT-RAT, compare against state-of-the-art SMT solvers and QE tools, and show competitive performance on NRA benchmarks, with QE results promising particularly for quantified problems. The study highlights strengths in handling quantifier structure and nondiscrete search, while identifying areas for improvement such as Boolean reasoning efficiency, dynamic variable orderings, and output-size reduction for QE. Overall, the framework demonstrates the viability of CAD-inspired covering methods as a practical alternative to traditional CDCL(T) and QE approaches for complex NRA problems, with clear paths for future enhancements and applications.

Abstract

The cylindrical algebraic covering method was originally proposed to decide the satisfiability of a set of non-linear real arithmetic constraints. We reformulate and extend the cylindrical algebraic covering method to allow for checking the truth of arbitrary non-linear arithmetic formulas, adding support for both quantifiers and Boolean structure. Furthermore, we also propose a variant to perform quantifier elimination on such formulas. After introducing the algorithm, we elaborate on various extensions, optimizations and heuristics. Finally, we present an experimental evaluation of our implementation and provide a comparison with state-of-the-art SMT solvers and quantifier elimination tools.

Extensions of the Cylindrical Algebraic Covering Method for Quantifiers

TL;DR

This work extends the cylindrical algebraic covering (CAlC) method to decide arbitrary quantified non-linear real arithmetic formulas and perform quantifier elimination. It introduces implicants and truth-invariant cells to integrate Boolean structure directly into the algebraic reasoning, and develops a projection-based approach tailored for coverings, including a formal proof system for certificates. The authors provide an implementation within SMT-RAT, compare against state-of-the-art SMT solvers and QE tools, and show competitive performance on NRA benchmarks, with QE results promising particularly for quantified problems. The study highlights strengths in handling quantifier structure and nondiscrete search, while identifying areas for improvement such as Boolean reasoning efficiency, dynamic variable orderings, and output-size reduction for QE. Overall, the framework demonstrates the viability of CAD-inspired covering methods as a practical alternative to traditional CDCL(T) and QE approaches for complex NRA problems, with clear paths for future enhancements and applications.

Abstract

The cylindrical algebraic covering method was originally proposed to decide the satisfiability of a set of non-linear real arithmetic constraints. We reformulate and extend the cylindrical algebraic covering method to allow for checking the truth of arbitrary non-linear arithmetic formulas, adding support for both quantifiers and Boolean structure. Furthermore, we also propose a variant to perform quantifier elimination on such formulas. After introducing the algorithm, we elaborate on various extensions, optimizations and heuristics. Finally, we present an experimental evaluation of our implementation and provide a comparison with state-of-the-art SMT solvers and quantifier elimination tools.

Paper Structure

This paper contains 51 sections, 1 theorem, 10 equations, 7 figures, 2 tables, 19 algorithms.

Table of Contents

  1. Introduction
  2. Contribution
  3. Related Work
  4. Quantifier-free Formulas
  5. Quantified Formulas
  6. Preliminaries
  7. Cylindrical Algebraic Decomposition
  8. Cylindrical Algebraic Covering
  9. Implicit Cells.
  10. Implicants.
  11. Quantified Problems
  12. Existential Quantification
  13. Universal Quantification
  14. Truth-Invariant Cells
  15. Details of the projection operator
  16. ...and 36 more sections

Key Result

Lemma 8.4

Let $i \in \mathbb{N}_{>0}$, $R \subseteq \mathbb{R}^i$, $s \in \mathbb{R}^{i-1}$, $\texttt{C} = (\textnormal{I}_1, \ldots, \textnormal{I}_k)$ be a sequence of symbolic intervals of level $i$, and $\preceq$ be an indexed root ordering of level $i$. Assume that $\texttt{C}$ fulfils the following cond

Figures (7)

  • Figure 1: Illustration of the example.
  • Figure 2: Number of implicants that were used for the covering.
  • Figure 3: Performance profiles of SMT solvers.
  • Figure 4: Performance profile of quantifier elimination tools.
  • Figure 5: Quality of the solution formula: We compare the number of atoms in the solution formula (indicated by the coordinates). Every point that is not on one of the gray lines represents an instance solved by both solvers. The $\bot$ line indicates that the corresponding solver did time out on the instance.
  • ...and 2 more figures

Theorems & Definitions (22)

  • Definition 3.1: Cylindrical Algebraic Decomposition
  • Definition 3.2: Implicit Cell
  • Example
  • Definition 3.3: Implicant
  • Example
  • Definition 5.1: Indexed Root Expression
  • Definition 5.2: Indexed Root Formula
  • Example
  • Example
  • Example
  • ...and 12 more