The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponential complexity, diferent exploration-guided adaptations try to avoid some of the computations. The first such adaptation named NLSAT was followed by Non-uniform CAD (NuCAD) and the Cylindrical Algebraic Covering (CAlC). Both NLSAT and CAlC have been developed and implemented in SMT solvers for satisfiability checking, and CAlC was recently also adapted for quantifier elimination. However, NuCAD was designed for quantifier elimination only, and no complete implementation existed before this work. In this paper, we present a novel variant of NuCAD for both real quantifier elimination and SMT solving, provide an implementation, and evaluate the method by experimentally comparing it to CAlC.
Real algebra is a highly expressive logic, whose formulas are Boolean combinations of polynomial constraints over potentially quantified real-valued variables. In this paper, we consider three related problems for real algebra: (1) deciding the satisfiability of quantifier-free formulas (i.e., solving the existential fragment), (2) deciding the truth of sentences, and (3) quantifier elimination.
The first practically feasible complete algorithm for solving all these problems was the cylindrical
algebraic decomposition (CAD) method [
On another research line, exploration-guided proof generation turned out to be extremely efective
for checking the satisfiability of propositional logic formulas via SAT solvers. Extending this idea to
Satisfiability Modulo Theories (SMT) solving, the NLSAT [17] algorithm was the first exploration-guided
CAD adaptation for satisfiability checking. Whereas CAD analyses the whole state space regarding
the whole input formula, NLSAT first explores the state space through smart guesses of sample values
for the (real and Boolean) variables. If a partial sample turns out not to be further extensible to a
satisfying assignment, then some partial CAD computations are applied to generalize this sample to
a set of samples, which are not extensible to satisfying solutions for the same reason (i.e., the same
constraints in the input formula). These generalizations rely on the single cell paradigm introduced
in [
NLSAT inspired the development of another CAD adaptation named the Cylindrical Algebraic
Covering (CAlC) [
While having a focus on satisfiability checking, some SMT solvers can also solve quantified formulas
[
Also the non-uniform cylindrical algebraic decomposition (NuCAD) [
Our paper continues the above work on the NuCAD, contributing: • a complete variant of the NuCAD algorithm, • a modification which considers the input’s quantifier structure directly during the computation of the decomposition, • its implementation along with a post-processing of the NuCAD, and • experimental evaluation in particular against the CAlC algorithm, on deciding the existential fragment, deciding sentences, and quantifier elimination.
Though our experiments indicate that CAlC solves satisfiability checking problems faster than NuCAD, NuCAD seems to be competitive on quantifier elimination. However, the available quantified benchmark sets lack suficient diversity to make definitive conclusions on algorithm superiority.
Outline: We introduce the fundamentals of CAD and CAlC in Section 2, and introduce a complete version of the NuCAD algorithm in Section 3. In Section 4, we extend the algorithm for quantifier alternations. Finally, we present the experimental results in Section 5 and conclude the paper in Section 6.
Let N, N>0, Q, and R denote the natural (incl. 0), positive integer, rational, and real numbers respectively. For , ∈ N, we set [..] = {, . . . , } and [] = [1..]. For ∈ N, ∈ R and ∈ [] we write for the th component of . For tuples introduced as = (, , ), we use ., . and . to access their entries.
From now ∈ N>0, ∈ [0..], ∈ [], ∈ R , * ∈ R, ⊆ R , and ⊆ R.
We define (, * ) = (1, . . . , , * ), × = {} × , [] = (1, . . . , min{,}), and [] = {[]| ∈ }. Let , : → R be continuous functions, then × (, ) = {(, ′) | ∈ ∧ ′ ∈ R ∧ () < ′ < ()}, × [, ] = {(, ′) | ∈ ∧ ′ ∈ R ∧ () ≤ ′ ≤ ()} , analogously × (, ] and × [, ).
all polynomials in 1, . . . , with rational coeficients. Let ∈ Q[1, . . . , ]. The main variable of is the highest ordered variable occurring in it, and its level level() is the index of the main variable. The degree of in is denoted by deg (). For a univariate ∈ Q[ ], its real roots (in ) build the set realRoots().
′ ⊆ R if (′) has the same sign for all ′ ∈ ′. The polynomial is nullified over if () ≡ 0 , where ≡ denotes semantic equivalence. We further define [] to be () for level() ≤ , and otherwise.
A (polynomial) constraint has the form ∼ 0 with ∼∈ {=, ≤, ≥, ̸=, <, >} . Notations for polynomials are transferred to constraints where meaningful, for example ( ∼ 0)() is () ∼ 0 , and ( ∼ 0)[] is [] ∼ 0.
Real-algebraic formulae are potentially quantified Boolean combinations of polynomial constraints. Again, we inherit notations from constraints, e.g. we get () ([] ) from through replacing each constraint by () ([]). A formula is truth-invariant on ′ ⊆ R if ( ′) = ( ′′) for all ′, ′′ ∈ ′. A formula is in prenex normal form if it is of the form +1+1 . . . . ̄ for some ∈ N, consisting of a prefix of quantifiers and a quantifier-free formula ̄ called the matrix; the variables 1, . . . , are called free in (also called parameters). The task of quantifier elimination is, given a formula that may contain quantifiers, to compute a quantifier-free formula such that ≡ .
We will further make use of the following concept:
Definition 2.1 (Implicant [
The quantifier-free formula is an implicant of with respect to if all constraints ∼ 0 in have
level() ≤ and are contained in , [] ≡ true, and either ⇒ or ⇒ ¬. □
Example 2.1. As a univariate example with = 1, for = 21 > 0 ∧ (1 < 2 ∨ 1 > 4) we have
[
For ′ = (1 < 0 ∨ 2 ≤ 4) ∧ ( 1 > 2 ∨ 2 > 4) we observe ′[
For a given formula, the cylindrical algebraic decomposition (CAD) [
Definition 2.2 (Cylindrical Algebraic Decomposition [
• An (-dimensional) cell is a non-empty connected subset of R. • A decomposition of R is a finite set of -dimensional cells such that either = ′ or ∩ ′ = ∅ for all , ′ ∈ , and ∪∈ = R. • A set ′ ⊆ R is semi-algebraic if it is the solution set of a quantifier-free formula. • A decomposition of R is cylindrical if either = 1, or > 1 and −1 = {[−1] | ∈ } is a cylindrical decomposition of R−1 . • A cylindrical algebraic decomposition (CAD) of R is a cylindrical decomposition of R whose cells ∈ are semi-algebraic. • Let ⊆ Q[ 1, . . . , ] and be a CAD of R. We call sign-invariant for if each ∈ is sign-invariant on each cell ∈ . • Let ⊆ R be a cell and , : → R continuous functions with () < () for all ∈ . We call × R the cylinder over , × [, ] a section over , and × (, ) a sector over . □ Unfortunately, the number of cells in a CAD that is sign-invariant for some set of polynomials may be doubly exponential in the number of their variables. This heavy complexity is partly rooted in the projection phase of the CAD method, in which polynomials of level are projected to generate polynomials of level − 1 , iteratively for = , . . . , 2. The efort for these projections depends on the degree and on the number of the polynomials, which might grow double-exponentially during this process. Thus, the costs of the projection plays a substantial role for the practical feasibility of the algorithm.
p4 (−0.5, 3.5) (−0.5, 2) x1
(2.5) (b) Truth-invariant CAlC from Example 2.3, along with a sample point for each cell.
Example 2.2. Consider the formula ( 1, 2) = 1 ≤ 0 ∧ 2 > 0 ∧ 3 ≥ 0 ∧ 4 ≤ 0 ∧ 5 ≤ 0 using the following polynomials: built 1 = −0.006( 1 − 2)( 1 + 2)(1 − 3)( 1 + 3)(1 − 4)( 1 + 4) − 2 2 = (1 + 2.5)2 + (2 − 1.5) 2 − 0.25 3 = (1 − 2.5) 2 + (2 − 1.5) 2 − 0.25 4 = 2 − 2.5 5 = 1 The CAD method computes the projection polynomials 6 = disc2 (2), 7 = disc2 (3) and 8 = res2 (1, 4), where disc and res are operators which we do not detail here. Figure 1a illustrates the variety of these polynomials, as well as the CAD of R and R2.
Further, each cell is coloured according to the truth value (green for true and red for false) of on that cell, which is determined by substituting a sample point (not depicted in the figure) from each cell into .
If we aim to check whether ∃1. ∃2. holds, we only need to find one cell where evaluates to true. To check whether ∃1. ∀2. holds, we would iterate through the one-dimensional CAD (e.g. finitely many values for 1) and then check whether the respective cylinder is covered by cells where is true. ⌟
A key observation is that the computed CAD is often finer than necessary for quantifier elimination.
Some projection polynomials may be omitted, leading to a coarser CAD, because the real roots of the
projection polynomials define the boundaries of the CAD cells. Now the idea of exploration-guided
algorithms comes into play: we can iteratively guess sample points and generalize them to
truthinvariant cells, and compute a coarser decomposition (or covering) of the state space by combining
the individual generalizations. Such algorithms are NuCAD with a weaker notion of cylindricity, CAlC
[
• A covering of R is a finite set of -dimensional cells with ∪∈ = R. • A covering of R is minimal if there does not exist a covering ′ ⊆ of R. • A covering of R is cylindrical if either = 1, or > 1 and −1 minimal cylindrical covering of R−1 . = {[−1] | ∈ } is a • A cylindrical algebraic covering (CAlC) of R is a cylindrical covering of R whose cells ∈ are semi-algebraic. • Let be a formula with free variables 1, . . . , . A CAlC of R is truth-invariant for if is truth-invariant on each cell ∈ . □ Example 2.3. A truth-invariant CAlC for the formula from Example 2.2 is depicted in Figure 1b. We emphasize that due to the cylindrical arrangement, we can reason about the formula and its quantifiers similarly as with a CAD. ⌟
A key concept for exploration-guided algorithms is the single cell construction [
Definition 2.5 (Indexed Root Expression, Symbolic Interval). An indexed root expression (of level ) is a partial function root, : R−1 ˓ such that for each ∈ R−1 , root, (→) iRstfhoers-otmherea,lro∈otNo>ft0haenudniva∈riQat[ep1o,l.y.n.o,mia]lwi(th)le∈veQl([)] =if it, exists, and it is undefined (undef) otherwise.
A symbolic interval I of level has the form I = (, ), I = [, ], I = [, ), or I = (, ] where is either an indexed root expression of level or −∞ , and is either an indexed root expression of level or ∞. The polynomials I. and I. are the defining polynomials of I (if they exist). □
We use the cross product notation also for symbolic intervals.
Algorithm 1 computes such a single cell using the levelwise algorithm from [
We consider the first coordinate 1 = 0.125 of , evaluate the polynomials at this value for 1, and isolate the real roots of the resulting univariate polynomials to find 1 = root22,1, 2 = root32,1, 3 = root12,1, and 4 = root22,2. We order these, along with the second coordinate of , as in Figure 2a. The symbolic Algorithm 1: construct_cell( ,).
Input : = ′ ⊆ Q[ 1, . . . , ], ∈ R.
Output : Symbolic intervals I1, . . . , I of levels 1, . . . , respectively such that I1 × . . . × I 1 foreach = , . . . , 1 do 2 I := choose_interval( ′,[]) 3 ′ := compute_cell_projection( ′,[],I) 4 return I1, . . . , I ⊆ (, ). 2 x 2 x 2 x I2 p4 p5 p5 p4 ξ1′ ξ2′ ξ3′ = ξ′ 4 x1 x1 x1 (a) The sample point de- (b) The real roots witness (c) Zeros of projection poly- (d) On the level below, we picted on the one- and root functions of the nomials define the sym- iterate the process. two-dimensional coor- polynomials. bolic interval bound.
dinate systems. interval containing is denoted I2 = ( 1, 2) in Figure 2b. Thus local to 1, the cell we want is bounded from below by 2 and from above by 3.
As we generalize from we must ensure that the domains of 1 and 2 remain well-defined, no root function crosses the symbolic interval I2, and no additional roots pop up within I2. To achieve this, we compute the projection polynomials 4 and 5 (details omitted here). Figure 2c shows how the zeros of the projection map onto the geometric features. Analogously to 2, we isolate the real roots 1′ = root41,1, 2′ = root51,1, 3′ = root41,2, 4′ = root51,2 in 1. We determine the interval I1 = ( 2′, 3′) around 1 for 1 and thus generate the cell in Figure 2d. ⌟
The NuCAD algorithm builds — similarly to NLSAT and CAlC — on top of the single cell construction. It computes a decomposition of R, whose cells, however, are not globally cylindrically arranged. It can I1 x1 Algorithm 3: compute_cell_projection( ,,I).
Input : ⊆ Q[ 1, . . . , ], ∈ R, symbolic interval I of level for an ∈ [].
Output : ′ ⊆ Q[ 1, . . . , −1 ] such that ( ′, [−1] ) × I ⊆ (, ).
2 x be seen as a cylindrical decomposition, where some cells are further refined into a local cylindrical decomposition.
Definition 3.1 (Non-uniform CAD [
is a finite sequence of pairs (I1, T1), . . . , (I, T) with ∈ N>0 and for all ∈ [], I is a symbolic interval of level and T is either true, false, a NuCAD structure of level + 1 ≤ ′ w.r.t. global level ′, or a NuCAD structure of level 1 w.r.t. global level ′. □ We omit a formal semantics due to the space limit. Intuitively, each subtree of some node either describes a decomposition of the cylinder above the cell described by the intervals on the path to the given node (as long as the levels are increasing), or describes a decomposition of that cell (if the level is reset to 1). We represent the NuCAD recursively to retain information about the arrangement of the cells, similar to [7, Definition 2]. The technicalities of this definition are not crucial for the NuCAD algorithm. We thus refrain from going into more detail.
Example 3.2. The NuCAD depicted in Figure 3 is represented by the tree partially depicted in Figure 4. A path from the root of length 2 describes a cell of the decomposition, and the following subtree the decomposition of that cell, e.g., T0 is the tree decomposing R2, T1 is the decomposition of the first cell (−∞, root 51,1) × (−∞, ∞) of T 1. Figure 5 displays the corresponding decompositions. ⌟
We present a version of the algorithm from [9, Algorithm 2] for NuCAD computation, which we adapted to be complete (i.e. not restricted to open cells only). To handle the Boolean structure of the formula, we make use of Algorithm 4 for computing implicants as in Definition 2.1. For details, we refer to [21, Section 6].
T1
(−∞, root 51,1) [root51,1, root51,1] (root51,1, ∞) (−∞, root 51,1) (−∞, ∞) (−∞, ∞) (−∞,(∞−∞), root 4,1) T2 [ro(ortoo42t,1,42r,1o,o∞t2)42,1] fa..ls.e
(−∞, root 81,1) T2 [root81,1, root81,1] (root81,1, root51,1)
T1 (−∞, root 42,1) [root51,1, root51,1] [root42,1, root42,1] false (root42,1, ∞)
(−∞, root 12,11),1] [root1,1, root (r(o− ∞ot,r122o,1o,tro ot4,1422),1)
2 (−∞, root 42,1) false false false false . . .
T3 false false 2 x 2 x s 2 x x1 (a) Partition represented by T0.
x1 (b) Partition represented by T1. 2 x
s′′′ s′′
x1 (c) Partition represented by T2.
x1 (d) Partition represented by T3.
Let us assume that we generate a NuCAD of some cell = I1 × . . . × I ⊆ R for a quantifier-free formula using Algorithm 5; for now, ignore the highlighted (but consider the underlined) bits in the algorithm. We start by picking a sample point contained in in Algorithm 5, and in Algorithm 4, we obtain an implicant for w.r.t. . In Algorithm 5, we apply the single cell construction algorithm on the obtained implicit cell. To compute a cell that is a subset of ⊆ R , we insert the defining polynomials of I1, . . . , I to in Algorithm 5 before constructing the cell.
The obtained cell ′ = I′1 × . . . × I ′ is thus a subset of , and is truth-invariant on ′. We insert the cell into the NuCAD data structure T in Algorithm 5, such that — when seen as a tree — there is a path I′1, . . . , I′ from the root node leading to t. What remains is to explore the remaining parts ∖ ′. We do so by splitting using ′ into multiple cylindrical cells in Algorithm 5: we observe that a point is outside the cell if it violates one bound. We thus iterate through each level and encode that the first − 1 levels are in ′; on the -th level, we leave ′ (we are either below or above the cell, if possible) but stay in ; and on the levels starting from + 1, we remain in , but do not make assumptions about the bounds on ′, as we already left ′ on the -th level.
We end up with a set of unexplored cells which are locally cylindrical, i.e. they are described by symbolic intervals for each variable. We call the NuCAD algorithm on each cell in in Algorithm 5 to explore the remaining parts of .
Example 3.3. Consider the formula ( 1, 2) = 1 ≤ 0 ∧ 2 > 0 ∧ 3 ≥ 0 ∧ 4 ≤ 0 ∧ 5 ≤ 0 and the polynomials from Example 2.2 again. We give an exemplary run of Algorithm 5 that computes the NuCAD as depicted in Figures 3 and 4. nucad_full(, ((−∞, ∞), (−∞, ∞))) We choose as sample point. As evaluates to false at , we obtain the implicant 5 > 0, and thus obtain ({5}, ) as implicit cell. By single cell construction, we obtain the cell described by I′1 × I ′2 = (root51,1, ∞) × (−∞, ∞) . Accordingly, we split (−∞, ∞) × (−∞, ∞) into (−∞, root 51,1) × (−∞, ∞) , [root51,1, root51,1] × (−∞, ∞) , and I′1 × I ′2, as depicted in Figure 5a. nucad_full(, ((−∞, root 51,1), (−∞, ∞))) We choose the sample point ′, and obtain the implicit cell ({4}, ′) where is truth-invariant. As we aim to compute a truth-invariant cell that is a subset of (−∞, root 51,1) × (−∞, ∞) , we run single cell construction on ({4, 5}, ′). We obtain I′ 5,1) × (root 42,1, ∞), and split into (−∞, root 51,1) × (−∞, root 42,11 )×,I(−∞′2, r=oot(−∞,51,r1o)o× t[roo1t 42,1, root42,1], and I′1 × I ′2, as depicted in Figure 5b. nucad_full(, ((−∞, root 51,1), (−∞, root 42,1))) We choose ′′, and obtain ({1}, ′′) from the implicant. We run single cell construction on ({1, 4, 5}, ′′) and obtain (−∞, root 81,1) × (−∞, root 12,1) (where 8 is the resultant of 1 and 4), and split the input cell into the cells as indicated in Figure 5c and the following recursive calls: nucad_full(. . ., ([root81,1, root81,1], (−∞, root 42,1))) . . . nucad_full(. . ., ((root81,1, root51,1), (−∞, root 42,1))) . . . nucad_full(. . ., ((−∞, root 81,1), [root12,1, root12,1])) . . . nucad_full(. . ., ((−∞, root 81,1), (root12,1, root42,1))) We choose ′′ and obtain ({2}, ′′′) from the implicant. We run single cell construction on ({1, 2, 4}, ′′′) and obtain (root61,1, root61,2) × (root 22,1, root22,2) (where 6 is the resultant of 2), and split the input cell into the cells as indicated in Figure 5d and computed by some recursive calls (omitted due to limited space). nucad_full(, ((−∞, root
51,1), [root42,1, root42,1])) . . . nucad_full(, ([root 51,1, root51,1], (−∞, ∞))) . . . ⌟
A NuCAD as computed by the algorithm presented in the previous section is not eligible for reasoning
about quantifier alternations, as it does not have the cylindrical structure. An extension for quantifier
elimination is given in [
Algorithm 4: choose_enclosing_cell(, ).
Input : Formula , ∈ R for an ∈ [] s.t. [] ≡ false or [] ≡ true.
Output : ⊆ Q[ 1, . . . , ], t ∈ {true, false} s.t. ( ′) ≡ t for all ′ ∈ (, ).
Algorithm 5: nucad_full(, , (I1, . . . , I) (I+1, . . . , I′ )).
Input : Formula , ∈ R for an ∈ [0..],
symbolic intervals (I1, . . . , I) (I+1, . . . , I′ ) for an ′ ∈ [+1..].
Output : ⊆ Q[ 1, . . . , ], and NuCAD data structure T representing a truth-invariant NuCAD of
I1 × . . . × I (, ) × I +1 × . . . × I ′ over (, ). 1 choose ∈ R s.t. ∈ I1 × . . . × I ∈ R′ s.t. ∈ × I +1 × . . . × I ′ 2 , t := choose_enclosing_cell(, ) nucad_recurse(, ) 3 := ∪ {I.. | ∈ [1..] [+1..′], I.̸= − ∞} ∪
{I.. | ∈ [1..] [+1..′], I.̸=∞} 4 foreach = , . . . , 1 ′, . . . , +1 do 5 I′ := choose_interval( ,[]) 6 := compute_cell_projection( ,[],I′)
Borrowing ideas from CAlC, we present an adaptation which directly computes a NuCAD adapted to the input’s quantifier structure, making the refinement step obsolete. For doing so, we define a NuCAD over a cell, which allows to generalize the notion of cylindricity from single levels to blocks of levels. Definition 4.1. Let ∈ [0..], ′ ∈ [+1..], and ⊆ R ′ be an algebraic cell. A NuCAD of over [] is a NuCAD of s.t. [′] = [] for all ′ ∈ . □
If we call Algorithm 5 — now we consider the highlighted and ignore the underlined parts — with a sample point ∈ R and ′ < , it will compute a NuCAD over some cell around of R′ . For doing so, it fixes the first levels of the guessed sample point in Algorithm 5, applies single cell construction only from level ′ to level + 1 in Algorithm 5, applies the splitting accordingly in Algorithm 5, and — most importantly for the correctness — collects the polynomials that characterize the NuCAD. This set consists of the polynomials of level and below that are left over from the single cell construction, and the projections obtained from the recursive calls to NuCAD (see Algorithm 5). Further, as we do not Algorithm 7: nucad_quantifier(, , , (I +1, . . . , I′ )).
Input : ∈ {∃, ∀}, formula , ∈ R for an ∈ [0..],
symbolic intervals (I+1, . . . , I′ ) for an ′ ∈ [+1..].
Output : ⊆ Q[ 1, . . . , ], t ∈ {true, false} s.t. ( ′) ≡ t for all ′ ∈ (, ). 1 choose ∈ R′ s.t. ∈ × I +1 × . . . × I ′ 2 , t := nucad_recurse(, ) 3 if ( = ∃ ∧ t = true) ∨ ( = ∀ ∧ t = false) then 4 foreach = ′, . . . , +1 do 5 I′ := choose_interval( ,[]) 6 := compute_cell_projection( ,[],I′) 7 return , t 8 := ∪ {I.. | ∈ [+1..′], I. ̸= −∞} ∪ {I .. | ∈ [+1..′], I. ̸= ∞} 9 foreach = ′, . . . , +1 do 10 I′ := choose_interval( ,[]) 11 := compute_cell_projection( ,[],I′) compute a NuCAD of R but of R′ , the call to Algorithm 6 in Algorithm 5 gets important, as it obtains a truth-invariant cell for even if is only a partial sample point.
Algorithm 6 decides whether to call Algorithm 4 or the NuCAD algorithm (we could replace nucad_quantifier(...) by nucad_full(...)). For handling formulas with quantifiers, it “structures” the NuCAD such that we construct a NuCAD for each quantifier block separately.
Although we could use Algorithm 5 for quantifier blocks, we only use it for describing the parameter space (by choosing ′ as the highest index of a free variable in the input formula); for quantifier blocks, similarly to the CAlC algorithm, we can terminate the NuCAD construction earlier, depending on the quantifier: if the given variables are existentially quantified, we can stop when we find a cell where the input formula is true, and return a projection of that cell (instead of the NuCAD). Analogously, if the given variables are universally quantified, we stop when we find a cell where the input formula is false. Algorithm 7 implements this idea and difers from Algorithm 5 only in two places: if a call to Algorithm 6 yields a desired cell, we call single cell construction and return the result in Algorithm 7. If a recursive call to itself yields such a cell, we return that cell in Algorithm 7, omitting the intermediate results from the NuCAD computation.
We implemented the NuCAD algorithm in SMT-RAT [
As the NRA and QE benchmark sets do mostly contain small formulas, we compare NuCAD and CAlC on the QF_NRA benchmark set by treating all variables as parameters, e.g. we generate a formula that describes all solutions by quantifier elimination. Note that the input formula already does this implicitly; however, the results by quantifier elimination describe them by cylindrical cells, which makes e.g. the generation of a solution point straight-forward. Of the 12154 instances, CAlC solved 9559, while NuCAD only solved 9253; CAlC solved 422 not solved by NuCAD, while NuCAD solved 116 not solved by CAlC. Figure 6 shows that CAlC is much faster on the majority of the instances, but there are instances where NuCAD is more eficient. Thus, the algorithms seem complementary to some degree.
Looking at Table 1, CAlC produces smaller solution formulas. Comparing the number of cells (before the simplification) and symbolic intervals that describe the cells, we see that NuCAD requires more cells and proportionally more computation steps (reflected by the number of symbolic intervals). The reason for this clear diference is not obvious: as the CAlC algorithm computes coverings of cylinders (which may lead to repeated expensive computations), it may visit the same cells multiple times, while NuCAD visits each cell only once (sometimes leading to coarser decompositions, e.g. compare Figure 1b and Figure 3).
Further, the CAlC avoids the costly exploration of sections more successfully than NuCAD: Looking again at Table 1, NuCAD explores 29 times more sections than CAlC. As consequence, NuCAD spends significantly more time on real root isolation. We hoped that the optimization in Section A.1 might avoid large parts of the sections. However, on instances solved by both solvers, during the run of NuCAD, only 5% of all non-point intervals have at least one closed bound. For CAlC, which implements a similar technique, this number is 90%.
NuCAD CAlC z3 cvc5 yices2
NuCAD CAlC z3 cvc5 yicesQS 20 15 10 5 0
NuCAD CAlC QEPCAD B
Redlog 0
Still, NuCAD spends fewer time on non-algebraic computations. In fact, we observe that NuCAD is able to solve bigger formulas (the mean number of nodes in the directed acyclic graph representing the formula is 833 (1565) over the instances solved exclusively by NuCAD (CAlC)), while CAlC is able to solve formulas with higher degree (the mean maximal degree is 3.8 (9.85) over the instances solved exclusively by NuCAD (CAlC)); see also Table 2 in the appendix.
We compare NuCAD and CAlC against the state-of-the-art SMT solvers z3 4.13.4, cvc5 1.2.0, and yices2
2.6.5 / yicesQS, as well as the open source quantifier elimination tools QEPCAD B (through Tarski
1.28) and Redlog 6658. The SMT results are depicted in Figure 7a and Figure 7b, the QE results in
Figure 7c. We omit the comparison against the TIOpen-NuCAD implementation from [
While NuCAD and CAlC are not competitive on QF_NRA, both outperform the other solvers on NRA. On the QE benchmarks, NuCAD even solves the most instances. However, the NRA and QE benchmarks are quite small and not diverse, we thus cannot draw any robust conclusion. Unfortunately, there are no more accessible benchmark collections for these problems available currently.
We reported on the first complete implementation of NuCAD. We simplified the algorithm for quantiifer alternation by considering the quantifier structure during the computations, and applied further optimizations to reduce the computational efort.
We evaluated the NuCAD algorithm against the related CAlC algorithm. We found that CAlC is more eficient on problems without quantifier elimination, as it produces fewer cells and avoids heavy computations with non-rational numbers more efectively. On the two benchmark sets with quantifier alternations, NuCAD was competitive or even more eficient; however, these sets are too small and not suficiently diverse for drawing any reliable conclusion. Combinations of the two algorithms could be explored in future to benefit from their individual strengths. In particular, NuCAD is better suited for parallelization: it computes a decomposition, and thus exactly describes the parts of the space which are yet unexplored. We thus can delegate their exploration to threads in a clean way.
No generative AI was used. [21] Jasper Nalbach and Gereon Kremer. Extensions of the Cylindrical Algebraic Covering Method for
Quantifiers. 2024.
David Wilson. Real Geometry and Connectedness via Triangular Description: CAD Example Bank. 2013.
The loop in Lines 10-18 of Algorithm 5 splits the input cell (I+1, . . . , I′ ) into the generated cell (I′+1, . . . , I′′ ) and the neighbouring sections and sectors: if the generated cell is a sector, then we split the space below and above into a section and sector respectively, and explore them separately. However, in many cases, handling them separately causes unnecessary efort, as their truth value may be the same — see e.g. the first and second child of T in Figure 4. In particular, exploring the sections is computationally heavy, as the points sampled from a section are likely non-rational.
By using half-closed symbolic intervals, we can avoid such unnecessary splitting (or defer splitting
in the corresponding recursive call for cases where the truth value indeed changes). For doing so, we
adapt Algorithms 5 and 7 as follows:
• We allow closed bounds (e.g. (, ], [, ]) for the symbolic intervals of the input cell and the
generated cell.
• When adding the defining polynomials of the input cell to the polynomial set in Algorithm 5
of Algorithm 5, we flag the ones that stem from closed bounds. For them, we do not require
sign-invariance in the required cell, but only semi-sign-invariance (it holds ≤ 0 or ≥ 0 on the
required cell), which is introduced in [
// analogous For constructing a solution formula for quantifier elimination problems, we need to encode the NuCAD that describes the solution space. For doing so, we apply a post-processing to the NuCAD data structure — similarly as done for the CAlC algorithm in [21]. The idea is — given some node in the NuCAD data structure — (1) to merge all neighbouring children which carry the same label (true or false) and (2) to replace the subtree of a node where all of its leaves carry the same label by that label. Example A.1. Consider Figure 3. The cell [root51,1, root51,1] × (−∞, ∞) is split into multiple cells which carry the same label, thus they can be merged during post-processing. Similarly, the cells after (−∞, root 81,1)×[root 42,1, root42,1] and (−∞, root 81,1)×[root 12,1, root12,1] can be merged respectively. ⌟
For obtaining the solution formula, we encode the parts of the tree that describe the cells labelled with true. Without the preprocessing step, we would only need to encode the outermost bounds on the variables (i.e. the bounds in the nodes closest to the leaves). However, after the preprocessing, some of these bounds are omitted; we thus need to include additional (non-outermost) bounds on variables. Further, in some cases, we would yield smaller solution formulas by taking the negation of the encoding of the cells labelled with false. The work in [21] describes a technique that makes use of this observation and applies it also to subtrees of the NuCAD data structure.
# nodes median max mean max degree median max