Extensions of the Cylindrical Algebraic Covering Method for Quantifiers

TL;DR

This paper extends the cylindrical algebraic covering method to handle arbitrary non-linear formulas with quantifiers and Boolean structure, introduces a quantifier elimination variant, and evaluates its performance against existing tools.

Contribution

The paper introduces novel extensions and optimizations to the cylindrical algebraic covering method, enabling broader applicability and improved efficiency in non-linear real arithmetic reasoning.

Findings

The extended method can decide satisfiability of complex non-linear formulas with quantifiers.

Experimental results show competitive performance with state-of-the-art SMT solvers.

The quantifier elimination variant effectively simplifies formulas for easier analysis.

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.