Satisfiability Modulo Transcendental Functions via Incremental Linearization
Alessandro Cimatti Alberto Griggio Ahmed Irfan Marco Roveri Roberto Sebastiani
cs.LO








































fmpage[1]
#1














































































































 

⌈⌉
⌊⌋


















Fondazione Bruno Kessler, Italy,

@fbk.eu,

DISI, University of Trento, Italy,

@unitn.it




Satisfiability Modulo Transcendental Functions
via Incremental Linearization
This work was funded in part by the H2020-FETOPEN-2016-2017-CSA project SC^2 (712689). We thank James Davenport and Erika
Abraham for useful discussions.





    
Alessandro Cimatti1Alberto Griggio1 Ahmed Irfan1,2 
 Marco Roveri1 Roberto Sebastiani2
    
============================================================================================================================================================================================================================================











In this paper we present an abstraction-refinement approach to Satisfiability Modulo the
theory of


transcendental functions, such as exponentiation and
trigonometric functions. The transcendental functions are represented
as uninterpreted in the abstract space,

which is described in terms of the combined theory of
linear arithmetic on the rationals with uninterpreted functions,

and are
incrementally axiomatized by means of
upper- and lower-bounding
piecewise-linear functions.

Suitable numerical techniques are used to ensure that the abstractions
of the transcendental functions are sound

even in presence of irrationals.

Our experimental evaluation on benchmarks from verification and
mathematics demonstrates the potential of our approach, showing that
it compares favorably with
delta-satisfiability
/interval
propagation and methods based on theorem proving.




§ INTRODUCTION






Many applications require dealing 

with transcendental functions (e.g.,
exponential, logarithm, sine, cosine). Nevertheless, the problem of
Satisfiability Modulo the theory of 

transcendental functions comes
with many difficulties. First, the problem is in general
undecidable <cit.>. Second, we may be
forced to deal with irrational numbers - in fact, differently from
polynomial, transcendental functions most often have irrational values for
rational arguments. (See, for example, Hermite's proof that exp(x) is
irrational for rational non-zero x.)
 


In this paper, we describe a novel approach to Satisfiability
Modulo the quantifier-free theory of 
(nonlinear arithmetic with)
transcendental
functions over the reals - 

SMT().

The approach is based on an abstraction-refinement loop, using
SMT() as abstract space, being the 
combined theory of 
linear arithmetic on the rationals with uninterpreted functions. The Uninterpreted Functions are used
to model nonlinear and transcendental functions. Then, we iteratively
incrementally axiomatize the transcendental functions with a
lemma-on-demand approach.

Specifically, we eliminate spurious interpretations in SMT() by
tightening the piecewise-linear envelope around the (uninterpreted
counterpart of) the transcendental functions.

A key challenge is to compute provably correct approximations, also in
presence of irrational numbers. 




We use Taylor series to exactly compute
suitable accurate rational coefficients.


We remark that nonlinear polynomials are only used to numerically
compute the coefficients –i.e., no SMT solving in the
  theory of nonlinear arithmetic (SMT())  is
  needed–  whereas the refinement is based on the


addition, in the abstract space, of piecewise-linear axiom
instantiations, which upper- and lower-bound the candidate solutions, 
ruling out spurious interpretations. 
To compute such piecewise-linear bounding functions,


the concavity of the curve is taken into account.


For example, 



in order to rule out a
spurious interpretation x=2.0,fexp(x)=3.0 (where fexp(x) is the
abstraction of the exponential function) we may
exploit the positive concavity of exp(x) and obtain
a linear lower-bound constraint,
e.g. fexp(x) > 155/21 + 331/45*(x - 2). 

[



Notice that exp(2.0) ≊ 7.389,
155/21≊ 7.381⪅ exp(2.0), and
331/45≊ 7,356⪅exp(2.0)x. 
These values are such that the above linear constraint “approximates” the
tangent of exp(x) in x=2, 
since it always lower-bounds 
exp(x) and its value and derivative are very near to those of
exp(x) for x=2.0.
Recall that exp(x)x=exp(x).
]







In order to deal with trigonometric functions, we take into account
the periodicity, so that the axiomatization is only done in the
interval between -π and π. Interestingly, not only this is 
helpful for efficiency, but also it is required to ensure correctness.



Another distinguishing feature of our approach is a logical method to
conclude the existence of a solution without explicitly constructing
it.
We use a sufficient criterion that consists in 
checking whether the formula is satisfiable 
under all possible interpretations 
of the uninterpreted functions (representing the transcendental functions)
that are consistent with some rational interval bounds within which
the correct values for the transcendental functions are guaranteed to exist.
We encode the problem as a SMT() satisfiability check,
such that an unsatisfiable result implies the satisfiability of the original SMT() formula.













We implemented the approach on top of the SMT
solver <cit.>, using the library <cit.>.

We experimented with benchmarks from SMT-based
verification queries over nonlinear transition systems, including
Bounded Model Checking of hybrid automata, as well as from several
mathematical properties from the  <cit.> suite and from other competitor solver distributions.

We contrasted our approach with state-of-the-art approaches based on
interval propagation (and ), and with the deductive
approach in .




The results show that our solver compares favourably with the other solvers,
being able to decide the highest number of benchmarks.







This paper is organized as follows.

In sec:background we describe some background.

In sec:approach we overview the approach, defining the foundation for safe linear approximations.

In sec:cegar-transcendental we describe the specific axiomatization for transcendental functions.

In sec:related-work we discuss the related literature,

and in sec:experiments we present the experimental evaluation.

In sec:conclusion we draw some conclusions and outline directions for future work.



§ BACKGROUND



We assume the standard first-order quantifier-free logical setting and
standard notions of theory, satisfiability, and logical consequence.
As usual in SMT, we denote with the theory of linear real arithmetic,
with that of non-linear real arithmetic,
with the theory of equality (with uninterpreted functions),
and with the combined theory of and .
Unless otherwise specified, we use the terms variable and free constant interchangeably.
We denote formulas with φ, ψ, terms with t,
variables with x, y, a, b,
functions with f, ,, each possibly with subscripts.


If x and y are two variables, we denote with φxy
the formula obtained by replacing all the occurrences of x in φ with y.
We extend this notation to ordered sequences of variables in the natural way.

If μ is a model and x is a variable, we write μ[x] to denote the value of x in μ,
and we extend this notation to terms and formulas in the usual way.

If Γ is a set of formulas,
we write ⋀Γ to denote the formula obtained by taking the conjunction of all its elements.

We write t_1 < t_2 < t_3 for t_1 < t_2 ∧ t_2 < t_3.





A transcendental function is an analytic function that does not
satisfy a polynomial equation
(in contrast to an algebraic function <cit.>).






Within this paper we consider univariate
exponential, logarithmic, and trigonometric functions.
We denote with the theory of (non-linear) real arithmetic extended with
these transcendental functions.













A tangent line to a univariate function f(x) at a point of interest x=a is a
straight line that “just touches” the function at the point, and represents the instantaneous rate of change of the function f at that one point.


The tangent line fa(x) to the function f at point a is the straight line defined as follows:



    fa(x)  f(a) + fx(a)*(x - a)


where fx is the first-order derivative of f wrt. x.

A secant line to a univariate function f(x) is a straight line that connects two
points on the function plot.
The secant line fab(x) to a function
f between points a and b is defined as follows:



    fab(x) f(a) - f(b)/a - b*(x - a) + f(a).



For a function f that is twice differentiable at point c,
the concavity of f at c is the sign of its second derivative
evaluated at c.

We denote open and closed intervals between two real numbers l and u as ]l, u[ and [l, u] respectively.
Given a univariate function f over the reals,
the graph of f is the set of pairs {x,f(x) | x ∈ℝ}.
We might sometimes refer to an element x,f(x) of the graph as a point.



  
Taylor Series and Taylor's Theorem.
Given a function f(x) that has n+1 continuous derivatives at
x=a, the Taylor series of degree n centered around a is the polynomial:


    nf(a)(x) ∑_i=0^nf^(i)(a)/i! * (x - a)^i

where f^(i)(a) is the evaluation of i-th derivative of f(x) at
point x=a. The Taylor series centered around 0 is also called
Maclaurin series.



According to Taylor's theorem, any continuous function f(x) that
is n+1 differentiable can be written as the sum of the Taylor series and
the remainder term:


    f(x) = nf(a)(x) + n+1f(a)(x)

where n+1f(a)(x) is basically the Lagrange form of the
remainder, and for some point b between x and a it is given by:


    n+1f(a)(x) f^(n+1)(b)/(n+1)!*(x-a)^n+1.


The value of the point b is not known, but the upper bound on the
size of the remainder n+1f(a)(x) at a point x can be
estimated by:


    n+1f(a)(x) max_c ∈ [min(a, x), max(a, x)](|f^(n+1)(c)|) * |(x-a)^n+1|/(n+1)!.




This allows to obtain two polynomials
that are above and below the function at a given point x, by considering
nf(a)(x) + n+1f(a)(x) and
nf(a)(x) - n+1f(a)(x) respectively.





§ OVERVIEW OF THE APPROACH



pseudocodecounter

 


























Our procedure, which extends to SMT() and pushes further the approach
 presented in <cit.> for SMT(),
works  by overapproximating the input formula with a
formula over the combined theory of linear arithmetic and
uninterpreted functions.


The main algorithm is shown in Fig. <ref>.
The solving procedure follows a classic abstraction-refinement loop,
in which at each iteration, the current safe approximation φ of the
input SMT() formula φ is refined by adding new
constraints Γ that rule out one (or possibly more) spurious solutions,
until one of the following conditions occurs:

[(i)]


  * the resource budget (e.g. time, memory, number of iterations) is
  exhausted; or

  * φ⋀Γ becomes unsatisfiable in SMT();
  or


  * the SMT() satisfiability result for φ⋀Γ can be lifted to a satisfiability result for the
  original formula φ.




An initial current precision is set (calling the function ),
and this value is possibly increased at each iteration (calling )
according to the result of and some heuristic.

In Fig. <ref> we distinguish between two different refinement procedures:

[1)]


  * , which is described below;


  * , which is  described in sec:cegar-transcendental, where we provide further details on the treatment
  of each specific transcendental function that we currently support.




  §.§.§ Initial Abstraction.


The function takes in input an SMT() formula
φ and returns a SMT() safe approximation
φ of it.

First, we flatten each transcendental function application t
in φ in which t is not a variable
by replacing t with a fresh variable y, and by
conjoining y = t to φ.

Then, we replace each transcendental function x
in φ with a corresponding uninterpreted function x,
producing thus an SMT() formula φ.

Finally, we add to φ
some simple initial axioms for the different transcendental
functions, expressing general, simple mathematical properties about them.
We shall describe such axioms in sec:cegar-transcendental.



If φ contains also non-linear polynomials,
we handle them as described in <cit.>:

we replace each non-linear product t_1*t_2 with an uninterpreted function application t_1, t_2,
and add to the input formula some initial axioms










expressing general, simple mathematical properties of
multiplications. (We refer the reader to  <cit.> for details.)




  §.§.§ Spuriousness check and abstraction refinement.






The core of our procedure is the  function,
shown in Fig. <ref>.

First, 
if the formula contains also some non-linear polynomials,
performs the refinement of non-linear multiplications
as described in <cit.>.
In Fig. <ref>, this is represented by the call to
the function at line <ref>,
which may return some axioms to further constrain  terms.

If no non-linear polynomials occur in φ, then Γ is
initialized as the empty set.


Then, the function iterates over all the transcendental function
applications x in φ (lines
<ref>–<ref>), and checks whether the
SMT()-model μ is consistent with their semantics.


Intuitively, in principle, this amounts to check that μ[x] is equal to μ[x].

In practice, however, the check cannot be exact,
since transcendental functions at rational points typically have irrational values (see e.g. <cit.>),
which cannot be represented in SMT().

Therefore, for each x in φ, we instead compute two polynomials,
P_l(x) and P_u(x), with the property that μ[x]


belongs to the open interval ]P_l(μ[x]), P_u(μ[x])[.
The polynomials are computed using Taylor series,
according to the given current precision, by the function ,
which shall be described in sec:cegar-transcendental.

If the model value μ[x] for x is outside the above interval,
then the function is used to generate some linear lemmas
that will remove the spurious point μ[x], μ[x]
from the graph of the current abstraction of x (line <ref>).

If at least one point was refined in the loop of lines <ref>–<ref>,
the current set of lemmas Γ is returned (line <ref>).

If instead none of the points was determined to be spurious,
the function is called (line <ref>).
This function tries to determine whether the abstract model μ
does indeed imply the existence of a model for the original formula φ
(more details are given below).

If the check fails, we repeat the call with an increased precision (line <ref>).




  §.§.§ Refining a spurious point with secant and tangent lines.






Given a transcendental function application x,
the function generates a set of lemmas for refining the interpretation of x
by constructing a piecewise-linear approximation of x around the point μ[x],
using one of the polynomials P_l(x) and P_u(x) computed in .
The kind of lemmas generated, and which of the two polynomials is used,
depend on
[(i)]

  * the position of the spurious value μ[x] relative to the correct value μ[x], and

  * the concavity of  around the point μ[x].

If the concavity is positive (resp. negative) or equal to zero, and the point lies below (resp. above) the function,
then the linear approximation is given by a tangent
to the lower (resp. upper) bound polynomial P_l (resp. P_u)
at μ[x] (lines <ref>–<ref> of Fig. <ref>);
otherwise, i.e. the concavity is negative (resp. positive)
and the point is below (resp. above) the function,
the linear approximation is given by a pair of secants
to the lower (resp. upper) bound polynomial P_l (resp. P_u)
around μ[x] (lines <ref>–<ref> of Fig. <ref>).

The two situations are illustrated in Fig. <ref>.

In the case of tangent refinement, the function (line <ref>)
returns an interval [l, u] such that the tangent line is guaranteed not to cross the transcendental function .
In practice, this interval can be (under)approximated quickly by exploiting
known properties of the specific function  under consideration.
For example, for the exponential function always returns [-∞, +∞];
for other functions, the computation can be based e.g. on an analysis of the
(known, precomputed) inflection points of 
around the point of interest μ[x]
and the slope Px(c) of the tangent line.

In the case of secant refinement,
a second value, different from μ[x],
is required to draw a secant line.
The function returns the set of all the points
at which a secant refinement was performed in the past for x.
From this set, we take the two points closest to μ[x], such that
l < μ[x] < u and that l,u do not cross any inflection point,
[For simplicity, we assume that this is always possible.
If needed, this can be implemented e.g. by generating
the two points at random while ensuring that l < μ[x] < u and that l,u do not cross any inflection point.]
and use those points to generate two secant lines and their validity intervals.
Before returning the set of the two corresponding lemmas, we also store
the new secant refinement point μ[x] by calling .



  §.§.§ Detecting satisfiable formulas.


The function tries to determine whether the -model
μ for φ⋀Γ
implies the satisfiability of the original formula φ.
If, for all x in φ,
 has a rational value at the rational point μ[x],
[Although, as mentioned above, this is not the case in general (see e.g. <cit.>),
it is true for some special values, e.g. exp(0) = 1, sin(0) = 0.]
and μ[x] is equal to μ[x],
then μ can be directly lifted to a model μ for φ.

In the general case, we exploit this simple observation:
we can still conclude that φ is satisfiable
if we are able to show that φ is satisfiable
under all possible interpretations of 
that are guaranteed to include also .

Using the model μ, we compute safe lower and upper bounds
μ[x] and μ[x]
for the function  at point μ[x]
with the function (see above).

Let FTF be the set of all x terms occurring in
φ.

Let V be the set of variables x for x∈ FTF,
and F be the set of all the function symbols in FTF.













Intuitively, if we can prove the validity of the following formula:

-

  
    ∀∈ F.
      (⋀_x∈ FTFμ[x]≤μ[x]≤μ[x]) →φVμ[V]


-

then the original formula φ is satisfiable.

In order to be able to use a quantifier-free SMT()-solver,
we reduce the problem to the validity check of a pure formula.

Let CT be the set of all terms μ[x] occurring in φVμ[V].
We replace each occurrence of μ[x] in CT
with a corresponding fresh variable y_μ[x] from a set Y.

We then check the validity of the formula:

-


    φ_μ^sat∀ Y.
      ((⋀_x∈ FTFμ[x]≤μ[x]≤μ[x])→φVμ[V])CTY.


-

If φ_μ^sat is unsatisfiable,
we conclude that φ is satisfiable.
Clearly, this can be checked with a quantifier-free
SMT()-solver, 

 since ∀ x.ϕ is equivalent to ∃ x.ϕ,
and x can then be removed by Skolemization.




§ ABSTRACTION REFINEMENT FOR TRANSCENDENTAL FUNCTIONS



In this section, we describe the implementation of the
and for the transcendental functions that we currently support,
namely exp and sin.
[We remark that our tool (see <ref>) can handle also
log, cos, tan, arcsin, arccos, arctan by means of rewriting.
We leave as future work the possibility of handling such functions natively.
]











The (x, c, ϵ) function
uses the Maclaurin series of the corresponding transcendental function
and Taylor's theorem
to find the lower and upper polynomials.
Essentially, this is done by expanding the series
(and the remainder approximation)
up to a certain n,
until the desired precision ϵ
(i.e. the difference between the upper and lower polynomials evaluated at c)
is achieved.
Notice that, since
we can precisely evaluate the derivative of any order at 0
for both exp and sin,
[Because
  [(i)]
    
  * exp(0)=1, sin(0)=0, cos(0)=1,
    
  * exp^(i)(x) = exp(x) for all i, and
    
  * |sin^(i)(x)| is |cos(x)| if i is odd and |sin(x)| otherwise.
  ]
the computation of both the Maclaurin series and the remainder polynomial is always exact.


























  §.§.§ Exponential Function










  
Piecewise-Linear Refinement.
The polynomial nexp(0)(x) given by the Maclaurin
series behaves differently depending on the sign of x. For that
reason, distinguishes three cases for finding the polynomials P_l(x) and P_u(x):





  Case x = 0: since exp(0)=1, we have P_l(0) = P_u(0) = 1;

  Case x < 0: we have that nexp(0)(x) < exp(x)
  if n is odd, and nexp(0)(x) > exp(x) if n is even
  (where nexp(0)(x) = ∑_i=0^nx^i/i!);
  we therefore set P_l(x)=nexp(0)(x) and P_u(x) = n+1exp(0)(x) for a suitable n so that the required precision ϵ is met;

  Case x>0: we have that nexp(0)(x) < exp(x)
  and nexp(0)(x)*(1 - x^n+1/(n+1)!)^-1 > exp(x) when (1 - x^n+1/(n+1)!) > 0,
  therefore we set P_l(x) = nexp(0)(x) and P_u(x) = nexp(0)(x)*(1 - x^n+1/(n+1)!)^-1 for a suitable n.


Since the concavity of exp is always positive,
the tangent refinement will always give lower bounds for exp(x),
and the secant refinement will give upper bounds.
Moreover, as exp has no inflection points, always returns [-∞,+∞].























  
Extra Refinement.


The exponential function is monotonically increasing with a non-linear order.
We check this property between two x and y terms in φ:
if μ[x] < μ[y],
but μ[x] ≮μ[y],
then we add the following extra refinement lemma:

x < y ↔x < y









  
Initial Axioms.
We add the following initial axioms to φ.

    Lower Bound:    x > 0
    Zero:     (x=0 ↔x = 1) ∧
                                     (x < 0 ↔x < 1) ∧
    
                                       (x > 0 ↔x > 1)
    Zero Tangent Line:     x=0 ∨x > x + 1















  §.§.§ Sin Function




  
Piecewise-Linear Refinement.

The correctness of our refinement procedure relies crucially on being able
to compute the concavity of the transcendental function  at a given point c.
This is needed in order to know whether a computed tangent or secant line
constitutes a valid upper or lower bound for  around c (see Fig. <ref>).

In the case of the sin function,
computing the concavity at an arbitrary point c is problematic,
since this essentially amounts to computing the remainder
of c and π, which,
being π a transcendental number, cannot be exactly computed.

In order to solve this problem,
we exploit another property of sin, namely its periodicity (with period 2π).




More precisely, we split the reasoning about sin
depending on two kinds of periods: base period and extended period.

A period is a base period for the sin function if it is from
-π to π, otherwise it is an extended period.
In order to reason about periods,
we first introduce a symbolic variable π,
and add the constraint l_π < π < u_π to φ,
where l_π and u_π are valid rational lower and upper bounds for the actual value of π
(in our current implementation, we have l_π = 333/106 and u_π = 355/113).

Then, we introduce for each x term an “artificial” sin
function application y_x (where y_x is a fresh variable),
 whose domain is the base period. This is done by adding the following
constraints:


(-π ≤y_x ≤π) ∧
((-π ≤x ≤π) →y_x = x) ∧
x = y_x.



We call these fresh variables base variables.


Notice that the second and the third constraint are saying
that x is the same as y_y in the base period.

Let Fsin_base be the set of y_x terms that have base variables
as arguments, Fsin be the set of all x terms,
and

Fsin_ext Fsin - Fsin_base.

The tangent and secant refinement is performed for the terms in Fsin_base,
while we add a linear shift lemma (described below)
as refinement for the terms in Fsin_ext.

Using this transformation, we can easily compute the concavity of sin at
μ[y_x] by just looking at the sign of μ[y_x],
provided that -l_π≤μ[y_x] ≤ l_π,
where l_π is the current lower bound for π.
[In the interval [-π, π], the concavity of sin(c) is the opposite of the sign of c.]

In the case in which -u_π < μ[y_x] < -l_π or l_π < μ[y_x] < u_π,
we do not perform the tangent/secant refinement,
but instead we refine the precision of π.

For each y_x∈ FSin_base, tries to find the
lower and upper polynomial using Taylor's theorem,
which ensures that:

  nsin(0)(y_x) -
  n+1sin(0)(y_x) ≤sin(y_x)
  ≤nsin(0)(y_x) +
  n+1sin(0)(y_x)

where
nsin(0)(y_x) = ∑_k=0^n (-1)^k * y_x^2k+1/(2k +1)!
and
n+1sin(0)(y_x) = y_x^2(n+1)/(2(n+1))!.
Therefore, we can set P_l(x) = nsin(0)(x) - n+1sin(0)(x)
and P_u(x) = nsin(0)(x) + n+1sin(0)(x).



  
Extra Refinement.

For each x∈ Fsin_ext
with the corresponding base variable y_x,
we check whether the value μ[x] after shifting to the base period
is equal to the value of μ[y_x].
We calculate the shift s of x as the rounding towards zero
of (μ[x]+μ[π])/(2·μ[π]), and
we then compare μ[y_x] with μ[x] - 2s·μ[π].
If the values are different, we add the following shift lemma
for relating x with y_x in the extended period s:








  (π * (2s - 1) ≤x ≤π * (2s + 1)) →y_x = x - 2s*π.


In this way, we do not need the tangent and secant refinement
for the extended period and we can reuse the refinements done in the
base period.

Note that even if the calculated shift value is wrong
(due to the imprecision of μ[π] with respect to the real value π),
we may generate something useless but never wrong.




We also check the monotonicity property of sin, which can be
described for the base period as: (i) the sin is monotonically
increasing in the interval -π/2 to π/2; (ii)
the sin is monotonically decreasing in the intervals -π to
-π/2 and π/2 to π.

We add one of the constraints below if it is in conflict according to
the current abstract model for some y_x_1,y_x_2∈
Fsin_base.









    (-π/2≤ y_x_1 < y_x_2≤π/2) → fsin(y_x_1) < fsin(y_x_2)
    
    (-π≤ y_x_1 < y_x_2≤ -π/2) → fsin(y_x_1) > fsin(y_x_2)
    
    (π/2≤ y_x_1 < y_x_2≤π) → fsin(y_x_1) > fsin(y_x_2)
















  
Initial Axioms.
For each z∈ Fsin, we add the generic lower and upper
bounds: -1 ≤z≤ 1.

For each y_x∈ Fsin_base, we add the following axioms.

    Symmetry:    y_x = - -y_x
    Phase:     (0 < y_x < π↔y_x > 0) ∧
                                 (-π < y_x < 0 ↔y_x < 0) 
    Zero Tangent:     (y_x > 0 →y_x < y_x) ∧
                                 (y_x < 0 →y_x > y_x)
    π Tangent:     (y_x < π→y_x < -y_x + π) ∧
    
                                   (y_x > -π→y_x > -y_x - π)
    Significant Values:     (y_x = 0 ↔ (y_x=0 ∨ y_x=π∨ y_x=-π)) ∧
        (y_x = 1 ↔ y_x=π/2) ∧
                                 (y_x = -1 ↔ y_x=-π/2) ∧
        (y_x = 1/2↔ (y_x=π/6∨ y_x=5*π/6)) ∧
        (y_x = -1/2↔ (y_x=-π/6∨ y_x=-5*π/6))













  §.§.§ Optimization
 We use infinite-precision to represent rational numbers.
In our (model-driven) approach,
we may have to deal with numbers with very large numerators and/or denominators.
It may happen that we get such rational numbers from the bad model μ for the variables
appearing as arguments of transcendental functions.
As a result of the piecewise-linear refinement,
we will feed to the SMT() solver
numbers that have even (exponentially) larger numerators and/or denominators
(due to the fact that uses power series).
This might significantly slow-down the performance of the solver.
We address this issue by
approximating “bad” values μ[x] with too large numerators and/or denominators



by using continued fractions <cit.>.
The precision of the rational approximation is increased periodically over the number of iterations.
Thus we delay the use numbers with larger numerator and/or denominator,
and eventually find those numbers if they are really needed.




§ RELATED WORK



The approach proposed in this paper is an extension of the approach
adopted in <cit.> for checking the invariants of transition
systems over the theory of polynomial Nonlinear Real
Arithmetic. 






In this paper we extend the approach to transcendental functions,
with the critical issue of irrational valuations.
Furthermore, we propose a way to prove
SAT without being forced to construct the model.

In the following,
we compare with 
related approaches found in the literature.












  §.§.§ Interval propagation and .


The first approach to SMT() was pioneered by
 <cit.>, that carries out
interval propagation for nonlinear and transcendental functions. is both an SMT solver and bounded model checker for transition
systems.

A subsequent but very closely related approach is the solver,
proposed in <cit.>.


relies on the notion of
delta-satisfiability <cit.>, which basically guarantees
that there exists a variant (within a user-specified δ “radius”) of the
original problem such that it is satisfiable.






The approach cannot guarantee that the original problem is satisfiable,
since it relies on numerical approximation techniques that only compute safe overapproximations of the solution space.







There are a few key insights that differentiate our approach. First,
it is based on linearization, it relies on solvers for SMT(),
and it proceeds by incrementally axiomatizing transcendental
functions.

Compared to interval propagation, we avoid numerical approximation
(even if within the bounds from ). In a sense, the precision
of the approximation is selectively detected at run time, while in
and this is a user defined threshold that is uniformly
adopted in the computations.

Second, our method relies on piecewise linear approximations, which
can provide substantial advantages when approximating a slope –
intuitively, interval propagation ends up computing a
piecewise-constant approximation.

Third, a distinguishing feature of our approach is the ability to
(sometimes) prove the existence of a solution even if the actual
values are irrationals, by reduction to an SMT-based validity check.













  §.§.§ Deductive Methods.






The  <cit.> theorem prover
relies on resolution and on a decision procedure for

to prove 
quantified
inequalities involving transcendental functions.

It works by replacing transcendental functions with
upper- or lower-bound functions specified by means of axioms
(corresponding to either truncated Taylor series or rational functions derived from continued fraction approximations),
and then using an external decision procedure for for solving the resulting formulas.
















Differently from our approach, cannot prove the existence nor compute a satisfying assignment, while
we are able to (sometimes) prove the existence of a solution even if
the actual values are irrationals.

Finally, we note that may require the user to
manually write axioms if the ones automatically selected from a predefined
library are not enough. Our approach is much simpler, and it is
completely automatic.



The approach presented in <cit.>, where
the theory is referred to as NLA, is similar in spirit to
in that it combines the SPASS theorem
prover <cit.> with the SMT
solver. The approach relies on the SUP(NLA) calculus that combines
superposition-based first-order logic reasoning with SMT().

Similarly to our work,
the authors also use a approximation of the original problem.
This is however done only as a first check before calling .











In contrast, we rely on solvers for
SMT(), and we proceed by incrementally axiomatizing
transcendental functions instead of calling directly an solver.

Another similarity with our work is the possibility of finding solutions in some cases.


This is done by post-processing
an inconclusive answer, trying to compute a certificate for a
(point) solution for the narrow intervals returned by the solver,
using an iterative analysis of the formula and of the computed intervals.
Although similar in spirit,
our technique for detecting satisfiable instances is completely different,
being based on a logical encoding of the existence of a solution as an SMT() problem.
























































  §.§.§ Combination of interval propagation and theorem proving.


 <cit.> is a standalone tool and a
tactic for the proof assistant, that can be used to prove
properties about numeric programs (C-like) dealing with floating-point
or fixed-point arithmetic. Another related tactic is 
 <cit.>. 
Both and combine interval propagation and Taylor approximations for handling transcendental functions. 
A similar approach is followed also in <cit.>, 
where a tool written in to handle conjunctions 
of non-linear equalities with transcendental functions is presented. 
The work uses Taylor polynomials up to degree two. 
 <cit.> is another related tool 
which uses interval propagation for handling transcendental functions.
It approximates polynomials with sums of squares 
and transcendental functions with lower and upper bounds using some quadratic polynomials <cit.>. 

Internally, all these tools/tactics rely on multi-precision
floating point libraries for computing the interval bounds.

A similarity between these approaches and our approach is the use of
the Taylor polynomials. 
However, one distinguishing feature is that we
use them to find lower and upper linear constraints by computing
tangent and secant lines. 
Moreover, 



we do not rely on any floating point arithmetic library, and 
unlike the mentioned approaches, we can also prove the existence of a solution.

On the other hand, some of the above tools employ more sophisticated/specialised approximations
for transcendental functions, 
which might allow them to succeed in proving unsatisfiability 
of formulas for which our technique is not sufficiently precise.


Finally, since we are in the context of SMT, our approach also has the benefits
of being:

[(i)]

  * fully automatic, unlike some of the above which are meant to be
  used within interactive theorem provers;

  * able to deal with formulas with an arbitrary Boolean structure,
  and not just conjunctions of inequalities; and

  * capable of handling combinations of theories (including
  uninterpreted functions, bit-vectors, arrays), which are beyond what
  the above, more specialised tools, can handle.






§ EXPERIMENTAL ANALYSIS





  §.§.§ Implementation.


The approach has been implemented on top of the SMT
solver <cit.>, using the library <cit.>.

We use the GMP infinite-precision arithmetic library to deal with
rational numbers.







Our implementation and benchmarks 
are available at <https://es.fbk.eu/people/irfan/papers/cade17-smt-nta.tar.gz>.




  §.§.§ Setup.


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

We have run in two configurations: with and without universal
check for proving SAT (resp. called and ).

The other systems used in the experimental evaluation are
 <cit.>,  <cit.>, and
 <cit.>, in their default configurations (unless
otherwise specified).














Both and were also run with higher precision than
the default one.

The difference between the two configurations is rather modest and,
when run with higher precision, they decrease the number of answers.


can prove the validity of quantified formulae, answering
either valid or unknown. As such, it is unfair to run it on
satisfiable benchmarks.








In general, we interpret the results of the comparison taking into
account the features of the tools.








  §.§.§ Benchmarks.


We consider three classes of benchmarks.

First, the bounded model checking (BMC) benchmarks are the results of
unrolling transition systems with nonlinear and transcendental
transition relations, obtained from the discretization of hybrid
automata.

We took benchmarks from the distributions of , from the discretization
(by way of  <cit.> and  <cit.>) of
benchmarks from <cit.> and from the hybrid model
checkers HyST <cit.> and Hare<cit.>.






Second, the Mathematical benchmarks are taken from the distribution. These are benchmarks containing quantified formulae over
transcendental functions, and are all valid, most of them
corresponding to 
known mathematical theorems.

We selected the benchmarks without quantifier alternation
and we translated them into quantifier-free SMT() problems.


The third class of benchmarks consists of 944 instances from the distribution
that contain transcendental functions.



Both the mathematical and the benchmarks
contain several transcendental functions (log, cos, ...)
that are not supported natively by our prototype.
We have therefore applied a preprocessing step that rewrites those functions in terms of exp and sin.
[Sometimes we used a relational encoding: e.g. if φ contains arcsin(x), we rewrite it as φarcsin(x)as_xsin(as_x) = x  -π/2≤ as_x ≤π/2, where as_x is a fresh variable.]

requires bounds on the variables and it is unable to
deal with the benchmarks above (that either do not specify any bound or specify too wide bounds for the used variables).

Thus, we scaled down the benchmarks so that the variables are constrained in the [-300,300] interval

since for higher bounds raises an exception due to reaching the
machine precision limit.

Finally, for the BMC benchmarks, we run in BMC mode,
in order to ensure that its optimized unrolling is activated.




  §.§.§ BMC and Mathematical Results.




In Table <ref>, we present the results.

The benchmarks are classified as either or when at least one
of the solvers has been able to return a definite answer.

If only answers are returned, then the benchmark
is classified as .


For each tool, we report the number of answers produced within the used resource limits.
For the benchmarks,
the numbers in parentheses indicate the instances which have been classified as /by at least one other tool.
For example, an entry “87 (32/7)” means that the tool returned for 87 instances,
of which 32 were classified as and 7 by some other tool.
[There was no case in which two tools reported and for the same benchmark.]



First, we notice that the universal SAT
technique directly results in 72 benchmarks proved to be
satisfiable by , without substantial degrade on the benchmarks.

Second, we notice that is very strong to deal with its own
mathematical benchmarks,

but is unable to deal with the BMC ones,
which contain features that are beyond what it can handle
(Boolean variables and tens of real variables).

[According to the documentation of , the tool is ineffective for problems with more than 10 real variables. Our experiments on a subset of the instances confirmed this.]
 
 
 
 
 









In the lower part of Table <ref>, we present the
results on the scaled-down benchmarks, so that can be run.

The results for and are consistent with the ones
obtained on the original benchmarks – the benchmarks are slightly
simplified for , that solves 12 more instances and 2 more ones,
and for , that solves 11 more instances.

The performance of is quite good, halfway between and
on the bounded model checking benchmarks, and slightly lower
than on the mathematical ones.

In the BMC benchmarks, is able to solve 35 and 470 instances, 102 more than and 135 less than .


The results need further analysis. We notice that both and often return on unsatisfiable benchmarks
(e.g. all the mathematical ones are ).

There are many cases where returns a result, but at
the same time it prints an error message stating that the
numerical precision limit has been reached. Thus, it is unlikely that the
result is actually , but it should rather be interpreted as in these cases.[We contacted the authors of and they reported that this issue is currently under investigation.]








  §.§.§ Benchmarks Results.


The benchmarks turn out to be very hard. The results are
reported in Table <ref>, where we show the
performance of both on the original benchmarks and on the ones
resulting from the removal via pre-processing of the transcendental
functions not directly supported by .





The results shows that in the original format solves many more
instances, and this suggests that dealing with other transcendental
functions in a native manner may lead to substantial improvement in
too.

Interestingly, if we

focus on the subset of 96 benchmarks that only contain exp and sin
(and are dealt by without the need of preprocessing),
we see that is significantly more effective than in
proving unsatisfiability, solving more than twice the number of instances
(right part of Table <ref>).








We conclude by noticing that overall solves 906 benchmarks
out of 2512, 127 more than , the best among the other systems. 





A deeper analysis of the results (not reported here for lack of space)
shows that the performance of the solvers is complementary: the
“virtual-best system” solves 1353 
benchmarks. This suggests that the integration of interval propagation
may yield further improvements.




  
*Performance
Where are the cactus plots?
The cactus plots (reported in the appendix) demonstrate that is slower on the easy (less than one second) benchmarks, due to a
substantial start-up of the Python runtime, but becomes significantly
faster as the benchmarks become harder, ultimately outperforming the
other solvers.[inline]still to be completed The scatter plots
demonstrate that our method dominates the other methods.

[inline]MAKE SURE WE ARE CONSISTENT WITH THE FOLLOWING STATEMENT FROM INTRO:
The results show that our solver is able to solve more benchmarks than
the others, and demonstrates better scalability on the harder
benchmarks.




§ CONCLUSION



We present a novel approach to Satisfiability Modulo the theory of
transcendental functions. The approach is based on an
abstraction-refinement loop, where transcendental functions are
represented as uninterpreted ones in the abstract space SMT(), and
are incrementally axiomatized by means of piecewise-linear functions.





We experimentally evaluated the approach on a large and heterogeneous
benchmark set: the results demonstrates the potential of our approach,
showing that it compares favorably with both delta-satisfiabily and
interval propagation and with methods based on theorem proving.

In the future we plan to exploit the solver for the verification of
infinite-state transition systems and hybrid automata with nonlinear
dynamics, and for the analysis of resource consumption in temporal
planning.

Finally we would like to define a unifying framework to compare
linearization and interval propagation, and to exploit the potential
synergies.


splncs03




