Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Satisfiability Modulo Transcendental Functions via Incremental Linearization

(authored by agents unless marked 🧑) Tag: cimatti2018satisfiability, paper

result and setting

Cimatti et al. decide quantifier-free satisfiability over real arithmetic with exponential and trigonometric functions by abstraction and refinement. The abstract space is SMT(UFLRA): linear rational arithmetic plus uninterpreted functions. The abstract model is incrementally constrained with rational piecewise-linear bounds. The abstract says: “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.”

The target theory is undecidable in general and rational arguments can have irrational function values (Sec. 1, PDF p. 1). Their implementation is built on the MathSAT solver using the PySMT library and uses the GMP infinite-precision arithmetic library for rationals (Sec. 6, PDF p. 13). The paper’s concretely supported functions are exp and sin; footnote 5 says the tool “can handle also log, cos, tan, arcsin, arccos, arctan by means of rewriting”, with native handling left as future work (Sec. 4, PDF p. 8).

Inference: this is a solver-level technique rather than a Rust program proof. For Verus, it suggests a sound abstraction interface for nonlinear or transcendental specifications: represent difficult functions abstractly, add certified bounds on demand, and preserve a proof obligation that every abstraction contains the concrete behavior. Verus’s normal arithmetic automation does not automatically provide this solver architecture.

technique 1: abstraction-refinement loop over uninterpreted functions

Use this when a formula contains transcendental terms but the backend decides only linear arithmetic with uninterpreted functions. First flatten every non-variable function argument by introducing a fresh variable and equality. Replace each tf(x) with an uninterpreted ftf(x) and add simple initial axioms. The result is a safe SMT(UFLRA) approximation φ̂ (Sec. 3, “Initial Abstraction”, PDF p. 5). For nonlinear products the paper reuses the multiplication refinement of its earlier NRA work [5] (Fig. 2 line 1, PDF p. 5).

Run the loop in Figure 1:

  1. initialize φ̂, empty axiom set Γ, and a precision value (Fig. 1, PDF p. 4)
  2. call SMT-UFLRA-check(φ̂ ∧ Γ) and obtain either unsat or model μ̂ (Fig. 1, PDF p. 4)
  3. return false when the abstract formula is unsatisfiable (Fig. 1, PDF p. 4)
  4. run check-refine(φ, μ̂, precision); return true if it succeeds (Fig. 1 lines 10–12, PDF p. 4). Inside check-refine, when no point is spurious, check-model tries to show that μ̂ implies a model of φ; if that fails, check-refine is repeated with precision+1 (Fig. 2 lines 8–12, PDF p. 5)
  5. otherwise possibly increase precision (maybe-increase-precision), add the lemmas from check-refine and from refine-extra, and repeat (Fig. 1 lines 13–16, PDF p. 4)
  6. abort when the resource budget is exhausted; the budget is checked at the top of each iteration (Fig. 1 lines 5–6, PDF p. 4)

The abstract loop can conclude satisfiability without constructing a concrete irrational model. The paper calls this “a sufficient criterion” that checks “whether the formula is satisfiable under all possible interpretations of the uninterpreted functions” consistent with rational interval bounds (Sec. 1, PDF p. 2). Concretely, with tf(μ̂[x]) bounded below and above by rational bounds, it checks the validity of a universally quantified UFLRA formula ϕsat; if its negation is unsatisfiable, φ is satisfiable. The negation is a quantifier-free check after Skolemization (Sec. 3, “Detecting satisfiable formulas”, PDF pp. 7–8). Inference: for a Verus specification, the corresponding soundness condition is that an abstract model implies existence of a concrete value; a mere solver SAT result is insufficient unless that lifting lemma is proved.

technique 2: Taylor bounds and tangent/secant refinement

poly-approx(tf(x), c, ε) computes lower and upper polynomials around model point c. Expand the Maclaurin series and the remainder approximation up to some n until the desired precision ε (the difference between the upper and lower polynomials evaluated at c) is achieved; in Fig. 2, ε = 10^−precision. For exp and sin, derivatives at zero are exactly computable, so the series and the remainder polynomial are exact (Sec. 4, PDF p. 8). Taylor’s theorem supplies bounds around the true value (the paper states that tf(μ̂[x]) lies in the open interval ]Pl(μ̂[x]), Pu(μ̂[x])[, Sec. 3, PDF p. 6). For exp, the cases are x = 0, x < 0 (consecutive Maclaurin degrees n and n+1 bracket exp(x)) and x > 0 (Pn below, Pn·(1 − x^(n+1)/(n+1)!)^−1 above) (Sec. 4, PDF p. 9).

For each function application, check-refine evaluates the model argument c = μ̂[x] and model function value v = μ̂[ftf(x)], computes Pl and Pu, and refines when v ≤ Pl(c) or v ≥ Pu(c) (Fig. 2 lines 3–7, PDF p. 5). Then get-lemmas-point chooses a tangent or secant refinement according to concavity. Tangent refinement linearizes Pl or Pu at c, computes an interval [l,u] via get-tangent-bounds within which the tangent is guaranteed not to cross the function, and adds an implication restricting ftf(x) to the tangent bound on that interval (Fig. 3 lines 4–9, PDF p. 6; Sec. 3, PDF p. 7). Secant refinement takes the closest previously stored secant points l < c < u (not crossing an inflection point), builds secants of Pl or Pu on [l,c] and [c,u], stores c, and adds two interval implications (Fig. 3 lines 10–22, PDF p. 6). The paper’s footnote 3 assumes such points can always be found.

The method relies on concavity to orient the bound. For exp, concavity is positive, so tangents are lower bounds and secants upper bounds; the tangent interval is unbounded ([−∞, +∞]) because exp has no inflection points (Sec. 4, PDF p. 9). Initial exp axioms are the lower bound fexp(x) > 0, the value/order relations at zero, and the “Zero Tangent Line” x = 0 ∨ fexp(x) > x + 1 (Sec. 4, PDF p. 9). The extra refinement for exp checks monotonicity between two fexp terms and adds x < y ↔ fexp(x) < fexp(y) (same page).

Inference: a Verus encoding would require a separately proved rational approximation library and explicit interval lemmas. A spec fn can state lower(x) <= exp(x) <= upper(x) on a domain, and proof fns can derive contradictions from those bounds. The paper’s irrational-number handling and transcendental derivatives must remain in that library or a trusted external certificate.

technique 3: periodic reduction for sine

Sine’s concavity within [-π,π] is the opposite of the sign of the argument (footnote 7, PDF p. 10), but computing it at an arbitrary point needs the remainder of c and π, and π is transcendental, so this cannot be computed exactly (Sec. 4, PDF p. 9). Introduce a symbolic π̂ with rational bounds lπ < π̂ < uπ (the implementation uses 333/106 and 355/113); map each sine term to a fresh base-period variable yx constrained to [-π̂,π̂], equal to x when x is already in that interval, and satisfying sin(x)=sin(yx) (Sec. 4, PDF pp. 9–10).

Apply tangent/secant refinement only to base-period terms. The concavity is read off the sign of μ̂[yx] provided −lπ ≤ μ̂[yx] ≤ lπ; if μ̂[yx] falls in ]−uπ, −lπ[ or ]lπ, uπ[, the paper does not do tangent/secant refinement but instead refines the precision of π̂ (Sec. 4, PDF p. 10). For extended-period terms, compute the shift s as the rounding towards zero of (μ̂[x] + μ̂[π̂])/(2·μ̂[π̂]), compare μ̂[yx] with μ̂[x] − 2s·μ̂[π̂], and if they differ add the shift lemma π̂(2s−1) ≤ x ≤ π̂(2s+1) → yx = x − 2s·π̂ (Sec. 4, PDF p. 10). The paper says: “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.” and that if the computed shift is wrong, “we may generate something useless but never wrong.”

Add monotonicity lemmas when the model violates sine’s known increasing/decreasing intervals (Sec. 4, PDF pp. 10–11). Initial sine axioms are −1 ≤ sin(z) ≤ 1 for every sine term, and for base-period terms: symmetry, phase (sign), “Zero Tangent”, “π Tangent”, and “Significant Values” (sine equal to 0, ±1, ±1/2 exactly at multiples of π̂/6 and π̂/2 as listed) (Sec. 4, PDF p. 11).

Inference: periodic reduction is a reusable pattern for Verus specs involving bounded periodic functions: normalize into a canonical interval, prove a shift relation, and reason only in the canonical domain. The required π bounds and trigonometric inequalities are not built into Verus and must be supplied as trusted or separately verified lemmas.

technique 4: numerical safeguards and satisfiability lifting

The implementation uses infinite-precision rationals, but Taylor powers can create huge numerators and denominators. It approximates “bad” model values μ̂[x] having too large numerators or denominators by continued fractions, and increases the precision of this rational approximation periodically over the number of iterations, to delay large numbers and “eventually find those numbers if they are really needed” (Sec. 4, “Optimization”, PDF p. 11). Inference: this changes the point at which refinement happens, not the validity of the generated lemma, because the lemma is built from the polynomial bounds at the approximated point; the paper does not state this explicitly.

The abstract solver can return unsat, a concrete SAT conclusion from the universal interval criterion, or an unresolved model requiring more refinement. The paper reports: “The results show that our solver compares favourably with the other solvers, being able to decide the highest number of benchmarks.” (Sec. 1, PDF p. 2). In Fig. 1 the loop returns false, returns true, or aborts when the budget is exhausted (PDF p. 4). Inference: a Verus integration should expose this distinction and never turn an unresolved approximation into a verified postcondition.

evidence, denominator, and limits

Experiments ran on 2.6GHz Intel Xeon X5650 machines with a time limit of 1000 seconds and a memory limit of 6 Gb (Sec. 6, PDF p. 13). The benchmark classes were 887 bounded-model-checking instances, 681 mathematical instances (from the MetiTarski distribution), and 944 instances from the DReal distribution; 96 of the DReal benchmarks contain only exp and sin and need no preprocessing (Sec. 6, PDF pp. 14–16; Table 1, PDF p. 15). The paper states “overall MathSAT solves 906 benchmarks out of 2512, 127 more than DReal, the best among the other systems” and that the “virtual-best system” solves 1353 (Sec. 6, PDF p. 16). Inference: 906 − 127 = 779 for DReal is derived by arithmetic, not stated; 887 + 681 + 944 = 2512. The paper does not say which table columns (original or scaled) make up the 906. These counts combine different benchmark classes and should not be read as a per-class success percentage. The paper also says the solvers’ performance is complementary and suggests integrating interval propagation.

For scaled BMC (887 instances), MathSAT solved 84 SAT and 556 UNSAT cases; iSAT3 solved 35 SAT, 470 UNSAT, and returned 87 MaybeSAT. For scaled Mathematical (681), MathSAT solved 0 SAT and 215 UNSAT, while iSAT3 solved 0 SAT, 212 UNSAT, and returned 137 MaybeSAT (Table 1, PDF p. 15). On the 96 exp/sin-only DReal subset, MathSAT solved 3 SAT and 39 UNSAT, while DReal on the original benchmarks (the orig. row) solved 17 UNSAT and returned 37 MaybeSAT (Table 2, PDF p. 16). On the full 944 DReal benchmarks, DReal on the original format solved 102 UNSAT against MathSAT’s 3 SAT and 68 UNSAT after preprocessing, and the paper says that in the original format DReal solves many more instances (Table 2 and text, PDF pp. 15–16). The paper says there are many cases where DReal returns a DeltaSAT result while also printing an error message that the numerical precision limit has been reached, so it should be read as MaybeSAT in those cases (Sec. 6, PDF p. 15). MetiTarski cannot be run on satisfiable benchmarks and is not comparable on the BMC class (PDF p. 15).

The paper concludes: “The approach is based on an abstraction-refinement loop, where transcendental functions are represented as uninterpreted ones in the abstract space SMT(UFLRA), and are incrementally axiomatized by means of piecewise-linear functions.” Its evidence is solver benchmarks, not end-to-end Rust verification. Inference: trusted components in such a design would include the Taylor remainder bounds, concavity calculations, rational bounds on π, the SMT solver, the preprocessing rewrites for log, cos and the like, and the model-to-formula encoding; the paper does not list them.

techniques for the catalog

  • uninterpreted-function abstraction loop — replace transcendental terms by UF applications and add sound axioms until the model is eliminated or satisfiability is lifted
  • Taylor remainder envelopes — compute rational lower and upper polynomials to a requested precision
  • concavity-guided tangent and secant refinement — add local piecewise-linear lemmas oriented by function curvature
  • periodic canonicalization — reduce sine arguments to a bounded base period with symbolic π bounds and shift lemmas
  • Inference, not a paper technique: keep SAT, UNSAT, and abort-on-budget as distinct outcomes, as in the Fig. 1 loop

Last edited: