Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization

Abstract

Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

This work was funded in part by the H2020-FETOPEN-2016-2017-CSA project SC$^2$ (712689).

1 Introduction

The field of Satisfiability Modulo Theories (SMT) has seen tremendous progress in the last decade. Nowadays, powerful and effective SMT solvers are available for a number of quantifier-free theories¹ and their combinations, such as equality and uninterpreted functions (UF), bit-vectors (BV), arrays (AX), and linear arithmetic over the reals (LRA) and the integers (LIA). A fundamental challenge is to go beyond the linear case, by introducing nonlinear polynomials – theories of nonlinear arithmetic over the reals (NRA) and the integers (NIA). Although the expressive power of nonlinear arithmetic is required by many application domains, dealing with nonlinearity is a very hard challenge. Going from SMT(LRA) to SMT(NRA) yields a complexity gap that results in a computational barrier in practice – most available complete solvers rely on Cylindrical Algebraic Decomposition (CAD) techniques [8], which require double exponential time in worst case. Adding integrality constraints exacerbates the problem even further, because reasoning on NIA has been shown to be undecidable [16].

Recently, we have proposed a conceptually simple, yet effective approach for dealing with the quantifier-free theory of nonlinear arithmetic over the reals, called Incremental Linearization [4,5,6]. Its underlying idea is that of trading the use of expensive, exact solvers for nonlinear arithmetic for an abstraction-refinement loop on top of much less expensive solvers for linear arithmetic and uninterpreted functions. The approach is based on an abstraction-refinement loop that uses SMT(UFLRA) as abstract domain. The uninterpreted functions are used to model nonlinear multiplications, which are incrementally axiomatized, by means of linear constraints, with a lemma-on-demand approach.

In this paper, we show how incremental linearization can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas, performed within the MathSAT [7] SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all NIA benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

Related Work. Several SMT solvers supporting nonlinear integer arithmetic (e.g., Z3 [10], smt-rat [9]) rely on the bit-blasting approach [12], in which a nonlinear integer satisfiability problem is iteratively reduced to a SAT problem by first bounding the integer variables, and then encoding the resulting problem into SAT. If the SAT problem is unsatisfiable then the bounds on the integer variables are increased, and the process is repeated. This approach is geared towards finding models, and it cannot prove unsatisfiability unless the problem is bounded.

In [3], the SMT(NIA) problem is approached by reducing it to SMT(LIA) via linearization. The linearization is performed by doing case analysis on the variables appearing in nonlinear monomials. Like the bit-blasting approach, the method aims at detecting satisfiable instances. If the domain of the problem is bounded, the method generates an equisatisfiable linear SMT formula. Otherwise, it solves a bounded problem and incrementally increases the bounds of some (heuristically chosen) variables until it finds a solution to the linear problem. In some cases, it may also detect (based on some heuristic) the unsatisfiability of the original problem.

The CVC4 [1] SMT solver uses a hybrid approach, in which a variant of incremental linearization (as presented in [5, 17]) is combined with bit-blasting.

Recent works presented in [13] and [15] have considered a method that combines solving techniques for SMT(NRA) with branch and bound. The main idea is to relax the NIA problem by interpreting the variables over the reals, and apply NRA techniques for solving it. Since the relaxed problem is an over-approximation of the original problem, the unsatisfiability of the NIA problem is implied by the unsatisfiability of the NRA problem. If the NRA-solver finds a non-integral solution a to a variable x, then a lemma $(x \le \lfloor a\rfloor \vee x \ge \lceil a \rceil )$ is added to the NRA problem. Otherwise, an integral solution is found for the NIA problem. In [13], the Cylindrical Algebraic Decomposition (CAD) procedure (as presented in [14]) is combined with branch and bound in the MCSAT framework. This is the method used by the Yices [11] SMT solver. In [15], the authors show how to combine CAD and virtual substitution with the branch-and-bound method in the DPLL(T) framework.

Contributions. Compared to our previous works on incremental linearization [4,5,6], we make the following contributions. First, we give a significantly more detailed description of our implementation (in the SMT solver MathSAT), showing pseudo-code for all its major components. Second, we evaluate the approach over NIA problems, both by comparing it with the state of the art, and by evaluating the contributions of various components/heuristics of our procedure to its overall performance.

Structure of the Paper. This paper is organized as follows. In § we provide some background on the ideas of incremental linearization. In § we describe our implementation in detail. In § we present our experimental evaluation. Finally, in § we draw some conclusions and outline directions for future work.

2 Background

We assume the standard first-order quantifier-free logical setting and standard notions of theory, satisfiability, and logical consequence.

Fig. 1.

Axioms of the multiplication function.

We denote with $\mathbb {Z}$ the set of integer numbers. A monomial in variables $v_1,v_2,\ldots ,v_n$ is a product $v_1^{\alpha _1}*v_2^{\alpha _2}*\ldots * v_n^{\alpha _n}$, where each $\alpha _i$ is a non-negative integer called exponent of the variable $v_i$. When clear from context, we may omit the multiplication symbol $*$ and simply write $v_1^{\alpha _1}v_2^{\alpha _2}\ldots v_n^{\alpha _n}$. A polynomial p is a finite linear combination of monomials with coefficients in $\mathbb {Z}$, i.e., where each $c_i \in \mathbb {Z}$ and each $m_i$ is a monomial. A polynomial constraint or simply constraint P is of the form $p \bowtie 0$ where p is a polynomial and $\bowtie {}\in \{<, \le , >, \ge \}$.²

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories. Most SMT solvers are based on the lazy/DPLL(T) approach [2], where a SAT solver is tightly integrated with a T-solver, that is demanded to decide the satisfiability of a list of constraints (treated as a conjunction of constraints) in the theory T. There exist several theories that the modern SMT solvers support. In this work we are interested in the following theories: Equality and Uninterpreted Functions (UF), Linear Arithmetic and Nonlinear Arithmetic over the integers (LIA and NIA, resp.), and in their combinations thereof.

We denote formulas with $\varphi$, lists of constraints with $\phi$, terms with t, variables with v, constants with a, b, c, monomials with w, x, y, z, polynomials with p, functions with f, each possibly with subscripts. If $\mu$ is a model and v is a variable, we write $\mu [v]$ to denote the value of v in $\mu$, and we extend this notation to terms and formulas in the usual way. If $\phi$ is a list of constraints, we write $\bigwedge \phi$ to denote the formula obtained by taking the conjunction of all its elements.

We call a monomial m a toplevel monomial in a polynomial if $m = m_j$ for $0 \le j \le n$. Similarly, a monomial m is a toplevel monomial in $\varphi$ if there exists a polynomial p in $\varphi$ such that m is a toplevel monomial in p. Given $\varphi$, we denote with $\widehat{\varphi }$ the formula obtained by replacing every nonlinear multiplication between two monomials $x*y$ occurring in $\varphi$ by a binary uninterpreted function $f_{*}(x,y)$.

We assume that the polynomials in $\varphi$ are normalized by applying the distributivity property of multiplication over addition, and by sorting both the monomials and the variables in each monomial using a total order (e.g. lexicographic). Moreover, we always rewrite negated polynomial constraints into negation-free polynomial constraints by pushing the negation to the arithmetic relation (e.g., we write $\lnot (p \le 0)$ as $(p > 0)$).

Overview of Incremental Linearization. The main idea of incremental linearization is to trade the use of expensive, exact solvers for nonlinear arithmetic for an abstraction-refinement loop on top of much less expensive solvers for linear arithmetic and uninterpreted functions. First, the input SMT(NIA) formula $\varphi$ is abstracted to the SMT(UFLIA) formula $\widehat{\varphi }$ (called its UFLIA-abstraction). Then the loop begins by checking the satisfiability of $\widehat{\varphi }$. If the SMT(UFLIA) check returns false then the input formula is unsatisfiable. Otherwise, the model ${\mu }$ for $\widehat{\varphi }$ is used to build an UFLIA underapproximation $\widehat{\varphi }^*$ of $\varphi$, with the aim of finding a model for the original NIA formula $\varphi$. If the SMT check for $\widehat{\varphi }^*$ is satisfiable, then $\varphi$ is also satisfiable. Otherwise, a conjunction of linear lemmas that is sufficient to rule out the spurious model $\mu$ is added to $\widehat{\varphi }$, thus improving the precision of the abstraction, and another iteration of the loop is performed. The lemmas added are instances of the axioms of Fig. 1 obtained by replacing the free variables with terms occurring in $\varphi$, selected among those that evaluate to false under the current spurious model $\mu$.

Fig. 2.

The top-level NIA theory solver procedure.

3 Implementing Incremental Linearization in a Lazy SMT Solver

We now describe in detail our implementation of the basic incremental linearization ideas as a theory solver inside an SMT prover based on the lazy/DPLL(T) approach. The pseudo-code for the toplevel algorithm is shown in Fig. 2. The algorithm takes as input a list of constraints $\phi$, corresponding to the NIA constraints in the partial assignment that is being explored by the SAT search, and it returns a result consisting of a status flag plus some additional information that needs to be sent back to the SAT solver. If the status is true, then $\phi$ is satisfiable, and a model $\mu$ for it is also returned. If the status is false, then $\phi$ is unsatisfiable, and a conflict set $\phi ' \subseteq \phi$ (serving as an explanation for the inconsistency of $\phi$) is also returned. If the status is undef, the satisfiability of $\phi$ cannot be determined yet. In this case, the returned result contains also a set of lemmas to be used by the SAT solver to refine its search (i.e. those lemmas are learnt by the SAT solver, and the search is resumed). Finally, a status of unknown means that the theory solver can neither determine the satisfiability of $\phi$ nor generate additional lemmas³; in this case, the search is aborted.

Fig. 3.

Recursive model evaluation.

Fig. 4.

Searching for a model via linearization.

Fig. 5.

Main lemma generation procedure.

check-nia starts by invoking a theory solver for UFLIA on the abstract version $\widehat{\phi }$ of the input problem (lines 1–4), in which all nonlinear multiplications are treated as uninterpreted functions. The unsatisfiability of $\widehat{\phi }$ immediately implies that $\phi$ is inconsistent. Otherwise, the UFLIA solver generates a model $\mu$ for $\widehat{\phi }$. $\mu$ is then used (lines 5–9) to determine the set of nonlinear multiplications that need to be refined. This is done by collecting all nonlinear multiplication terms $x*y$ which have a wrong value in $\mu$; that is, for which the value of the abstraction $\widehat{x*y}$ is different from the value obtained by fully evaluating the multiplication under $\mu$ (using the eval-model function shown in Fig. 3). It is important to observe that here we can limit the search for multiplications to refine only to those that appear in constraints that evaluate to false under $\mu$ (line 6). In fact, if all the constraints evaluate to true, then by definition $\mu$ is a model for them, and we can immediately conclude that $\phi$ is satisfiable (line 10).

Even when $\mu$ is spurious, it can still be the case that there exists a model for $\phi$ that is “close” to $\mu$. This is the idea behind the check-sat procedure of Fig. 4, which uses $\mu$ as a guide in the search for a model of $\phi$. check-sat works by building an UFLIA-underapproximation of $\phi$, in which all multiplications are forced to be linear. The resulting formula $\widehat{\varphi }$ can then be solved with an SMT solver for UFLIA. Although clearly incomplete, this procedure is cheap (since the Boolean structure of $\widehat{\varphi }$ is very simple) and, as our experiments will show, surprisingly effective.

When check-sat fails, we proceed to the generation of lemmas for refining the spurious model $\mu$ (lines 15–21). Our lemma generation strategy works in three rounds: we invoke the generate-lemmas function (Fig. 5) on the multiplication terms $x*y$ that need to be refined using increasing levels of effort, stopping at the earliest successful round – i.e., a round in which lemmas are generated. In the first round, only basic lemmas encoding simple properties of multiplications (sign, zero, neutral, proportionality in Fig. 1) are considered (generate-basic-lemmas). In the second round, we consider also “order” lemmas (generate-order-lemmas, Fig. 6), i.e. lemmas obtained via (a restricted, model-driven) application of the order axioms of $\mathbb {Z}$. If generate-order-lemmas fails, we proceed to generating monotonicity (generate-monotonicity-lemmas, Fig. 7) and tangent plane (generate-tangent-lemmas, Fig. 8) lemmas, restricting the instantiation however to only toplevel monomials. Finally, in the last round, we repeat the generation of monotonicity and tangent lemmas, considering this time also non-toplevel monomials.

Fig. 6.

Generation of order lemmas.

Lemma Generation Procedures. We now describe our lemma generation procedures in detail. The pseudo-code is reported in Figs. 5, 6, 7 and 8. All procedures share the following two properties: (i) the lemmas generated do not contain any nonlinear multiplication term that was not in the input constraints $\phi$; and (ii) all the generated lemmas evaluate to false ($\bot$) in the current model $\mu$.

The function generate-basic-lemmas, whose pseudo-code is not reported, simply instantiates all the basic axioms for the input term $x*y$ that satisfy points (i) and (ii) above.

The function generate-order-lemmas (Fig. 6) uses the current model and asserted constraints to produce lemmas that are instances of the order axiom for multiplication. It is based on ideas that were first implemented in the CVC4 [1] SMT solver.⁴ It works by combining, for each variable v in the input term $x*y$, the monomials $t*v$ in which v occurs (retrieved by get-monomials) with the predicates of the form $(w * v \bowtie p)$ (where $\bowtie {}\in \{ <, >, \le , \ge \}$ and p is a polynomial) that are induced by constraints in $\phi$ (which are collected by the get-bounds function). The (non-constant) coefficient t of v in the monomial $t * v$ is used to generate the terms $t * w * v$ and $t * p$: if both occur⁵ in the input constraints $\phi$, then an instance of the order axiom is produced, using the current model $\mu$ as a guide (lines 7–15).

Fig. 7.

Generation of monotonicity lemmas.

The function generate-monotonicity-lemmas (Fig. 7) returns instances of monotonicity axioms relating the current input term $x*y$ with other monomials that occur in the set of terms to refine. In the second round of lemma generation, only toplevel monomials are considered.

Finally, the function generate-tangent-lemmas (Fig. 8) produces instances of the tangent plane axioms. In essence, the function instantiates all the clauses of the tangent plane lemma using the two factors x and y of the input multiplication term $x*y$ and their respective values a and b in $\mu$, returning all the instances that are falsified by $\mu$. This is done in lines 15–21 of Fig. 8. In our actual implementation, however, we do not use the model values a and b directly to generate tangent lemmas, but we instead use a heuristic that tries to reduce the number of tangent lemmas generated for each $x*y$ term to refine. More specifically, we keep a 4-value tuple $\langle l_x, l_y, u_x, u_y\rangle$ associated with each $x*y$ term in the input problem (which we call frontier) consisting of the smallest and largest of the previous model values for x and y for which a tangent lemma has been generated, and for each frontier we maintain an invariant that whenever x is in the interval $[l_x , u_x ]$ or y is in the interval $[l_y , u_y ]$, then $x*y$ has both an upper and a lower bound. This condition is achieved by adding tangent lemmas for the following four points of each frontier: $(l_x, l_y), (l_x, u_y), (u_x, l_y), (u_x, u_y)$ (the function update-tangent-frontier in Fig. 8 generates those lemmas). If the current model values a and b for x and y are outside the intervals $[l_x, u_x]$ and $[l_y, u_y]$ respectively, we try to adjust them with the goal of enlarging the frontier as much as possible whenever we generate a tangent plane. Intuitively, this can be seen as a form of lemma generalisation. The procedure is shown in lines 6–14 of Fig. 8: the various push-tangent-point* functions try to move the input points along the specified directions (either ‘U’p, by increasing a value, or ‘D’own, by decreasing it) as long as the tangent plane passing through (a, b) still separates the multiplication curve from the spurious value c.⁶

Fig. 8.

Generation of tangent lemmas.

Fig. 9.

Illustration of the strategy for adjusting the refinement point for the tangent lemma.

Example 1

(Tangent frontier enlargement – Fig. 9). Let $\langle -3, -1, 5, 2\rangle$ be the current frontier of $x*y$ during the search. Suppose the abstract model gives: $\mu [x] = a = 15$, $\mu [y] = b = 5$, and $\mu [\widehat{x*y}] = c = 48$. This model is spurious because $15*5 \ne 48$. Notice that the point (15, 5) is outside of the frontier, because 15 is not in $[-3,5]$ and 5 is not in $[-1,2]$. So, during the tangent lemmas generation, the function push-tangent-points-UU can return $a = 20$ and $b = 10$, as one of the constraints of the tangent lemma instantiated at that point is violated by the current model, i.e., we can obtain the following clauses from the tangent lemma:

$$\begin{aligned} x> 20 \wedge y< 10 \rightarrow x*y< 10*x + 20*y - 200\\ x< 20 \wedge y> 10 \rightarrow x*y< 10*x + 20*y - 200\\ x< 20 \wedge y < 10 \rightarrow x*y> 10*x + 20*y - 200\\ x> 20 \wedge y> 10 \rightarrow x*y > 10*x + 20*y - 200 \end{aligned}$$

by plugging in the values $x = 15$, $y=5$, and $x*y=48$, then we obtain a conflict in the third clause because $15 < 20$ and $5 < 10$, but $48 \not > 10*15 + 20*5 - 200$. This means that the tangent lemma instantiated at point (20, 10) can be used for refinement (Fig. 9(c)).

However, if we use (21, 11) for the tangent lemma instantiation, we get the following clauses:

$$\begin{aligned} x> 21 \wedge y< 11 \rightarrow x*y< 11*x + 21*y - 231\\ x< 21 \wedge y> 11 \rightarrow x*y< 11*x + 21*y - 231\\ x< 21 \wedge y < 11 \rightarrow x*y> 11*x + 21*y - 231\\ x> 21 \wedge y> 11 \rightarrow x*y > 11*x + 21*y - 231 \end{aligned}$$

Notice that, all these clauses are satisfied if we plug in the values $x = 15$, $y=5$, and $x*y=48$. Therefore, we cannot use them for refinement (Fig. 9(d)).

4 Experimental Analysis

We have implemented our incremental linearization procedure in our SMT solver MathSAT [7]. In this section, we experimentally evaluate its performance. Our implementation and experimental data are available at https://es.fbk.eu/people/irfan/papers/sat18-data.tar.gz.

Setup and Benchmarks. We have run our experiments on a cluster equipped with 2.6 GHz Intel Xeon X5650 machines, using a time limit of 1000 s and a memory limit of 6 Gb.

For our evaluation, we have used all the benchmarks in the QF_NIA category of SMT-LIB [18], which at the present time consists of 23876 instances. All the problems are available from the SMT-LIB website.

Our evaluation is composed of two parts. In the first, we evaluate the contribution of different parts of our procedure to the overall performance of MathSAT, by comparing different configurations of the solver. In the second part, we compare our best configuration against the state of the art in SMT solving for nonlinear integer arithmetic.

Fig. 10.

Comparison among different configurations of MathSAT.

Comparison of Different Configurations. We evaluate the impact of the main components of our procedure, by comparing five different configurations of MathSAT:

• The standard configuration, using all the components described in the previous section (simply denoted MathSAT);

• a configuration with check-sat disabled (denoted MathSAT-no-check-sat);

• a configuration with generate-order-lemmas disabled (denoted MathSAT-no-order);

• a configuration with generate-monotonicity-lemmas disabled (denoted MathSAT-no-mono);

• a configuration with generate-tangent-lemmas disabled (denoted MathSAT-no-tangent); and finally

• a configuration with both check-sat and generate-tangent-lemmas disabled (denoted MathSAT-no-check-sat-no-tangent).

The results are presented in Fig. 10. The plot on the left shows, for each configuration, the number of instances that could be solved (on the y axis) within the given time limit (on the x axis). The table on the right shows the ranking of the configurations according to the number of instances solved. From Fig. 10, we can see that all components of our procedure contribute to the performance of MathSAT. As expected, tangent lemmas are crucial, but it is also interesting to observe that the cheap satisfiability check by linearization is very effective, leading to an overall performance boost and to the successful solution of 746 additional benchmarks that could not be solved by MathSAT-no-check-sat. Finally, although the addition of order axioms (by generate-order-lemmas) does not pay off for simpler problems, its impact is clearly visible for harder instances, allowing MathSAT to solve 338 more benchmarks than MathSAT-no-order.

Comparison with the State of the Art. In the second part of our experiments, we compare MathSAT with the state-of-the-art SMT solvers for NIA. We consider CVC4 [1], smt-rat [9], Yices [11] and Z3 [10]. Figures 11 and 12 show a summary of the results (with separate plots for satisfiable and unsatisfiable instances in addition to the overall plot), whereas Fig. 13 shows a more detailed comparison between MathSAT and Yices. Additional information about the solved instances for each benchmark family is given in Table 1. From the results, we can see that the performance of MathSAT is very competitive: not only it solves more instances than all the other tools, but it is also faster than CVC4, smt-rat and Z3. On the other hand, Yices is much faster than MathSAT in the majority of cases, especially on easy unsatisfiable instances (solved in less than 10 s). However, the two tools are very complementary, as shown by Fig. 13: MathSAT can solve 2436 instances for which Yices times out, whereas Yices can successfully handle 1505 instances that MathSAT is unable to solve. Moreover, MathSAT overall solves 931 more problems (915 satisfiable and 16 unsatisfiable) than Yices in the given resource limits.

Fig. 11.

Comparison with state-of-the-art SMT solvers for NIA.

Fig. 12.

Comparison with state-of-the-art SMT solvers for NIA – without the VeryMax benchmarks.

Fig. 13.

Detailed comparison between MathSAT and Yices.

Table 1. Summary of the comparison with the state of the art.

5 Conclusions

We have presented a solver for satisfiability modulo nonlinear integer arithmetic based on the incremental linearization approach. Our empirical analysis of its performance over all the nonlinear integer benchmarks in the SMT-LIB library shows that the approach is very competitive with the state of the art: our solver MathSAT can solve many problems that are out of reach for other tools, and overall it solves the highest number of instances. Our evaluation has however also shown that current approaches for SMT(NIA) are very complementary, with no tool that always outperforms all the others. This suggests the investigation of hybrid approaches that combine multiple methods as a very promising direction for future work.