**dReal** is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions. **dReal** implements the framework of \(\delta\)-complete decision procedures.

\(\delta\)-Complete decision procedures bypass well-known theoretical difficulties in nonlinear theories over the reals. We say a decision procedure is \(\delta\)-complete for a set \(S\) of formulas, where \(\delta\) is an arbitrary positive rational number, if for any \(\varphi\) from \(S\) the procedure returns one of the following answers:

- “unsat”: \(\varphi\) is unsatisfiable.
- ”\(\delta\)-sat”: \(\varphi^{\delta}\) is satisfiable.

Here, \(\varphi^{\delta}\) is a syntactic variant of \(\varphi\) that encodes a notion of numerical perturbation on logic formulas. Essentially, we allow such a procedure to give answers with one-sided, \(\delta\)-bounded errors. With this relaxation, \(\delta\)-complete decision procedures can fully exploit the power of numerical approximations without losing formal correctness guarantees.

**dReal** returns “unsat” or
“\(\delta\)-sat” on input formulas, where \(\delta\) can be
specified by the user. When the answer is “unsat”, **dReal** produces
a proof of unsatisfiability; when “\(\delta\)-sat”, it provides a
solution such that a \(\delta\)-perturbed form of the input formula
is satisfied.

We have benefited greatly from the following tools: realpaver, ibex, opensmt, minisat, and capd.

## Example

Let’s consider the following example which slighly modifies a formula from the Flyspeck project benchmarks:

\[ \exists^{[3.0,3.14]}x_1. \exists^{[-7.0,5.0]}x_2. 2 \times 3.14159265 - 2 x_1 \arcsin \left(\cos 0.797\times \sin \left(\frac{3.14159265}{x_1}\right)\right) \le - 0.591 - 0.0331 x_2 + 0.506 + 1.0 \]

### Solving with dReal

To solve the formula using **dReal**, we first translate it into the
following SMT2 formula (172.smt2):

1
2
3
4
5
6
7
8
9
10
11

(set-logic QF_NRA)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(assert (<= 3.0 x1))
(assert (<= x1 3.14))
(assert (<= -7.0 x2))
(assert (<= x2 5.0))
(assert (<= (- (* 2.0 3.14159265) (* 2.0 (* x1 (arcsin (* (cos 0.797) (sin (/ 3.14159265 x1)))))))
(+ (- 0.591 (* 0.0331 x2)) (+ 0.506 1.0))))
(check-sat)
(exit)

Note that we encode the range of \(x_1\) and \(x_2\) using four
`assert`

commands `(assert (<= 3.0 x1)`

, ```
(assert (<= x1
64.0))
```

, `(assert (<= -7.0 x2))`

, and `(assert (<= x2 5.0))`

.

We check the \(\delta\)-satisfiability of the formula using
**dReal**:

It takes less than a second to terminate with the **unsat** result.
Recall that this **unsat** result is **exact** and does not involve
any numerical approximation. In the above example, we did not provide
the value of \(\delta\) and therefore **dReal** used the default
value – 0.001. We do have a command-line argument to specify the
delta `--precision`

.

To see the detailed decision traces along with the solving process,
use `--verbose`

option (the omitted result is in
172.smt.verbose):

### Proof Checking

**dReal** is also able to generate a proof along with the
\(\delta\)-satisfiability result. Using `--proof`

option generates
the proof 172.smt2.proof.

We also provide a *proof checker* which can validate the proof for the
*unsat* cases. Our proof-checking process is a semi-algorithm and
therefore its termination is not guaranteed. `-t`

option shoud be
used to specify the timeout in seconds.

172.smt2.proof.output shows that our proof checker solved 4 subproblems in the process of checking and was able to verify the proof within 3 seconds. It saves all the extra information under the directory 172.smt2.proof.extra.