One of the few available complete methods for checking the satisfiability of sets of polynomial constraints over the reals is the cylindrical algebraic covering (CAlC) method. In this paper, we propose an extension for this method to exploit the strictness of input constraints for reducing the computational efort. We illustrate the concepts on a multidimensional example and provide experimental results to evaluate the usefulness of our proposed extension.
Quantifier-free (non-linear) real-algebraic ( QFNRA) formulas are Boolean combinations of
polynomial constraints over the reals. Eficiently determining the satisfiability of such formulas
has become increasingly relevant in the last decades. A relatively recent general methodology,
which has been proven very successful, encodes various properties of real-world systems by
such formulas, e.g. the correctness of programs [
Besides general-purpose computer algebra systems, this functionality is ofered by some dedicated satisfiability modulo theories (SMT) solvers . These tools use SAT solving to identify sets of polynomial constraints whose truth satisfies the Boolean structure of an input formula, and require a theory solver that can check the satisfiability of such constraint sets.
There are a few, even though not many, algorithms available that can be implemented to
obtain such a theory solver. Incomplete methods like interval constraint propagation [
The QFNRA satisfiability problem is decidable [ 13] but hard. Both CAD and CAlC might need doubly exponential efort in the worst case [ 14] and there are currently no cheaper alternatives, even though QFNRA is known to be solvable in singly exponential time [15]. Thus optimizations play an important role to improve applicability and practical relevance.
In this paper we propose such an optimization for the CAlC algorithm: we exploit knowledge about the strictness of input constraints in order to reduce the computational efort. For constraints in variables, the CAlC method iteratively computes subsets of R over which the input constraint set is invariantly unsatisfiable, until either it finds a solution or the computed subsets cover R. Such a covering is composed of a finite number of open and non-open subsets, where each non-open one lies in the boundary of an open one. Previous work like e.g. [16] already exploited the well-known fact that if all input constraints are strict then only the open subsets need to be considered: if there is a solution in a non-open subset then there is also an -ball of solutions around it, therefore also the open subset whose boundary contains will contain solutions. Skipping non-open subsets does not simply reduce the number of cases, but it avoids the hard cases, which typically require efortful computations with non-rational real-algebraic numbers. In this work, we go further and show that we can neglect some of the non-open subsets even if not all (but some) of the input constraints are strict. This paper has three main contributions: 1. We formalize the above-mentioned optimization for the CAlC method, to save efort in the presence of strict input constraints. Since a decomposition is a special type of covering, our results are transferable to the CAD method. 2. We provide a publicly available implementation of the proposed optimization. 3. We evaluate this implementation to evaluate and compare the modification to the original
CAlC method.
Outline: We introduce the CAD and the CAlC methods in Section 2 before we present our optimization in Section 3. We discuss the implementation in the SMT-RAT toolbox [17] and provide experimental results to demonstrate efectiveness in Section 4. Finally, we draw conclusions in Section 5.
all natural, natural excluding zero, rational resp. real numbers. For ∈ R, its sign sgn() is 1 if > 0, 0 if = 0, and − 1 otherwise. For a set , we define () = {′ | ′ ⊆ }.
Assume for the rest of the paper ∈ N>0 and some statically ordered variables 1≺ . . . ≺ . Let ∈ N>0 with ≤ . By Q[1, . . . , ] we denote the set of all polynomials with variables 1, . . . , and rational coeficients. The variety of ∈ Q[1, . . . , ] is the set of its real zeros or roots { ∈ R | () = 0}. A (QFNRA) constraint has the form ∼ 0 with ∈ Q[1, . . . , ] and ∼ ∈ { <, ≤ , =, ̸=, ≥ , >}; ∼ 0 is strict if ∼ ∈ { <, >, ̸=}. A (QFNRA) formula is a Boolean combination of constraints. By (1, . . . , ) we express that Q[1, . . . , ] includes all polynomials appearing in . For (1, . . . , ) ∈ R, by (1, . . . , , +1, . . . , ) we denote the formula [1/1] . . . [/] after substituting for for = 1, . . . , .
A cell is a non-empty, connected subset of R for some 1 ≤ ≤ . Let ⊆ R be a cell. Given ∈ R, > 0 and ∈ R, the -ball around is the set () := {′ ∈ R | | − ′| ≤ }. is open if for all ∈ there is an ∈ R, > 0 such that () ⊆ . is closed if R ∖ is open. The closure cl () of is its smallest closed superset, its interior int () is its largest open subset, and its boundary bound () is its closure without its interior.
is semi-algebraic if it is the solution set of a QFNRA formula. Assuming ∈ N>0 with 1 ≤ < , the projection of to R is ↓ = {(1, . . . , ) | (1, . . . , ) ∈ }; note that if is semi-algebraic then ↓ is semi-algebraic.
is sign-invariant for ⊆ Q[1, . . . , ] if sgn(()) = sgn((′)) for all ∈ and all , ′ ∈ . is truth-invariant (respectively UNSAT ) for a formula (1, . . . , ) if () and (′) simplify to the same truth value (respectively to False) for all , ′ ∈ . For ⊆ Q[1, . . . , ] and ∈ R, by (, ) we denote the maximal cell ⊆ R that is sign-invariant for and contains .
Cell properties are generalized to sets of cells by requiring the respective property for each cell in the set. E.g., a cell set ⊆ (R) is semi-algebraic if each ∈ is semi-algebraic. We also extend the projection to sets of cells ⊆ (R) as ↓ = { ↓ | ∈ }.
Collins in 1975. Despite its doubly exponential complexity, all complete algorithms in SMT solvers for QFNRA are based on the techniques underlying the CAD. This also holds true for the CAlC method. For a formula (1, . . . , ), the CAD method decomposes R into a finite set of cells that are sign-invariant for the polynomials in and thus truth-invariant for , such that we can decide ’s satisfiability by evaluating it at one sample point from each ∈ . Definition 1 (Cylindrical algebraic decomposition). Assume ∈ N>0 with ≤ . • A decomposition of R is a finite set ⊂ (R) such that ∪∈ = R and either = ′ or ∩ ′ = ∅ for every , ′ ∈ . • A decomposition of R is algebraic if each ∈ is a semi-algebraic cell. • A decomposition of R is cylindrical if either = 1, or > 1 and − 1 = { ↓− 1| ∈ } is a cylindrical decomposition of R− 1.
For a finite set of polynomials ⊂ Q[1, . . . , ], the CAD method computes CADs 1, . . . , of R1, . . . , R with ↓− 1= − 1 for = 2, . . . , , in two phases: (1) The projection phase computes for = , . . . , 1, in this order, finite sets of polynomials ⊂ Q[1, . . . , ] such that the varieties of ∪=1 define the boundaries of the cells in . Starting from = , for = − 1, . . . , 1 we obtain by a projection operator proj : (Q[1, . . . , +1]) → (Q[1, . . . , ]) that eliminates the highest variable from its input polynomials. We do not define proj here, it sufices to assume that it maintains some properties such that the resulting CAD is sign-invariant for . (2) In the lifting phase, compute the cells in the CADs 1, . . . , , in this order. Instead of representing them explicitly, usually a sample point for every cell is generated. For ∈ {1, . . . , } and ∈ R− 1 (with R0 = {()}), let Ξ = { ,1, . . . , , } be the ordered set of all real roots of the univariate polynomials from {(, ) | ∈ }. Let furthermore = {(−∞ , ∞)} if Ξ = ∅, and otherwise let consist of all point-sets { , }, = 1, . . . , (which cover the sections, i.e. the cells consisting of roots of ), and the intervals (−∞ , 1), ( 1, 2), . . . , ( − 1, ), ( , ∞) (which cover the sectors, i.e. the open cells between the sections). Assume furthermore a fixed but arbitrary function sample that assigns to each non-empty interval a value from this interval. For = 1, . . . , , based on − 1 with 0 = {()}, we iteratively define the sample sets for as = {(, ) | ∈ − 1 ∧ ∈ ∧ = sample()}.
Example 1. Consider = 2 = {1 : − 21 − 2 + 1, 2 : 21 − 2 − 1, 3 : (1 − 0.5)2 + (2 + 1.5)2 − 0.25, 4 : 1 + 0.5} with projection 1 = proj 2(2). Figure 1 depicts the varieties of the polynomials from 2, and below it those from 1. The intervals defined by the real zeros from 1 form a sign-invariant CAD 1 for 1. The sign-invariant CAD 2 for 2 is cylindrical over 1, i.e. the cells of 2 are arranged in cylinders over 1. In 1, the sections are the cells containing only a real root from 1, the open intervals are the sectors. In 2, we extend the varieties with the cylinder boundaries induced by 1, and define 2’s sections as the intersection points of lines as well as the line segments bounded by them, and the sectors as the open cells bounded by the sections. 2
We note that not only the computation of the projection is computationally expensive, but also
the number of samples grows exponentially with the number of variables. Although lifting over
rational samples (that involves plugging in the sample point to obtain univariate polynomials
and isolating their real roots) is rather eficient, in general, expensive lifting over non-rational
real-algebraic samples (which requires similar machinery as the projection) cannot be avoided.
Cylindrical algebraic covering CADs are finer than what we actually need for checking
the satisfiability of QFNRA formulas, as we either need to find a satisfying sample, or cover R
with UNSAT cells. Example 1 illustrates that cells which are UNSAT for a constraint are often
split into several smaller cells due to sign changes of some other polynomials. To avoid such
splits, the cylindrical algebraic covering (CAlC) [
• A covering of R is a finite set ⊆ (R) such that ∪∈ = R. • A covering of R is algebraic if each ∈ is a semi-algebraic cell. • A covering of R is cylindrical if either = 1, or > 1 and − 1 = { ↓− 1| ∈ } is a cylindrical covering of R− 1.
The CAlC method is sample-guided: in contrast to CAD, it does not start with projection but with a dimension-wise guess of values for a sample, with the aim to satisfy the input formula . For a current partial sample (1, . . . , − 1) ∈ R− 1 with 1 ≤ ≤ , we iteratively identify intervals ⊆ R such that for any ∈ , (1, . . . , ) is unsatisfiable. We continue this process until either we find a solution (along with a partial UNSAT covering) or the intervals cover the whole R. In the latter case, if = 1 then the problem is unsatisfiable and a complete CAlC is returned; otherwise, we backtrack one level to sampling for − 1, generalize − 1 to an unsatisfying interval, and try to guess another value for − 1 outside the already excluded intervals. The interval generalization of − 1 is computed using real root isolation and a reduced version of the CAD projection. Intuitively, it contains − 1 and other points ′− 1 for which (1, . . . , − 2, ′− 1) is unsatisfiable for same reason as (1, . . . , − 2, − 1).
In general, CAlCs require less computational efort than CADs: the sample-based search in CAlC saves parts of the projection executed in CAD, as well as the lifting efort corresponding to them.
Example 2. Re-using = {1 : − 21 − 2 + 1, 2 : 21 − 2 − 1, 3 : (1 − 0.5)2 + (2 + 1.5)2 − 0.25, 4 : 1 + 0.5} from Example 1, we consider the formula := 1 < 0 ∧ 2 > 0 ∧ 3 ≥ 0 ∧ 4 ≥ 0. Figure 1 illustrates on the right the following CAlC computations.
Samples 1 ∈ (−∞ , − 0.5) violate 4 ≥ 0. Outside (−∞ , − 0.5) we pick 1 = 0.25 for 1, and consider (0.25, 2). The constraint 1(0.25, 2) < 0 is unsatisfiable for 2 ∈ (−∞ , 1165 ), and 2(0.25, 2) > 0 is unsatisfiable for 2 ∈ (− 1156 , ∞), together covering the real line. We generalize the UNSAT result to the cell (− 1, 1) containing 1 = 0.25 in the 1 CAD for {1, 2} (see also Example 3).
Outside (−∞ , − 0.5) ∪ (− 1, 1) we pick 1 = 1 for 1, and compute a covering of unsatisfying
intervals for (1, 2) as depicted in the two-dimensional coordinate system. This time the sample
1 = 1 is a real root, which cannot be generalized further than the section [
Next, we pick a satisfying sample with 1 = 1.5 and 2 = 0, and the algorithm terminates.
This example shows where the CAlC method is more eficient than the CAD: Firstly, single constraints like 4 ≥ 0 above can be used to rule out parts of the search space requiring fewer projection and lifting steps. Secondly, the CAlC method does not necessarily involve all polynomials in projection and corresponding lifting steps if they are redundant, as e.g. 3 ≥ 0 above excludes part of the search space that is already ruled out by the other constraints. 2
Each UNSAT interval ⊆ R generated during the CAlC computations over some partial sample ∈ R− 1 corresponds to an UNSAT cell ⊆ R with {} × = ({} × R) ∩ . This UNSAT cell is represented implicitly by a set of polynomials ⊂ Q[1, . . . , ] and the sample (, ) for some ∈ such that, except for some special cases, is the maximal sign-invariant cell for that contains (, ), i.e. = (, (, )).
For generalizing a covering of intervals 1, . . . , ⊆ R (i.e. ∪=1 = R) over some sample point ∈ R− 1, the CAlC method defines a partial projection operator that projects the implicitly represented cells to an ( − 1)-dimensional cell containing as follows: Definition 3. The covering projection operator proj cov is a function which, for any , ∈ N>0, 1, . . . , ⊂ Q[1, . . . , ], ∈ R− 1 and ′1, . . . , ′ ∈ R with × R ⊆ ∪ =1( , (, ′ )) as input, returns a set of polynomials = proj cov(1, . . . , , , ′1, . . . , ′) ⊆ Q[1, . . . , − 1] with the property that (, ) × R ⊆ ∪ =1( , (, ′ )).
The correctness of an UNSAT covering is given by the following theorem: Theorem 1. Let be a formula in variables 1, . . . , , > 1, 1, . . . , ⊆ Q[1, . . . , ], ∈ R− 1 and ′1, . . . , ′ ∈ R such that × R ⊆ ∪ =1( , (, ′ )) and for all = 1, . . . , the cell ( , (, ′ )) is UNSAT for .
Then (proj cov(1, . . . , , , ′1, . . . , ′), ) is UNSAT for .
Strict constraints < 0 are never satisfied at the real roots of . Therefore, when checking the satisfiability of a formula that contains only strict constraints (and no negations), sections can be neglected in CAD and CAlC computations, i.e. real roots can be omitted during sample construction. This observation is exploited e.g. in [16].
In this work we propose an approach that allows to omit real roots during sample construction in certain cases even if the input formula contains also weak constraints. We start with illustrating the idea on an example.
Example 3. In Example 2, for each 1 ∈ R, both 1(1, 2) and 2(1, 2) have exactly one real root, which we denote by 1(1) respectively 2(1).
For the sample 1 = 0.25 for 1, we covered 2 by the intervals (−∞ , 1156 ) violating 1 < 0, and (− 1156 , ∞) violating 2 > 0. The above intervals represent the cells {(1, 2) ∈ R2 | 2 < 1(1)} and {(1, 2) ∈ R2 | 2 > 2(1)}. The generalization of 1 = 0.25 is the maximal interval (− 1, 1) over which the above cells still build a covering (see Figure 1).
Note that 2 = 1(1) implies 1 = 0, and 2 = 2(1) implies 2 = 0. Thus, the closures {(1, 2) ∈ R2 | 2 ≤ 1(1)} and {(1, 2) ∈ R2 | 2 ≥ 2(1)} are still unsatisfying for 1 < 0 (a) Closed cells from strict constraints.
(b) Closed generalizations from coverings of closed cells.
(c) A closed set with open
projection.
resp. 2 > 0. Now, since both cells are closed, they cover 2 over the closed generalization [
Clearly, if we are able to deduce closed intervals, the computed CAlC consists not only of fewer cells, but we can also avoid computationally intensive lifting operations over potentially non-rational algebraic numbers. The following example demonstrates that for two-dimensional formulas we could go even further.
Example 4. Assume in the previous example that the first constraint would be non-strict, then for
the constraints 1(0.25, 2) ≤ 0 and 2(0.25, 2) > 0 we would achieve the covering (−∞ , 1165 )
and [− 1165 , ∞) for 2. Now, only the second cell is closed. However, this still sufices to cover [
However, generalizing this observation to constraint sets with more than two variables is non-trivial; we therefore focus on the case where all intervals of a covering are closed.
To that end, we change our view from UNSAT intervals to the UNSAT cells they represent. During the CAlC computations, some UNSAT cells violate a constraint (as indicated by the arrows in Figure 2a); as illustrated in Example 3, we can close those cells that violate strict constraints ∼ 0 (i.e. () ̸∼ 0 for all ∈ ) without losing the UNSAT property of the cell (i.e. () ̸∼ 0 for all ∈ cl ()).
Furthermore, for any covering by UNSAT intervals which represent the -dimensional closed cells 1, . . . , ⊆ R, if ⊆ R− 1 is a possible generalization of the current sample (i.e. × R ⊆ ∪ =1 ), then also the closure of is a valid generalization (cl () × R ⊆ ∪ =1 ). This fact is formalized in the following theorem and visualized in Figure 2b. Theorem 2. Assume , ∈ N>0, closed cells 1, . . . , ⊆ × R ⊆ ∪ =1 . Then cl () × R ⊆ ∪ =1 .
R, and a cell ⊆
R− 1 such that Proof. Assume for contradiction that there exists an ∈ bound () × R ⊆ R such that ∈/ ∪=1 . Then ∈/ , i.e. ∈ R ∖ for all ∈ {1, . . . , }. As the sets are closed, their complements R ∖ are open. By definition of an open cell, for each ∈ {1, . . . , } there exist > 0 such that () ⊆ R ∖ . Let be the smallest such under all ∈ {1, . . . , }. Then () ⊆ R ∖ for all ∈ {1, . . . , }. As ∈ bound () × R = bound ( × R), by the definition of () there exist an ′ ∈ () ∩ ( × R), in other words, ′ ∈/ for all ∈ 1, . . . , , which is a contradiction to the assumption that × R ⊆ ∪ =1 .
The above theorem might seem straight-forward at the first sight, but there are some special cases that make it less trivial, e.g. that the projection of a closed cell might not be closed as shown in Figure 2c.
Now, we apply the general Theorem 2 from above to Theorem 1 to obtain a variant that supports the derivation of closed cells.
Theorem 3. Let be a formula in variables 1 . . . , , > 1, 1, . . . , ⊆ Q[1, . . . , ], ∈ R− 1 and ′1, . . . , ′ ∈ R such that × R ⊆ ∪ =1cl (( , (, ′ ))) and for all = 1, . . . , the cell cl (( , (, ′ ))) is UNSAT for .
Then cl ((proj (1, . . . , , , ′1, . . . , ′), )) is UNSAT for .
Proof sketch. Let ≥ , +1, . . . , ⊆ Q[1, . . . , ], ′+1, . . . , ′ ∈ R such that × R ⊆ ∪=1( , (, ′ )) and for every ′ = + 1, . . . , there exists a ∈ {1, . . . , } such that ′ = and (, ′′ ) ∈ bound (( , (, ′ ))), that means (′ , (, ′′ )) ⊆ bound (( , (, ′ ))).
Then by Theorem 1 it holds for := proj (1, . . . , , , ′1, . . . , ′) that (, ) × R ⊆ ∪=1( , (, ′ )) = ∪=1cl (( , (, ′ ))).
We now apply Theorem 2 to (, ) and cl (( , (, ′ ))), = 1, . . . , and obtain cl ((, )) × R ⊆ ∪ =1cl (( , (, ′ ))).
For the theorem, it remains to show that = proj (1, . . . , , , ′1, . . . , ′). A formal proof would require the definition of the details of the projection operator proj , which we had to omit due to space restrictions. At this point, we just state without proving that adding the additional cells does not change the projection. We justify that as each additional cell (′ , ′′ ), = + 1, . . . , describes the boundary of a neighbouring open cell ( , ′ ) for some ∈ {1, . . . , } and the defining polynomial sets = ′ are equal, and thus the ‘skeleton’ of the covering does not change.
This result yields a simple adaption of the CAlC algorithm: Along with each implicit cell representation, we store a Boolean flag that indicates whether the corresponding unsatisfiable cell is closed or not. If the flag is set, the corresponding cell is closed, thus we can set the bounds of the witnessing interval to closed. Whenever we compute the base cell of a covering consisting of closed cells, we can easily deduce the flag for the new cell (it is true whenever the parents’ lfags are all true). Thus, any implementation of the CAlC implementation can be adapted for the theorem by only superficial changes in the code.
We provide a 3D example for the covering method and our adaption in the appendix of [19].
We implemented the proposed method to exploit strict constraints in our SMT-RAT [17] solver, using standard preprocessing and DPLL(T) solving with an implementation of the CAlC method ) (% 80 s l lce 60 d seo 40 l c fo 20 e rah 0 S ⊥
Trivial instances d e i l p p a s y a w l a m e r o e h T as the only theory solver. The implementation is accessible at https://doi.org/10.5281/zenodo. 7900518. We execute the solver on the QF_NRA benchmark library from SMT-LIB [20] (as of April 2022), consisting of 11552 instances that stem from 11 diferent families. Each formula is solved on a CPU with 2.1 GHz with a timeout of 60 seconds and a memory limit of 4 GB. In the following, we denote the original CAlC solver by CAlC and the modification that maintains interval flags to indicate closed cells by CAlC-I.
Table 1 shows the overall performance of CAlC and CAlC-I. The modified method CAlC-I solves 80 instances more than CAlC, whereby more than two thirds of this gain is on SAT instances, the remaining on UNSAT instances. CAlC times out on 77 instances which are solved by CAlC-I. Conversely, CAlC-I times out on 7 instances which are solved by CAlC. Applications of the theorem Figure 3 depicts the share of the derived implicit cell representations that carry a True flag (i.e. Theorem 3 was applicable during its creation). More than half of the instances are already solved by the SAT solver (the theory solver is never called) or the call to the CAlC contains only univariate polynomials. The theorem is never applied on 2518 instances. The theorem is applied at least once in 1699 instances. The theorem is always applied on 1162 instances (i.e. all cells are closed).
We focus the further analysis on the interesting instances where the theorem was applied at least once: the instances solved by both solvers and the theorem was applied at least once (1623 instances), instances solved only by CAlC (8 instances), and instances solved only by CAlC-I (88 instances).
Running times Figure 4a compares the running times of CAlC and CAlC-I on the interesting instances. The bottom left cluster of instances is computationally easy; small deviations in running time between CAlC and CAlC-I are negligible. Most instances with higher running time are located near the equality line, i.e. CAlC and CAlC-I are equally eficient on them. There are 30 instances solved faster by more than 0.1 seconds on CAlC than on CAlC-I (including instances solved only by CAlC, see area below the equality line). The other way around, 197 instances are solved faster by CAlC-I (see area above the equality line). We conclude that CAlC-I can significantly improve the running time on certain instances.
In particular, some UNSAT instances (blue crosses) deviate from the equality line for running times greater than one second. CAlC-I is able to cover the entire space with fewer UNSAT cells than CAlC; this efect is less significant on the SAT instances, where only a partial covering is computed.
Number of samples We expect that the advantage of the proposed optimization is due to the fact that the application of Theorem 3 reduces the number of samples constructed in the CAlC method.
To evaluate this correlation, Figure 4b compares the number of partial sample points of CAlC and CAlC-I. Though the number of samples is often similar, CAlC-I tends to generate fewer samples especially on the larger instances.
Iterative applications of the theorem As Theorem 3 can only be applied if all cells forming the covering are closed, the question raises how often it can be applied iteratively. To that end, we say that the cells forming a covering are the parents of the covering’s base cell. In that sense, we define for every cell its depth as the distance to its ‘oldest’ ancestor. Figure 5a plots for every instance the maximal depth among all cells versus the relative maximal depth among all closed cells.
We clearly see that the theorem is mostly applicable to cells with low depth. In particular, the 1308 instances at the top left of the plot, where at least one closed cell has maximal depth, have a total maximal depth below 10. Further, the instances where the theorem is only applied to cells with depth one form a visible hyperbola, which are 1159 of the 1711 depicted instances. We conclude that the performance gains stem mostly from ‘superficial’ application of the theorem. Still, there are some instances above this hyperbola, representing non-trivial applications of our theorem.
CAlC & CAlC-IH
Only CAlC-IH (a) Cell depth ratio of CAlC-I (b) Cell depth ratio of CAlC-IH Figure 5: Maximal cell depth and the relative maximal closed cell depth.
Modification of the covering heuristic The modification CAlC-I is clearly more eficient than CAlC; as we just observed, these gains are due to ‘superficial’ application of Theorem 3. We now aim to adapt the CAlC-I method to support the application of the theorem also to cells of higher depth. Whenever the CAlC method finds a covering of cells at some sample, the choice of the cells forming the covering is not unique; redundancies in the formula might allow for a choice of the cells. CAlC-I heuristically minimizes the number of cells forming a covering. We propose an adaption CAlC-IH which first tries to cover using closed cells only, and falls back to the default heuristic if it fails.
Figure 5b shows that the theorem is now applied on more instances with higher depth. However, the running times do not improve significantly (not shown here); Table 1 shows that even one instance less is solved. Thus, more sophisticated heuristics are desirable which find a better trade of between a covering of ‘good’ intervals and supporting the theorem applicability.
The cylindrical algebraic covering method admits reducing the number of projection and lifting operations compared to the cylindrical algebraic decomposition switching from being signinvariant for a set of polynomials to being truth-invariant for an input formula. In this paper, we propose a natural extension to the CAlC method that exploits strict constraints in the input formula: If a strict constraint is unsatisfiable in some cell, then it is so in the closure of that cell. Our adaption allows to carry this information through the CAlC algorithm to avoid lifting over roots of polynomials, which is desirable as this is usually computationally expensive.
The proposed adaption is easy and eficient to implement. Our experimental evaluation concluded that (1) we gain a good portion of newly solved instances, (2) these gains are due to reduced number of lifting steps, and (3) our modification is still ‘superficial’ and leaves potential for future investigation into the topic.
Future work consists of advanced theoretical work as motivated by Example 4, and better heuristics for choosing good coverings as motivated in the last paragraph of Section 4.
Jasper Nalbach was supported by the DFG RTG 2236/2 UnRAVeL. We thank James Davenport and Matthew England for fruitful discussions. of the 28th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’22), volume 13243 of LNCS, Springer, 2022, pp. 415–442. URL: https: //doi.org/10.1007/978-3-030-99524-9_24. doi:10.1007/978-3-030-99524-9\_24. [12] SMT-COMP 2022, https://smt-comp.github.io/2022/, 2022. [13] A. Tarski, A Decision Method for Elementary Algebra and Geometry, RAND Corporation, 1951. doi:10.1007/978-3-7091-9459-1_3. [14] J. H. Davenport, J. Heintz, Real quantifier elimination is doubly exponential, J. Symbolic
Comp. 5 (1988) 29–35. [15] C. W. Brown, J. H. Davenport, The complexity of quantifier elimination and cylindrical algebraic decomposition, in: Proceedings of ISSAC’07, 2007, pp. 54–60. [16] C. W. Brown, Open non-uniform cylindrical algebraic decompositions, in: Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC’15, Association for Computing Machinery, 2015, p. 85–92. doi:10.1145/2755996. 2756654. [17] F. Corzilius, G. Kremer, S. Junges, S. Schupp, E. Ábrahám, SMT-RAT: An open source C++ toolbox for strategic and parallel SMT solving, in: Proceedings of the Theory and Applications of Satisfiability Testing, SAT’15, Springer, 2015, pp. 360–368. doi: 10.1007/ 978-3-319-24318-4_26. [18] G. Kremer, J. Nalbach, Cylindrical algebraic coverings for quantifiers, in: Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation (SC² 2022), 2022. URL: https://nafur.github.io/static/2022-scsc-qe-coverings.pdf. [19] P. Bär, J. Nalbach, E. Ábrahám, C. W. Brown, Exploiting strict constraints in the cylindrical algebraic covering, 2023. doi:https://doi.org/10.48550/arXiv.2306.16757. [20] C. Barrett, P. Fontaine, C. Tinelli, The satisfiability modulo theories library (SMT-LIB), www.SMT-LIB.org, 2021.