=Paper= {{Paper |id=Vol-3717/paper8 |storemode=property |title=Under-Approximation of a Single Algebraic Cell (Extended Abstract) |pdfUrl=https://ceur-ws.org/Vol-3717/short3.pdf |volume=Vol-3717 |authors=Valentin Promies,Jasper Nalbach,Erika Abraham |dblpUrl=https://dblp.org/rec/conf/paar/PromiesNA24 }} ==Under-Approximation of a Single Algebraic Cell (Extended Abstract)== https://ceur-ws.org/Vol-3717/short3.pdf

Under-Approximation of a Single Algebraic Cell (Extended
Abstract)
Valentin Promies1,* , Jasper Nalbach1 and Erika Ábrahám1
1
RWTH Aachen University, Germany

Abstract
Single cell construction is a crucial subroutine in modern SMT solvers for non-linear real arithmetic. In this
extended abstract, we adapt a recent approach by dynamically under-approximating the cell boundaries using
linear polynomials, which can greatly reduce the effort of resultant computations, while maintaining the sign-
invariance properties of the cell. Although one must be careful to ensure termination, first experiments suggest
that this modification pays off in the context of SMT solving.

Keywords
Single Cell Construction, Approximation, Real Algebra, Cylindrical Algebraic Decomposition

1. Introduction
The NLSAT algorithm [1] is a modern and complete approach for deciding the satisfiability of quantifier-
free formulas in the theory of non-linear real arithmetic, and it relies heavily on a subroutine for single
cell construction (SCC): Given a sample point 𝑠 ∈ R𝑛 and a finite set 𝑃 ⊂ Q[𝑥1 , . . . , 𝑥𝑛 ] of polynomials,
the task is to compute the representation of a cell 𝑆 ⊂ R𝑛 , so that 𝑠 ∈ 𝑆 and the polynomials in 𝑃 are
sign-invariant over 𝑆. The cell 𝑆 is connected and algebraic, i.e. its boundaries are defined by the roots
of some polynomials.
NLSAT invokes this subroutine when it finds a sample 𝑠 at which the given formula is conflicting: the
conflict is generalized to 𝑆, which is then excluded from the search space. Accordingly, the excluded
cell should be as large as possible. However, the representation should be efficiently usable by NLSAT,
and, as SCC is based on the cylindrical algebraic decomposition [2], its computational effort can grow
quickly. Thus, 𝑆 is generally not inclusion-maximal in practice.
Recently, Nalbach et al. introduced a levelwise approach to SCC [3], which evolved from the method
of Brown and Košta [4]. We modify this approach by allowing it to dynamically under-approximate cell
boundaries using low-degree polynomials. This reduces the computational effort of the construction,
but it also affects the quality of the cell for NLSAT and the methods’ completeness.

2. Levelwise Single Cell Construction
Originally, Nalbach et al. [3] formulated the levelwise single cell construction by means of a proof
system, which offers great flexibility in heuristic choices. We now give a brief recall of the method, but
we omit details and focus here on those parts that we will adapt later, in Section 3.
For a given finite set 𝑃 ⊂ Q[𝑥1 , . . . , 𝑥𝑛 ] of 𝑛-variate polynomials and a given sample point 𝑠 ∈ R𝑛 ,
the method constructs a representation I = (𝐼1 , . . . , 𝐼𝑛 ) of a cell 𝑆 ⊆ R𝑛 so that 𝑠 ∈ 𝑆 and for all 𝑝 ∈ 𝑃
holds ∀𝑠′ ∈ 𝑆. 𝑠𝑖𝑔𝑛(𝑝(𝑠′ )) = 𝑠𝑖𝑔𝑛(𝑝(𝑠)). In the output representation, each 𝐼𝑖 is a symbolic interval
which bounds the value of 𝑥𝑖 w.r.t the variables 𝑥1 , . . . , 𝑥𝑖−1 of the lower levels, either by a lower and
an upper bound (𝑙(𝑥1 , . . . , 𝑥𝑖−1 ) < 𝑥𝑖 < 𝑢(𝑥1 , . . . , 𝑥𝑖−1 )) or by an equality (𝑥𝑖 = 𝑏(𝑥1 , . . . , 𝑥𝑖−1 )).

9th International Workshop on Satisfiability Checking and Symbolic Computation, July 2, 2024, Nancy, France, Collocated with
IJCAR 2024
*
Corresponding author.
$ promies@cs.rwth-aachen.de (V. Promies); nalbach@cs.rwth-aachen.de (J. Nalbach); abraham@cs.rwth-aachen.de
(E. Ábrahám)
0000-0002-3086-9976 (V. Promies); 0000-0002-2641-1380 (J. Nalbach); 0000-0002-5647-6134 (E. Ábrahám)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
The method maintains a working set 𝑃* of polynomials, which is initialized as 𝑃* := 𝑃 .
For 𝑖 = 𝑛, . . . , 1 (i.e. starting with 𝐼𝑛 and iterating down to 𝐼1 ), the interval 𝐼𝑖 at level 𝑖 is then
computed as follows.

1. Let 𝑃𝑖 := (𝑃* ∩ Q[𝑥1 , . . . 𝑥𝑖 ]) ∖ Q[𝑥1 , . . . 𝑥𝑖−1 ].
2. Isolate the real roots 𝑝∈𝑃𝑖 {𝑟 ∈ R | 𝑝(𝑠1 , . . . , 𝑠𝑖−1 , 𝑟) = 0} and order them, together with the
⋃︀
sample coordinate 𝑠𝑖 , giving −∞ < 𝑟1 ≤ . . . ≤ 𝑟𝑙 < 𝑠𝑖 < 𝑟𝑙+1 ≤ . . . ≤ 𝑟𝑚 < ∞. In this
paper, we only consider the case that 𝑠 is not a root of any polynomial in 𝑃* .
3. In a neighborhood of the sample, each root can be generalized to a continuous function, encoded
as an indexed root expression (IRE) of the form root𝑥𝑖 [𝑝, 𝑗] : R𝑖−1 → R ∪ {⊥}, which maps a given
(𝑖 − 1)-dimensional sample to the 𝑗-th real root of the polynomial 𝑝 in 𝑥𝑖 if it exists and otherwise
returns ⊥ (i.e. “undefined”). For an IRE 𝜉, we refer to the according polynomial by 𝜉.𝑝.
4. For 𝑖 ∈ {1, . . . , 𝑚}, let 𝜉𝑖 be the IRE corresponding to the root 𝑟𝑖 , and let Ξ = {𝜉1 , . . . , 𝜉𝑚 }.
5. Set 𝐼𝑖 := (𝜉𝑙 (𝑥1 , . . . , 𝑥𝑖−1 ) < 𝑥𝑖 < 𝜉𝑙+1 (𝑥1 , . . . , 𝑥𝑖−1 )).
6. The symbolic interval 𝐼𝑖 is only correct in a certain neighborhood of the sample, which is why
the underlying cell defined by (𝐼1 , . . . , 𝐼𝑖−1 ) is restricted using a projection.
a) To ensure well-definedness of the root functions over the underlying cell, it is restricted
so that the polynomials are delineable, by adding discriminants disc𝑥𝑖 [𝑝] ∈ Q[𝑥1 , . . . , 𝑥𝑖−1 ]
and some coefficients of the polynomials 𝑝 from 𝑃𝑖 to the working set 𝑃* .
b) To ensure that no root function crosses the boundaries defined by 𝐼𝑖 , choose a relation ⪯ ⊂
Ξ × Ξ so that (𝜉𝑙 , 𝜉𝑙+1 ) ∈ ⪯, {(𝜉𝑗 , 𝜉𝑙 ) | 𝑗 < 𝑙} ⊂ ⪯* and {(𝜉𝑙+1 , 𝜉𝑗 ) | 𝑙 + 1 < 𝑗 ≤ 𝑚} ⊂ ⪯* ,
where ⪯* is the transitive closure of ⪯. Then update 𝑃* := 𝑃* ∪ {res𝑥𝑖 [𝜉.𝑝, 𝜉 ′ .𝑝] | 𝜉 ⪯ 𝜉 ′ },
where the resultant res𝑥𝑖 [𝑝, 𝑞] ∈ Q[𝑥1 , . . . , 𝑥𝑖−1 ] of 𝑝, 𝑞 ∈ Q[𝑥1 , . . . , 𝑥𝑖 ] is a polynomial
whose roots are exactly the points 𝑡 ∈ R𝑖−1 where 𝑝(𝑡, 𝑥𝑖 ) ∈ R[𝑥𝑖 ] and 𝑞(𝑡, 𝑥𝑖 ) ∈ R[𝑥𝑖 ]
have a common root. If the resultant is order-invariant, then the roots of 𝑝 and 𝑞 do not
cross. This way, the boundaries are protected.

Figure 1 illustrates an example with a given sample 𝑠 ∈ R2 and polynomials 𝑃 = {𝑝1 , 𝑝2 , 𝑝3 } ⊂
Q[𝑥1 , 𝑥2 ]. For 𝑗 ∈ {1, 2, 3}, the line labeled with 𝑝𝑗 shows those points 𝑟 ∈ R2 with 𝑝𝑗 (𝑟) = 0. We
start at level 2, where 𝑃2 = 𝑃 . Fixing 𝑥1 to 𝑠1 and isolating the real roots of 𝑃2 yields one root of 𝑝2
below 𝑠2 and one root of each polynomial above 𝑠2 . The IREs corresponding to the roots closest to 𝑠2
define the symbolic interval 𝐼2 = (root𝑥2 [𝑝2 , 1](𝑥1 ) < 𝑥2 < root𝑥2 [𝑝3 , 1](𝑥1 )), as shown in Figure 1a.
Now, we need to ensure that this interval is correct for all values of 𝑥1 in the underlying cell which will
be computed at level 1. We choose 𝜉1 ⪯ 𝜉2 , 𝜉2 ⪯ 𝜉3 and 𝜉2 ⪯ 𝜉4 , and add thus the resultants of 𝑝3 with
𝑝1 and 𝑝2 , whose roots are given by the dashed lines in Figure 1b. On level 1, we again isolate those
roots and use the closest to 𝑠1 as interval boundaries, giving 𝐼1 = (𝜉1′ < 𝑥1 < 𝜉2′ ) and thus, (𝐼1 , 𝐼2 )
define the shaded area shown in Figure 1c. Note that the crossing of 𝜉3 and 𝜉4 over 𝐼1 is irrelevant, and
the corresponding resultant of 𝑝1 and 𝑝2 was avoided.

𝑥2 𝑝 𝑥2 𝑝 𝑥2 𝑝
1 𝜉4 1 𝜉4 1

𝑝2 𝜉3 𝑝2 𝜉3 𝑝2
𝜉2 𝜉2
𝑠 𝐼2 𝑆
𝑠
𝑝3 𝜉1 𝑝3 𝜉1 𝑝3 𝜉1′ 𝑠1 𝜉2′ 𝜉3′
𝑥1 𝑥1 𝑥1
𝐼1 𝐼1 𝐼1
(a) (b) (c)
Figure 1: Illustration of the levelwise single cell construction.
3. Under-Approximation with Low-Degree Polynomials
The most resource-intensive part of single cell construction is the computation of resultants and
discriminants, and we tackle the former. The computational effort and the degree of res𝑥𝑖 [𝑝, 𝑞] scales
with 𝑑𝑒𝑔(𝑝) · 𝑑𝑒𝑔(𝑞). Thus, if 𝑝 and 𝑞 have high degree, then not only is their resultant more expensive
to compute, but it also yields a polynomial of even higher degree which will be involved in resultants
in the subsequent levels. On the other hand, if 𝑝 is of the form 𝑥𝑖 − 𝑎, then its resultant with 𝑞 is simply
equal to 𝑞(𝑥1 , . . . , 𝑥𝑖−1 , 𝑎).
As seen in the example, one can choose the relation ⪯ so that all resultants in the current projection
take one of the boundary-defining polynomials as input. In [3], this is called the Biggest-Cell heuristic.
Our idea is to dynamically add artificial cell boundaries defined by linear polynomials and use that
heuristic so that the required resultants will be easy to calculate.
When computing the interval 𝐼𝑖 , if the upper (or lower) bound
of the interval would be defined by a high-degree polynomial, we
insert an “artificial” root 𝑟* between the sample 𝑠𝑖 and the actual 𝑝1
𝜉3 𝜉4
bound. This root is generalized to an IRE 𝜉 defined by a low-degree
*

polynomial, e.g. ℎ(𝑥𝑖 ) = 𝑥𝑖 − 𝑟* , and now we use 𝜉 * as the upper 𝑝2 𝜉2
interval bound. 𝑥 2

Figure 2 illustrates our idea. Interestingly, while we under- ℎ 𝜉*
approximate the symbolic interval 𝐼2 , the resulting cell is not a subset 𝑠
of the cell in Figure 1, because 𝐼1 is now defined by the resultants 𝑝3 𝜉1
of ℎ with 𝑝2 and 𝑝3 . This means that our approximated interval can 𝑥1
lead to larger underlying cells.
Our modification has two main benefits: the following projection Figure 2: Approximated cell
step is much easier to compute; and it is easier for NLSAT to check using an additional linear
whether a sample lies in the excluded cell, due to a less complex cell polynomial.
description that avoids algebraic number computations.

Correctness The approximation does not affect the correctness of the construction. To see this,
consider the original construction, but for a modified input 𝑃 ∪ 𝐻, where 𝐻 contains the approximation
polynomials that were dynamically added. This will yield the same cell as our version gives for the
input 𝑃 , and by the correctness of the original method, this cell contains 𝑠 and all polynomials in 𝑃 ∪ 𝐻
(in particular those in 𝑃 ) are sign-invariant over it.

Incompleteness When used in NLSAT, the approximation can lead to an incomplete (non-
terminating) algorithm, because the union of the approximated cells might converge to the inclusion-
maximal cell without ever covering it entirely and thus without ever considering the entire solution
space. This behavior can be circumvented by allowing NLSAT to only approximate a limited number of
cells before resorting to the original construction, which assures completeness.

4. Conclusions
Many SMT problems can be solved efficiently using approximative methods, like incremental lineariza-
tion [5] or ICP [6], though they are incomplete. We presented an approach that weaves dynamically
into the complete NLSAT method.

Experiments The levelwise SCC and a prototype of our modification are implemented as backends
for an NLSAT-style algorithm in the SMT-RAT solver [7, 8], and we conducted first experiments with
promising results. We obtained the best performance when applying linear approximations to cell
boundaries that are defined by a polynomial with degree 5 or higher, and not approximating after 50
calls to the SCC. When executed on the QF_NRA benchmark set from SMT-LIB [9], our modification
solved 44 instances more than the original version. When using the approximation, the solver needs
more calls to the SCC on average, but these calls are processed faster, leading to a lower mean runtime.

Next Steps We are currently working on different generalizations of our idea. Firstly, one can use
more intricate approximations, e.g. piecewise linear functions or Taylor polynomials, which hopefully
results in a cell that is more similar to the original one, but which also induces a larger overhead. In the
case of Taylor polynomials, a closer approximation could be obtained by using degree two or three,
instead of linear polynomials.
Secondly, the levelwise framework also allows us to add artificial roots between any two root functions,
not just as a cell boundary. In our example, we could have inserted 𝜉 * (and ℎ) between 𝜉2 and 𝜉3 . With
an appropriate choice of ⪯, this lets us replace res𝑥2 [𝑝3 , 𝑝1 ] by the less complex resultants res𝑥2 [𝑝3 , ℎ]
and res𝑥2 [ℎ, 𝑝1 ], while maintaining the original interval 𝐼2 = (𝜉1 < 𝑥2 < 𝜉2 ). This might still lead to
smaller intervals at the lower levels, due to the new resultants.
Finally, we are interested in transferring our ideas to the cylindrical algebraic coverings method [10],
which also uses the framework of the levelwise method.

Acknowledgments
Jasper Nalbach and Valentin Promies were supported by the Deutsche Forschungsgemeinschaft (DFG,
German Research Association) as part of AB 461/9-1 SMT-ART. Jasper Nalbach was supported by the
DFG RTG 2236 UnRAVeL.

References
[1] D. Jovanovic, L. M. de Moura, Solving non-linear arithmetic, in: Proc. of the 6th Int. Joint
Conf. on Automated Reasoning (IJCAR’12), volume 7364 of LNCS, Springer, 2012, pp. 339–354.
doi:10.1007/978-3-642-31365-3_27.
[2] G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition,
in: H. Barkhage (Ed.), Automata Theory and Formal Languages, 2nd GI Conference, Kaiserslautern,
May 20-23, 1975, volume 33 of Lecture Notes in Computer Science, Springer, 1975, pp. 134–183.
doi:10.1007/3-540-07407-4_17.
[3] J. Nalbach, E. Ábrahám, P. Specht, C. W. Brown, J. H. Davenport, M. England, Levelwise construc-
tion of a single cylindrical algebraic cell, Journal of Symbolic Computation 123 (2024) 102288.
doi:10.1016/j.jsc.2023.102288.
[4] C. W. Brown, M. Košta, Constructing a single cell in cylindrical algebraic decomposition, J. Symb.
Comput. 70 (2015) 14–48. doi:10.1016/J.JSC.2014.09.024.
[5] A. Cimatti, A. Griggio, A. Irfan, M. Roveri, R. Sebastiani, Invariant checking of NRA transition
systems via incremental reduction to LRA with EUF, CoRR abs/1801.08718 (2018). URL: http:
//arxiv.org/abs/1801.08718. arXiv:1801.08718.
[6] P. Van Hentenryck, D. McAllester, D. Kapur, Solving polynomial systems using a branch
and prune approach, SIAM Journal on Numerical Analysis 34 (1997) 797–827. doi:10.1137/
S0036142995281504.
[7] 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: Proc. of the 18th Int. Conf. on Theory and
Applications of Satisfiability Testing (SAT’15), volume 9340 of LNCS, Springer, 2015, pp. 360–368.
doi:10.1007/978-3-319-24318-4_26.
[8] SMT-RAT, a toolbox for strategic and parallel satisfiability modulo theories solving, https://github.
com/ths-rwth/smtrat, accessed 2024-06-01.
[9] C. Barrett, A. Stump, C. Tinelli, The SMT-LIB standard – version 2.0, in: Proc. of the 8th Int.
Workshop on Satisfiability Modulo Theories (SMT ’10), 2010. URL: http://theory.stanford.edu/
~barrett/pubs/BST10.pdf.
[10] E. Ábrahám, J. H. Davenport, M. England, G. Kremer, Deciding the consistency of non-linear real
arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, J. Log.
Algebraic Methods Program. 119 (2021) 100633. doi:10.1016/J.JLAMP.2020.100633.