dReal

An SMT solver for nonlinear theories of the reals

Sicun Gao, Soonho Kong, Edmund Clarke

CADE'13, 2013/06/12

SMT Problem

problem1.png

  • Complexity results of non-linear arithmetic over the reals
    • Decidable if \(\phi\) only contains polynomials [Tarski51]
    • Undecidable if \(\phi\) contains trigonometric functions
  • Real-world problems contain complex nonlinear functions (\(\sin\), \(\exp\), ODEs)

\(\delta\)-decision Problem

delta_1.png

Standard Form

$$\phi := \exists^{\mathbf{I}} \mathbf{x} \bigwedge_{i=1}^m \bigvee_{j=1}^k f_{ij}(\mathbf{x}) = 0$$

\(\delta\)-decision Problem

delta_2.png

\(\delta\)-Weakening of \(\phi\)

$$\phi^{\delta} := \exists^{\mathbf{I}} \mathbf{x} \bigwedge_{i=1}^m \bigvee_{j=1}^k \mid f_{ij}(\mathbf{x}) \mid \le \delta$$

\(\delta\)-decision Problem

problem2.png

  • UNSAT: \(\phi^\delta\) is unsatisfiable
  • \(\delta\)-SAT: \(\phi^\delta\) is satisfiable
  • Decidable [LICS'12, IJCAR'12]
    • NP-complete: \(\mathcal{F} = \{ +, \times, \exp, \sin, ... \}\)
    • PSPACE-complete: \(\mathcal{F} = \{ \text{ODEs with P-computable rhs} \}\)

\(\delta\)-decision Problem

delta_3.png

$$ \phi^{\delta} : UNSAT \implies \phi : UNSAT$$

\(\delta\)-decision Problem

delta_5.png

$$ \phi^{\delta} : SAT \implies \color{red}{\phi : SAT} \lor \phi : UNSAT$$

\(\delta\)-decision Problem

delta_4.png

$$ \phi^{\delta} : SAT \implies \phi : SAT \lor \color{red}{\phi : UNSAT}$$

\(\delta\)-decision Problem

delta_7.png

May find a smaller \(\delta' < \delta\) such that

$$\phi^{\delta'} : UNSAT \implies \phi : UNSAT$$

\(\delta\)-decision Problem

delta_8.png

\(\phi^{\delta'} : SAT\) with a reasonably small \(\delta'\)

may indicate a robustness problem of the system in verification.

"Small perturbation on the system may violate safety properties"

dReal

  • \(\delta\)-complete SMT solver
  • Can handle various nonlinear real functions such as $$\sin, \cos, \tan, \arcsin, \arccos, \arctan, \log, \exp$$
  • Can handle ODEs (Ordinary Differential Equations)
  • Open-source: http://dreal.cs.cmu.edu

Design of dReal

dpll1.png

General DPLL\(\langle T \rangle\) Framework

Design of dReal

dpll2.png

DPLL\(\langle \mathrm{ICP} \rangle\) Framework

  • ICP (Interval Constraint Propagation) solver
  • Uses "Branch & Prune" algorithm

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : y = \sin(x) \land y = \mathrm{atan}(x)$$

prune0.png

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : \color{red}{y = \sin(x)} \land y = \mathrm{atan}(x)$$

prune0.png

$$\begin{eqnarray*} x' & = & x \cap \sin^{-1}(y)\\ & = & [0.5, 1.0] \cap \sin^{-1}([0.5, 1.0])\\ & = & [0.5, 1.0] \cap [0.524, 1.570]\\ & = & [0.524, 1.0] \end{eqnarray*}$$

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : \color{red}{y = \sin(x)} \land y = \mathrm{atan}(x)$$

prune0.png

$$\begin{eqnarray*} y' & = & y \cap \sin(x)\\ & = & [0.5, 1.0] \cap \sin([0.524, 1.0])\\ & = & [0.5, 1.0] \cap [0.5, 0.841]\\ & = & [0.5, 0.841] \end{eqnarray*}$$

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : \color{red}{y = \sin(x)} \land y = \mathrm{atan}(x)$$

prune1.png

$$ x : [0.524,1.0], y : [0.5,0.841] $$

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : y = \sin(x) \land \color{red}{y = \mathrm{atan}(x)}$$

prune1.png

$$\begin{eqnarray*} x' & = & x \cap \mathrm{atan}^{-1}(y) \\ & = & [0.524, 1] \cap \mathrm{atan}^{-1}([0.5, 0.841]) \\ & = & [0.524, 1] \cap [0.546, 1.117] \\ & = & [0.546, 1.0] \end{eqnarray*}$$

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : y = \sin(x) \land \color{red}{y = \mathrm{atan}(x)}$$

prune1.png

$$\begin{eqnarray*} y' & = & y \cap \mathrm{atan}(x) \\ & = & [0.5, 0.841] \cap \mathrm{atan}([0.546, 1.0]) \\ & = & [0.5, 0.841] \cap [0.5, 1.0] \\ & = & [0.5, 0.785] \end{eqnarray*}$$

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : y = \sin(x) \land \color{red}{y = \mathrm{atan}(x)}$$

prune2.png

$$ x : [0.524,1.0], y : [0.5,0.785] $$

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : y = \sin(x) \land y = \mathrm{atan}(x)$$

ANSWER: UNSAT

ICP: Pruning

$$\exists x, y \in [0.5, 1.0] : y = \sin(x) \land y = \mathrm{atan}(x)$$

prune3.png

ANSWER: UNSAT

ICP: Branching

  • Divide the search space and try each one
  • Stop when the size of box is smaller than \(\epsilon\):

    $$ |B| < \epsilon$$

    epsilon.png

ICP: Branching

$$\exists x \in [0.5, 2.0], y \in [0.0, 2.0] : y = \sin(x) \land y = \mathrm{atan}(x)$$

$$\epsilon = 0.001$$

ANSWER: \(\delta\)-SAT

ICP: Branching

sin_arctan_sat.png

ANSWER: SAT

ICP in dReal

alg0.png

ICP in dReal

alg1.png

ICP in dReal

alg2.png

ICP in dReal

alg3.png

ICP in dReal

alg4.png

ICP in dReal

alg5.png

ODE Pruning in ICP (Forward)

ode_tx0.png

$$ X_t = \sharp \vec{y} (X_0, T) $$

ODE Pruning in ICP (Forward)

ode_tx1.png

$$ X_t = \sharp \vec{y} (X_0, T) $$

ODE Pruning in ICP (Forward)

ode_tx2.png

$$ X'_t = X_t \cap \sharp \vec{y} (X_0, T) $$

ODE Pruning in ICP (Backward)

ode_t00.png

$$ X_0 = \sharp \vec{y}_{-} (X_t, T) $$

ODE Pruning in ICP (Backward)

ode_t01.png

$$ X_0 = \sharp \vec{y}_{-} (X_t, T) $$

ODE Pruning in ICP (Backward)

ode_t02.png

$$ X'_0 = X_0 \cap \sharp \vec{y}_{-} (X_t, T) $$

Extracting Proofs from UNSAT Cases

proof1.png

  • Proving the correctness of an SMT solver is difficult task
  • Instead, dReal can generate proofs for the UNSAT cases
  • Proof checker is available, which is a small program. (<500 lines of OCaml code)

Input Format

  • Standard SMT-LIB 2.0 format with extensions
  • Allow transcendental functions such as \(\sin\), \(\tan\), \(\arcsin\), \(\exp\), \(\log\), \(\exp\), \(\sinh\)
  • Precision(\(\epsilon\)) can be set by "(set-info :precision \(\epsilon\))" (default: \(10^{-3}\))

Experimental Results: Flyspeck Benchmark

  • Formal verification of Kepler's conjecture
  • 916 Instances (supposed to be all UNSAT)
  • Highly complex (example: 859.smt2)

Experimental Results: Flyspeck Benchmark

  • Formal verification of Kepler's conjecture
  • 916 Instances (supposed to be all UNSAT)
  • We solve 909 instances, 7 timeout (5min)
    • 864 UNSAT
    • 45 \(\delta\)-SAT (precision = \(10^{-3}\))

Experimental Results: Flyspeck Benchmark

Experimental Results: Hybrid System Benchmark

Experimental Results: Hybrid System Benchmark

Bouncing Ball

Experimental Results: Hybrid System Benchmark

  • Including Atrial Filbrillation Model: (R. Groso et al, "From Cardiac Cells to Genetic Regulatory Networks", CAV'11)

cardiac1.png

Experimental Results: Hybrid System Benchmark

cardiac_sim.png

Conclusion

  • dReal is an \(\delta\)-complete SMT solver
  • Support nonlinear real functions such as $$\sin, \cos, \tan, \arcsin, \arccos, \arctan, \log, \exp, \dots$$
  • Handle ODEs (Ordinary Differential Equations)
  • Based on DPLL\(\langle \mathrm{ICP} \rangle\) framework
  • Scalable with our experiments
  • Open-source: available at http://dreal.cs.cmu.edu

Questions?

FAQ

  • Q: What is a proof for an UNSAT case?
  • A: Partition of search space. $$\exists x, y \in [0.5, 1.0] : y = \sin(x) \land y = \mathrm{atan}(x)$$ proof.png

FAQ

  • Q: Input format for ones with ODEs?
  • A: Here it is.