Keywords

1 Introduction

SMT solvers are used as back-end engines for a wide variety of academic and industrial applications [2, 19, 20]. Efficient reasoning in the theory of real arithmetic is crucial for many such applications [5, 8]. While modern SMT solvers have been shown to be quite effective at reasoning about linear real arithmetic problems [21, 43], nonlinear problems are typically much more difficult. This is not surprising, given that the worst-case complexity for deciding the satisfiability of nonlinear real arithmetic formulas is doubly-exponential in the number of variables in the formula [15]. Nevertheless, a variety of techniques have been proposed and implemented, each attempting to target a class of formulas for which reasonable performance can be observed in practice.

Related Work. All complete decision procedures for nonlinear real arithmetic (or the theory of the reals) originate in computer algebra, the most prominent being cylindrical algebraic decomposition (CAD) [11]. While alternatives exist [6, 25, 41], they have not seen much use [27], and CAD-based methods are the only sound and complete methods in practical use today. CAD-based methods used in modern SMT solvers include incremental CAD implementations [34, 36] and cylindrical algebraic coverings [3], both of which are integrated in the traditional CDCL(T) framework for SMT [40].

In contrast, the NLSAT [30] calculus and the generalized MCSAT [28, 39] framework provide for a much tighter integration of a conflict-driven CAD-based theory solver into a theory-aware core solver. This has been the dominant approach over the last decade due to its strong performance in practice. However, it has the significant disadvantage of being difficult to integrate with CDCL(T)-based frameworks for theory combination.

A number of incomplete techniques are also used by various SMT solvers: incremental linearization [9] gradually refines an abstraction of the nonlinear formula obtained via a naive linearization by refuting spurious models of the abstraction; interval constraint propagation [24, 36, 45] employs interval arithmetic to narrow down the search space; subtropical satisfiability [22] provides sufficient linear conditions for nonlinear solutions in the exponent space of the polynomials; and virtual substitution [12, 31, 46] makes use of parametric solution formulas for polynomials of bounded degree. Though all of these techniques have limitations, each of them is useful for certain subclasses of nonlinear real arithmetic or in combination with other techniques.

Contributions. We present an integration of cylindrical algebraic coverings and incremental linearization, implemented in the cvc5 SMT solver. Crucial to the success of the integration is an abstraction-refinement loop used to combine the two techniques cooperatively. The solution is effective in practice, as witnessed by the fact that cvc5 won the nonlinear real arithmetic category of SMT-COMP 2021 [44], the first time a non-MCSAT-based technique has won since 2013. Our integrated technique also has the advantage of being very flexible: in particular, it fits into the regular CDCL(T) schema for theory solvers and theory combination, it supports (mixed) integer problems, and it can be easily extended using further subsolvers that support additional arithmetic operators beyond the scope of traditional algebraic routines (e.g., transcendental functions).

2 Nonlinear Solving Techniques

The nonlinear arithmetic solver implemented in cvc5 generally follows the abstraction-refinement framework introduced by Cimatti et al. [9] and depicted in Fig. 1. The input assertions are first checked by the linear arithmetic solver, where they are linearized implicitly by treating every application of multiplication as if it were an arithmetic variable. For example, given input assertions \(x \cdot y> 0\,\wedge \,x > 1 \wedge y < 0\), the linear solver treats the expression \(x \cdot y\) as a variable. It may then find the (spurious) model: \(x \mapsto 2\), \(y \mapsto -1\), and \(x \cdot y \mapsto 1\). We call the candidate model returned by the linear arithmetic solver, where applications of multiplication are treated as variables, a linear model. If a linear model does not exist, i.e., the input is unsatisfiable according to the linear solver, the linear solver generates a conflict that is immediately returned to the CDCL(T) engine.

Fig. 1.
figure 1

Structural overview of the nonlinear solver

Full size image

When a linear model does exist, we check whether it already satisfies the input assertions or try to repair it to do so. We only apply a few very simple heuristics for repairs such as updating the value for z in the presence of a constraint like \(z = x \cdot y\) based on the values of x and y.

If the model can not be repaired, we refine the abstraction for the linear solver [9]. This step constructs lemmas, or conflicts, based on the input assertions and the linear model, to advance the solving process by blocking either the current linear model or the current Boolean model, that is, the propositional assignment generated by the SMT solver’s SAT engine. The Boolean model is usually eliminated only by the coverings approach, while the incremental linearization technique generates lemmas with new literals that target the linear model, e.g., the lemma \(x > 0\,\wedge \,y< 0 \Rightarrow x \cdot y < 0\) in the example above. We next describe our implementation of cylindrical algebraic coverings and incremental linearization, and how they are combined in cvc5.

2.1 Cylindrical Algebraic Coverings

Cylindrical algebraic coverings is a technique recently proposed by Ábrahám et al. [3] and is heavily inspired by CAD. While the way the computation proceeds is very different from traditional CAD, and instead somewhat similar to NLSAT [30], their mathematical underpinnings are essentially identical. The cylindrical algebraic coverings subsolver in cvc5 closely follows the presentation in [3]. Below, we discuss some differences and extensions. For this discussion, we must refer the reader to [3] for the relevant background material because of space constraints. We note that cvc5 relies on the libpoly library [29] to provide most of the computational infrastructure for algebraic reasoning.

Square-Free Basis. As with most CAD projection schemas, the set of projection polynomials needs to be a square-free basis when computing the characterization for an interval in [3, Algorithm 4]. However, the resultants computed in this algorithm combine polynomials from different sets, which are not necessarily coprime. The remedy is to either make these sets of polynomials pairwise square-free or to fully factor all projection polynomials. We adopt the former approach.

Starting Model. Although the linear model may not satisfy the nonlinear constraints, we may expect it to be in the vicinity of a proper model. We thus optionally use the linear model as an initial assignment for the cylindrical algebraic coverings algorithm in one of two ways: either using it initially in the search and discarding it as soon as it conflicts; or using it whenever possible, even if it leads to a conflict in another branch of the search. Unfortunately, neither technique has any discernible impact in our experiments.

Interval Pruning. As already noted in [3], a covering may contain two kinds of redundant intervals: intervals fully contained in another interval, or intervals contained in the union of other intervals. Removing the former kind of redundancies is not only clearly beneficial, but also required for how the characterizations are computed. It is not clear, however, if it is worthwhile to remove redundancies of the second kind because, while it can simplify the characterization locally, it may also make the resulting interval smaller, slowing down the overall solving process. Note that there may not be a unique redundant interval: e.g., if multiple intervals overlap, it may be possible to remove one of two intervals, but not both of them. We have implemented a simple heuristic to detect redundancies of the second kind, always removing the smallest interval with respect to the interval ordering given in [3]. Even if these redundancies occur in about \(7.5\%\) of all QF_NRA benchmarks, using this technique has only a very limited impact. It may be that for certain kinds of benchmarks, underrepresented in SMT-LIB, the technique is valuable. Or it may be that some variation of the technique is more broadly helpful. These are interesting directions for future work.

Lifting and Coefficient Selection with Lazard. The original cylindrical algebraic coverings technique is based on McCallum’s projection operator [37], which is particularly well-studied, but also (refutationally) unsound: polynomial nullification may occur when computing the real roots, possibly leading to the loss of real roots and thus solution candidates. One then needs to check for these cases and fall back to a more conservative, albeit more costly, projection schema such as those due to Collins [11] or Hong [26].

Lazard’s projection schema [35], which has been proven correct only recently [38], provides very small projection sets and is both sound and complete. This comes at the price of a different mathematical background and a modified lifting procedure, which corresponds to a modified procedure for real root isolation. Although the local projections employed in cylindrical algebraic coverings have not been formally verified for Lazard’s projection schema yet, we expect no significant issues there. Adopting it seems to be a logical improvement, as already mentioned in [3]. The modified real root isolation procedure is a significant hurdle in practice, as it requires additional nontrivial algorithms [32, Section 5.3.2]. We implemented it using CoCoALib [1] in cvc5 [33], achieving soundness without any discernible negative performance impact.

Using Lazard’s projection schema, for all its benefits, may seem questionable for the following reasons: (i) the unsoundness of McCallum’s projection operator is virtually never witnessed in practice [32, 33, Section 6.5], and (ii) the projection sets computed by Lazard’s and McCallums’s projection operator are identical on more than 99.5% on all of QF_NRA [33]. We argue, though, that working in the domain of formal verification warrants the effort of obtaining a (provably) correct result, especially if it does not incur a performance overhead.

Proof Generation. Recently, generating formal proofs to certify the result of SMT solvers has become an area of focus. In particular, there is a large and ongoing effort to produce proofs in cvc5. The incremental linearization approach can be seen as an oracle which produces lemmas that are easy to prove individually, so cvc5 does generate proofs for them; the complex part is finding those lemmas and making sure they actually help the solver make progress.

The situation is very different for cylindrical algebraic coverings: the produced lemma is the infeasible subset, and we usually have no simpler proof than the computations relying on CAD theory. That said, cylindrical algebraic coverings appear to be more amenable to automatic proof generation than traditional CAD-based approaches [4, 14]. In fact, although making these proofs detailed enough for automated verification is still an open problem, they are already broken into smaller parts that closely follow the tree-shaped computation of the algorithm. This allows cvc5 to produce at least a proof skeleton in that case.

2.2 Incremental Linearization

Our theory solver for nonlinear (real) arithmetic optionally uses lemma schemas following the incremental linearization approaches described by Cimatti et al. [9] and Reynolds et al. [42]. These schemas incrementally refine candidate models from the linear arithmetic solver by introducing selected quantifier-free lemmas that express properties of multiplication, such as signedness (e.g., \(x>0 \wedge y> 0 \Rightarrow x \cdot y> 0\)) or monotonicity (e.g., \(|x|> |y| \Rightarrow x \cdot x > y \cdot y\)). They are generated as needed to refute spurious models that violate these properties.

Most lemma schemas built-in in cvc5 are crafted so as to avoid introducing new monomial terms or coefficients, since that could lead to non-termination in the CDCL(T) search. As a notable exception, we rely on a lemma schema for tangent planes for multiplication [9], which can be used to refute the candidate model for any application of the multiplication operator \(\cdot \) whose value in the linear model is inconsistent with the standard interpretation of \(\cdot \). Note that since these lemmas depend upon the current model value chosen for arithmetic variables, tangent plane lemmas may introduce an unbounded number of new literals into the search. The set of lemma schemas used by the solver is user-configurable, as described in the following section.

2.3 Strategy

The overall theory solver for nonlinear arithmetic is built from several subsolvers, implementing the techniques described above, using a rather naive strategy, as summarized in Algorithm 1. After a spurious linear model has been constructed that cannot be repaired, we first apply a subset of the lemma schemas that do not introduce an unbounded number of new terms (with procedure IncLinearizationLight); then, we continue with the remaining lemma schemas (with procedure IncLinearizationFull); finally, we resort to the coverings solver which is guaranteed to find either a conflict or a model. Internally, each procedure sequentially tries its assigned lemma schemas from [9, 42] until it constructs a lemma that can block the spurious model.

figure a

The approach is dynamically configured based on input options and the logic of the input formula. For example, by default, we disable IncLinearizationFull for QF_NRA as it tends to diverge in cases where the coverings solver quickly terminates.

2.4 Beyond QF_NRA

The presented solver primarily targets quantifier-free nonlinear real arithmetic, but is used also in the presence of quantifiers and with multiple theories.

Quantified Logics. Solving quantified logics for nonlinear arithmetic requires solving quantifier-free subproblems, and thus any improvement to quantifier-free solving also benefits solving with quantifiers. In practice, however, the instantiation heuristics are just as important for overall solver performance.

Multiple Theories. The theory combination framework as implemented in cvc5 requires evaluating equalities over the combined model. To support this functionality, real algebraic numbers had to be properly integrated into the entire solver; in particular, the ability to compute with these numbers could not be local to the cylindrical algebraic coverings module or even the nonlinear solver.

3 Experimental Results

We evaluate our implementation within cvc5 (commit id 449dd7e) in comparison with other SMT solvers on all 11552 benchmarks in the quantifier-free nonlinear real arithmetic (QF_NRA) logic of SMT-LIB. We consider three configurations of cvc5, each of which runs a subset of steps from Algorithm 1. All the configurations run lines 2–4. In addition, cvc5.cov runs line 7, cvc5.inclin runs lines 5 and 6, and cvc5 runs lines 5 and 7. All experiments were conducted on Intel Xeon E5-2637v4 CPUs with a time limit of 20 min and 8 GB memory.

We compare cvc5 with recent versions of all other SMT solvers that participated in the QF_NRA logic of SMT-COMP 2021 [44]: MathSAT 5.6.6 [10], SMT-RAT 19.10.560 [13], veriT [7] (veriT+raSAT+Redlog), Yices2 2.6.4 [18] (Yices-QS for quantified logics), and z3 4.8.14 [16]. MathSAT employs an abstraction-refinement mechanism very similar to the one described in Sect. 2.2; veriT [23] forwards nonlinear arithmetic problems to the external tools raSAT [45], which uses interval constraint propagation, and Redlog/Reduce [17], which focuses on virtual substitution and cylindrical algebraic decomposition; SMT-RAT, Yices2, and z3 all implement some variant of MCSAT [30]. Note that SMT-RAT also implements the cylindrical algebraic coverings approach, but it is less effective than SMT-RAT’s adaptation of MCSAT [3].

Fig. 2.
figure 2

(a) Experiments for QF_NRA (b) Experiments for NRA and QF_UFNRA

Full size image

Figure a shows that cvc5 significantly outperforms all other QF_NRA solvers. Both the coverings approach (cvc5.cov) and the incremental linearization approach (cvc5.inclin) contribute substantially to the overall performance of the unified solver in cvc5, with coverings solving many satisfiable instances, and incremental linearization helping on unsatisfiable ones. Even though cvc5.inclin closely follows [9], it outperforms MathSAT on unsatisfiable benchmarks, those where cvc5 relies on incremental linearization the most.

Comparing cvc5 and Yices2 is particularly interesting, as the coverings approach in cvc5 and the NLSAT solver in Yices2 both rely on libpoly [29], thus using the same implementation of algebraic numbers and operations over them. Our integration of incremental linearization and algebraic coverings is compatible with the traditional CDCL(T) framework and outperforms the alternative NLSAT approach, which is specially tailored to nonlinear real arithmetic.

Going beyond QF_NRA, we also evaluate the performance of our solver in the context of theory combination (with all 37 benchmarks from QF_UFNRA) and quantifiers (with all 4058 benchmarks from NRA). There, cvc5 is a close runner-up to Yices2 and z3, thanks to the coverings subsolver which significantly improves cvc5 ’s performance. We conjecture that the remaining gap is due to components other than the nonlinear arithmetic solver, such as the solver for equality and uninterpreted functions, details of theory combination, or quantifier instantiation heuristics. Interestingly, the sets of unsolved instances in NRA are almost disjoint for cvc5.cov, Yices2 and z3, indicating that each tool could solve the remaining benchmarks with reasonable extra effort.

4 Conclusion

We have presented an approach for solving quantifier-free nonlinear real arithmetic problems that combines previous approaches based on incremental linearization [9] and cylindrical algebraic coverings [3] into one coherent abstraction-refinement loop. The resulting implementation is very effective, outperforming other state-of-the-art solver implementations, and integrates seamlessly in the CDCL(T) framework.

The general approach also applies to integer problems, quantified formulas, and instances with multiple theories, and can additionally be used in combination with transcendental functions [9] and bitwise conjunction for integers [47]. Further evaluations of these combinations are left to future work.