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 (see [GAC’12]).
dReal returns “unsat” or “\(\delta\)-sat” on input formulas, where \(\delta\) is a numerical error bound specified by the user. When the answer is “unsat”, dReal guarantees that the formula is unsatisfiable. When the answer is “\(\delta\)-sat”, it returns a set of solutions that all satisfy a \(\delta\)-perturbed form of the input formula.
We have benefited greatly from various tools, including ibex, picosat, 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.