Introduction

The NLSAT algorithm [1] is a modern and complete approach for deciding the satisfiability of quantifierfree 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.

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 )). 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)

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.

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 , . . . ,= (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.

𝑥 1 𝑥 2 𝑝 2 𝑝 3 𝑝 1 𝜉 1 𝜉 2 𝜉 3 𝜉 4 𝑠 𝐼 2 𝐼 1 (a) 𝑥 1 𝑥 2 𝑝 2 𝑝 3 𝑝 1 𝜉 1 𝜉 2 𝜉 3 𝜉 4 𝑠 𝐼 1 (b) 𝑥 1 𝑥 2 𝑆 𝑝 2 𝑝 3 𝑝 1 𝑠 1 𝜉 ′ 1 𝜉 ′ 2 𝜉 ′ 3 𝐼 1 (c)

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 bound. This root is generalized to an IRE 𝜉 * defined by a low-degree polynomial, e.g. ℎ(𝑥 𝑖 ) = 𝑥 𝑖 − 𝑟 * , and now we use 𝜉 * as the upper interval bound.

𝑥 1 𝑥 2 𝑝 2 𝑝 3 𝑝 1 ℎ 𝜉 1 𝜉 2 𝜉 3 𝜉 4 𝜉 * 𝑠

Figure 2 illustrates our idea. Interestingly, while we underapproximate 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 of ℎ with 𝑝 2 and 𝑝 3 . This means that our approximated interval can lead to larger underlying cells.

Our modification has two main benefits: the following projection step is much easier to compute; and it is easier for NLSAT to check whether a sample lies in the excluded cell, due to a less complex cell 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 (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.

Conclusions

Many SMT problems can be solved efficiently using approximative methods, like incremental linearization [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.