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 efort of resultant computations, while maintaining the signinvariance properties of the cell. Although one must be careful to ensure termination, first experiments suggest that this modification pays of in the context of SMT solving.
Originally, Nalbach et al. [
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)).
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 coeficients 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. The most resource-intensive part of single cell construction is the computation of resultants and discriminants, and we tackle the former. The computational efort 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 [
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 afect 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 (nonterminating) algorithm, because the union of the approximated cells might converge to the inclusionmaximal 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.
Many SMT problems can be solved eficiently using approximative methods, like incremental
linearization [
Experiments The levelwise SCC and a prototype of our modification are implemented as backends
for an NLSAT-style algorithm in the SMT-RAT solver [
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 res2 [3, 1] by the less complex resultants res2 [3, ℎ] and res2 [ℎ, 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.
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. [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.