## 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 ineqFor 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 secondsNote 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 secondsThe 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 secondsHere, 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.