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.