$\def\sc#1{\dosc#1\csod} \def\dosc#1#2\csod{{\rm #1{\small #2}}} \def\nlcertify{\textrm{NLCertify}} \def\xb{\mathbf{x}} \def\ocaml{\sc{OCAML}} \def\coq{\sc{COQ}} \def\ssreflect{\sc{SSREFLECT}} \def\hol{\sc{HOL-LIGHT}} \def\sdpa{\sc{SDPA}} \newcommand{\sollya}{\mathtt{Sollya}} \def\opam{\sc{OPAM}}$

## Input Settings

The user can define the input box $K := [a_1, b_1] \times \dots \times [a_n, b_n]$ and the multivariate transcendental objective function $f$ in the file nlcertify/test.ineq. The inequality $\forall \xb \in K, f(\xb) \geq m$ is encoded as follows:
let box_ineq x1 ... xn = [(a1 , b1); ... ; (an , bn)];;
let obj_ineq x1 ... xn = [(f, m )];;

Note that it is mandatory to separate each definition with a double semicolon ;; (either for a box or an objective function).
Let us give a concrete example for Problem MC. We recall the formulation of the problem: $\mathop{\min_{-1.5 \leq x_1 \leq 4}}_{-3 \leq x_2 \leq 3} f(\xb) = \sin (x_1 + x_2) + (x_1 - x_2)^2 - 1.5 x_1 + 2.5 x_2 + 1 \enspace .$ Hence we encode the inequality $\forall \xb \in K, f(\xb) \geq -1.92$ in $\nlcertify$ as follows:
let box_MC x1 x2 = [ (-1.5, 4) ; (-3, 3) ];;
let obj_MC x1 x2 = [ (sin(x1 + x2) + (x1 - x2)**2  - 1.5 * x1 + 2.5 * x2 + 1, -1.92 )];;


## Execution

Given a inequality identified with ineq, the following command line allows to execute the main program:
% ./nlcertify ineq

For instance, without domain subdivision (setting the option bb = false) and with the maxplus method (approx_minimax = false) the program returns the following output, after a single iteration (samp_iter = 1) :
% ./nlcertify MC
...
1 problem remaining, 0 cuts done
[(-1.5, 4.0) ; (-3.0, 3.0)]
...
Lower bound = -62.1516224511
Minimizer candidate x = [3.9999997899 ; 2.9999997870]

1 problem solved, 0 cuts done
End of maxplus algorithm
-62.1516382708 <= 0.0000000000
Failed to verify the inequality MC
Total time: 1.149512 seconds

Note that the box is displayed, as well as the lower bound $m$ of the objective function on this box ($m \simeq -62$). The minimizer candidate $\xb \simeq (4, 3)$ is obtained. In this case, the relaxation gap is too high to certify the inequality. After 3 iterations, (samp_iter = 3), the output is:
% ./nlcertify MC
...
Lower bound = -0.7724701755
Minimizer candidate x = [-1.1392425485 ; -2.3139139020]

1 problem solved, 0 cuts done
End of maxplus algorithm
-0.7724701755 <= 0.0000000000
Failed to verify the inequality MC
Total time: 1.828811 seconds

The lower bound is more precise ($m \simeq -0.772$). One has to switch the bb option to true to solve the inequality:
% ./nlcertify MC
...
8 problems solved, 7 cuts done
End of maxplus algorithm
0.0007519016 >= 0.0000000000
Inequality MC verified
Total time: 3.274948 seconds

Here, the lower bound obtained after the $7$ subdivisions is greater than $0$ ($m \simeq 0.00075$). The verbosity options can be switched to display more information when the algorithms implemented in $\nlcertify$ are called on each sub-box (e.g. the sequence of control points, the equation of the estimators, the I/O data of the external solvers, etc.). These information are saved in the nlcertify/log/mc.log file.