The cylindrical algebraic coverings method was originally proposed to decide the satisfiability of a set of nonlinear real arithmetic constraints. We reformulate and extend the cylindrical algebraic coverings method to allow for checking the validity of arbitrary nonlinear arithmetic formulas, adding support for both quantifiers and arbitrary Boolean structure. Furthermore, we also propose a variant to perform quantifier elimination on such formulas. Nonlinear real arithmetic is the first-order theory whose atoms are polynomial constraints over real variables. We consider three fundamental problems that deal with formulas from this theory: satisifability , validity and quantifier elimination . Satisfiability is concerned with the existential fragment (or equivalently the quantifier-free fragment) of this theory: given a purely existentially quantified formula (or a quantifier-free formula) it decides whether an assignment to the formula's variables exists such that the formula evaluates to True. In contrast to this, validity considers fully quantified formulas and checks whether they are equivalent to True or False. Finally, quantifier elimination deals with formulas that have both free variables (parameters) and quantified variables, and constructs equivalent quantifier-free formulas over the parameters. The cylindrical algebraic decomposition [1] method is the only complete procedure for solving all these questions for nonlinear real arithmetic that is used in practice, despite its doubly exponential worst-case complexity that severely limits the scalability of the method. For the satisfiability problem of conjunctions of constraints, motivated by the application in satisfiability modulo theories solving, the cylindrical algebraic coverings method [2] has been developed based on cylindrical algebraic decomposition. Although it retains the doubly exponential complexity, its performance is significantly better in practice [2, 3] while its implementation requires only a simple bookkeeping data structure. Furthermore, it closer resembles human reasoning and is more accessible to proof production [4, 5]. Contribution. We propose a novel reformulation and extension of the cylindrical algebraic coverings method that goes beyond the satisfiability problem of conjunctions and also allows to solve arbitrary quantified formulas as well as quantifier elimination queries. We first consider validity where all variables are explicitly quantified, either existentially or universally, in Section 3, and then expand to the quantifier elimination problem in Section 4.
We assume every formula to be a first-order formula over nonlinear real arithmetic with polynomial constraints defined in variables 1, . . . , ∈ R. Furthermore, we expect to be transformed to prenex normal form, i.e., consisting of a prefix of quantifiers and a quantifier-free formula called the matrix : := +1+1 · · · . (1, . . . , ) If ̸= 0, has free variables that are not explicitly quantified. These can be considered to be implicitly quantified existentially, much like we do for satisfiability modulo theories queries in general. We assume that in Section 3 and actually solve ∃1 · · · ∃ +1+1 · · · . (1 . . . ). Alternatively, these free variables can be understood as parameters to make the input a quantifier elimination problem, as we do in Section 4.
We use standard notation for arithmetic and assume an ordering on the variables 1 ≺ · · · ≺ .
The highest variable occurring in a polynomial or constraint is called their main variable. For further
details, we refer to [
We denote the constraints that occur in a formula by constraints( ). To select only those with main variable , we write constraints( ).
Cylindrical Algebraic Coverings. We briefly present the idea behind the cylindrical algebraic
coverings method for checking the existential fragment of nonlinear real arithmetic and refer to [
The algorithm starts by constructing unsatisfiable intervals for 1 based on univariate constraints
and then tries so select a value 1 for the variable 1 outside of these intervals. If such a value exists,
the method is called recursively with the partial sample point (1). After substituting 1 = 1, the
constraints with main variable 2 become univariate and thus suitable for identifying unsatisfiable
intervals for 2. This process is continued recursively until either all constraints are satisfied (and
we return SAT) or for some no suitable value exists. In the latter case, the set of unsatisfiable
intervals covers the whole real line and forms a covering. This covering is generalized by projecting it to
dimension − 1. The idea is to use projection tools borrowed from cylindrical algebraic decomposition
with some improvements: as we only need to characterize this covering and not a decomposition, only a
subset of the full projection is needed. Using the current sample point, an interval for the variable − 1
with respect to the projection result can be computed which is added to the set of unsatisfiable intervals
for − 1, possibly taking part in an unsatisfiable covering for − 1. Unless we find a full satisfying
sample point we eventually obtain an unsatisfiable covering for the first variable 1 and return UNSAT.
Algebraic Intervals. We generalize intervals (over a partial sample point) by attaching algebraic
information in the form of sets of polynomials whose order-invariance characterizes satisfiability-invariant
regions of a formula in multidimensional space. We call them algebraic intervals and represent them as a
tuple = (ℓ, , , , , ⊥). (ℓ, ) is the (numeric) interval over an ( − 1)-dimensional sample
point, and are sets of the polynomials with main variable which vanish at (1, . . . , − 1, ℓ)
and (1, . . . , − 1, ), respectively, is a set of polynomials with main variable which should be
order-invariant in the constructed interval and ⊥ is a set of lower-level polynomials which need to be
order-invariant in the underlying cell as well. See [
Example 1. Consider the polynomials = {2 + 1, 2 − 1, 11 + 22 − 2, 1 − 1} and the sample point = (0, 0). Then the algebraic interval (− 1, 1, {2 + 1}, {2 − 1}, {2 + 1, 2 − 1, 11 + 22 − 2}, {1 − 1}) represents the interval (− 1, 1) for 2 around 2 = 0 over the partial sample point 1 = 0. The lower and upper bounds are defined by 2 + 1 and 2 − 1, respectively. The polynomials in are order-invariant in the represented interval, the polynomials of defining zeros of 2 are {2 + 1, 2 − 1, 11 + 22 − 2}, while 1 − 1 is of lower level and thus stored separately.
Implicants. An implicant of a formula is usually understood to be a “simpler” formula that implies , or formally ⇒ ∧ constraints( ) ⊆ constraints( ). We adapt this concept as follows. Let ∈ R be a (partial) sample point. If [] = True, then is an implicant of with respect to if [] = True ∧ (
⇒ ) ∧ constraints( ) ⊆ constraints( ).
Otherwise, if [] = False, then is an implicant of with respect to if [] = True ∧ (
⇒ ¬ ) ∧ constraints( ) ⊆ constraints( ).
We call a prime implicant of if constraints( ) is minimal among all implicants of . Example 2. Let = 2 > 0 ∧ ( < 2 ∨ > 4). Note that (1) = True, (3) = False and (0) = False. 2 > 0 ∧ < 2 is a prime implicant of w.r.t. 1. ¬( < 2 ∨ > 4) is a prime implicant of w.r.t. 3. Both ¬(2 > 0) and ¬(2 > 0 ∧ > 4) are implicants of w.r.t. 0, but only the first is a prime implicant.
Algorithm 1: user_call()
Data: Global prefix 11 · · · and matrix .
Output : Either SAT or UNSAT 1 (, ) := recurse(()) 2 return // Algorithm 2 Algorithm 2: recurse()
Data: Global prefix 11 · · · and matrix .
Input : Sample point = (1, . . . , − 1) ∈ R− 1 such that [] ̸= False.
Output : (SAT, ) or (UNSAT, ) where × can or can not be extended to a model for any ∈ . In both cases, the algebraic information attached to describes how can be generalized. 1 if = ∃ then return exists() // Algorithm 3 2 else return forall() // Algorithm 4
We first describe how the cylindrical algebraic coverings method can be adapted for problems where all
variables are quantified. Our presentation stays very close to [
One of the most notable changes is the interface of the main method. In [
This introduces a technical problem for the first dimension ( = 1), as we refer to − 1 in the arguments to interval_from_characterization which does not exist. This is to be expected, as the returned interval would live in the “zero-th dimension”. To simplify the presentation, we assume that a special placeholder value is returned instead of an actual interval. Algorithm 2 only returns SAT or UNSAT and no longer exposes a model or an unsatisfiable covering. In an actual implementation, this information is easily accessible.
Algorithm 1 is the interface to the recursive Algorithm 2, calling it with an empty sample point and extracting the main return value. Algorithm 2 checks the current quantifier and calls out to Algorithm 3 or Algorithm 4 accordingly.
Algorithm 3 is mostly equivalent to [2, Algorithm 2] and incorporates the following changes: instead of returning a model, we obtain a feasible interval around the model and return the algebraic interval that can directly be used for a satisfiable covering in dimension − 1; instead of computing an algebraic interval from the covering obtained from the (UNSAT) recursive call, we use the result as it is and return the appropriate algebraic interval instead of a covering.
Algorithm 4 is analogous to Algorithm 3 that is used if the current variable is universally quantified. The two procedures are almost identical: while Algorithm 3 collects unsatisfiable intervals and returns early when it finds a satisfiable interval, Algorithm 4 collects satisfiable intervals and returns early when it finds an unsatisfiable interval. Note that we call out to characterize_covering for both satisfiable and unsatisfiable coverings in the very same way.
Algorithm 5 computes an interval around the given sample point that is satisfiability-invariant with
respect to . It first obtains the set of relevant polynomials by calling implicant_polynomials
and then uses [2, Algorithm 5] to construct the interval that is being returned. The helper function
implicant_polynomials is expected to return the polynomials of an implicant of with respect
to × . This might include polynomials with main variable or lower, efectively providing for a
proper characterization of the interval not only in variable , but also for lower variables. Further, if
[ × ] = False and is a simple conjunction, it is easy to obtain a prime implicant as the negation
of a single conflicting constraint in constraints( ). Calling it in a loop as done in Algorithm 3 is
thus a direct generalization of get_unsat_intervals from [
Algorithm 6 and Algorithm 7 replace [2, Algorithm 4] and compute the characterizations for a single interval and a covering, respectively. They contain no changes, except generalizing their input and output descriptions to any coverings, either satisfiable or unsatisfiable.
Note that we changed how we normalize the polynomial sets after projection. While [
Depending on the implementation of the required_coefficients() subroutine and which semantics for the root isolation is used, the projection operator would usually be either McCallum’s or Lazard’s projection operator; this choice is already discussed in [2, Section 4.4.6] and possibly changes the properties of the algebraic intervals which we define based on order-invariance.
As wide parts of the algorithm are taken from the cylindrical algebraic covering method, we again refer
to [
We sample 2 = 3.5 (Line 3) and find a satisfying sample. Now, we generalize to the feasible interval around (2, 3.5) as depicted in Figure 1b, which is bounded from below by 1 and from above by 3 (Line 7). Its projection is the satisfiable interval (1, 3) for 1 that we return (Lines 11 and 12).
We store the received satisfying interval (Line 11). As there exist samples outside the set of satisfying intervals (Line 2), we pick the next value 3.2 for 1 (Line 3): exists( = (3.2)) We sample 2 = 2.75 and find a satisfying sample. We generalize to the feasible interval bounded by 1 and 3. Note that in the projection of the feasible interval, we take all constraints into account (as all constraints are part of the implicant), even if they do not have a real root at = 3.2 – here, the discriminant of 2 is added to the projection ensuring that no root of 2 crosses the feasible interval. The resulting projection is the satisfiable interval (3, 3.5) for . (The underlined value is an approximation).
Similarly, the reveived interval is stored and we proceed with the sample 4 for 1: exists( = (4)) We sample 2 = 4 (Line 3) to obtain the unsatisfiable interval (3, ∞) (Line 5) which we store in the set of unsatisfying intervals (Line 15). As this set does not cover the whole real line yet (Line 2), we sample 2 = 2 (Line 3) to obtain the unsatisfiable interval (−∞ , 3.5) (Line 5), which is again stored (Line 15). The intervals cover the real line for 2 (Line 2), as depicted dashed in Figure 1b. We return the unsatisfiable interval (3.5, 4.5) for 1 which is the projection of the generalization of the covering (Lines 16 and 17).
Algorithm 8: user_call_qe()
Data: Global prefix +1+1 · · · and matrix .
Output : A disjunction of satisfiable regions of +1+1 · · · . . 1 if = 0 then return recurse(()) 2 else return parameter(())
As a recursive call returned an unsatisfiable interval, the algorithm terminates here by returning UNSAT (Line 15).
For extending the method for quantifier elimination, we could follow a NuCAD [
We propose an alternative approach in Algorithms 8 and 9 which builds upon the cylindrical algebraic coverings method. The idea is to consider the parameters first, and treating them similar to existentially quantified variables with a few diferences: instead of returning as soon as we find a satisfiable interval, we collect both satisfiable and unsatisfiable intervals until the whole real line is covered by either satisfiable or unsatisfiable intervals and return a characterization of this covering. This ensures that all satisfiable regions of the parameter space are enumerated. Simultaneously, a symbolic description of the satisfiable regions in the parameters is constructed as a formula and returned.
For the latter, we employ the concept of indexed root expressions [
We have proposed an extension of the cylindrical algebraic coverings approach that is suitable to solve
the validity problem for quantified formulas as well as quantifier elimination queries for partially
quantified formulas. This significantly extends the applicability of the cylindrical algebraic coverings
method to problems that were reserved to regular cylindrical algebraic decomposition so far. At the
same time it is backwards compatible in the sense that it can produce the same results as the original
method from [
We look forward to see how implementations of this approach fare in practice compared to the techniques for these problems that are in use today. Given the pleasant practical experience with cylindrical algebraic coverings in solving regular satisfiability modulo theories queries – one of the reasons cvc5 won on the QF_NRA logic in the SMT-COMP 2021 over alternative approaches – we are optimistic it can bring significant improvements, all while still allowing for a fairly easy implementation.