
## The param.transc file

The user can tune the parameters of the nonlinear certification scheme, by editing the nlcertify/param.transc file, whose content looks like:
******* User Parameters *******

* Maximal number of control points for maxplus approximation
samp_iters = 3

* Branch and Bound Parameters
bb = false

* Replace all the variables x by sqrt (x), this is HIGHLY RECOMMENDED FOR FLYSPECK INEQUALITIES
xconvert_variables = true

* Check the correctness of SOS certificates in Coq
check_certif_coq = false

* Verbose settings
problem_verb = true
semialg_verb = true
parab_verb = true
[...]
Note that the parameters are typed. For instance, the type of the parameter scale_pol is bool, so the user can edit the file by writing either scale_pol = true or scale_pol = false. The type of the relaxation order relax_order is int, thus the user may write relax_order = 2 to solve SDP at first or second relaxation order (when the degree of the minimal relaxation order is not greater than 2).

### General Parameters

• samp_iters (int): maximal length of the sequence of control points for maxplus approximation. When samp_iters = 0, the tool computes the bounds of semialgebraic functions with standard SOS relaxations and bounds the univariate transcendental functions by interval arithmetic.
• bb (bool): when bb = true, domain subdivision is performed until the inequality is successfully certified.
• xconvert_variables (bool): when xconvert_variables = true, then the objective function $\xb \mapsto f(x_1, \dots, x_n)$ is replaced by $\yb \mapsto f(y_1, \dots, y_n)$ with $y_i := \sqrt{x_i} \ (i = 1, \dots, n)$. The input box $K := [a_1, b_1] \times \dots \times [a_n, b_n]$ is replaced by $K' := [a_1^2, b_1^2] \times \dots \times [a_n^2, b_n^2]$. It works only when $K$ is contained in the nonnegative orthant of $\R^n$.
• check_certif_coq (bool): when check_certif_coq = true, the correctness of the SOS certificates is checked in $\coq$

### Verbosity

• problem_verb (bool): displays the function $f$ and the box $K$ of the initial problem.
• semialg_verb (bool): displays information when bounding semialgebraic components.
• parab_verb (bool): displays information about lower/upper approximations of special univariate functions ($\arctan$, $\sqrt{\cdot}$) as well as the sequence of control points for the nonlinear maxplus algorithm.
• pop_verb (bool): displays information when solving the polynomial optimization problems (polynomials, lower/upper bounds, SOS degree, timings, etc.).
• coq_verb (bool): displays time and success/failure information when checking SOS certificates inside $\coq$.
• print_precision (int): number of significant digits printed. Note that the coefficients of polynomials are arbitrary-size rationals. However there are displayed using floating-point numbers.

### POP/SDP Relaxations

Let $K := [a_1, b_1] \times \dots \times [a_n, b_n]$ be a box and let $\fpop$, $g_1, \dots, g_m \in \R[\xb]$. We recall the general constrained POP: $(POP)\left\{ \begin{array}{ll} \inf_{\xb \in K} & \fpop (\xb) \enspace , \\ \text{s.t.} & g_1(\xb)\geq 0,\dots,g_m(\xb) \geq 0 \enspace. \end{array} \right.$ Several options are available to handle numerical issues when solving SDP relaxations of $(POP)$. In the sequel, we will often refer to this problem to describe the usage of these options. We also recall that the minimal SDP relaxation order of Problem $(POP)$ is $k_0 := \max(\lceil \deg \fpop / 2 \rceil ,\max_{1 \leq j \leq m} \lceil \deg g_j / 2\rceil)$. There always exists $M > 0$ such that $M - \sum_{i = 1}^n x_i^2 \geq 0$. Let $(POP)'$ be the scaled POP version of Problem $(POP)$: $(POP)'\left\{ \begin{array}{ll} \inf_{\xb' \in [0, 1]^n} & \fpop' (\xb') \enspace , \\ \text{s.t.} & g_1'(\xb')\geq 0,\dots,g_m'(\xb') \geq 0 \enspace, \end{array} \right.$ where $x_i' := (x_i - a_i) / (b_i - a_i) \ (i = 1, \dots, n) \enspace,$ $\fpop' := \fpop / \linfnorm{\fpop}, \quad g_j' := g_j / \linfnorm{g_j} \ (j = 1, \dots, m) \enspace .$ The function $\linfnorm{\cdot}$ returns the maximum magnitude of the coefficients of polynomials in $\R[\xb']$. After solving Problem $(POP)$, one obtains the following decomposition from the output of $\sdpa$: $$\label{eq:soscertifconcl} \fpop(\xb) - \mu_k = \sum_{j = 0}^m g_j(\xb) \sum_{i = 1}^{r_j} \lambda_{i j} v_{i j}^2(\xb) \enspace.$$
• relax_order (int): when relax_order = $k$, SDP relaxations of $(POP)$ are solved using a relaxation order not greater than $\max (k, k_0)$.
• reduce_sos (bool): allows to eliminate the redundant vectors for any SOS representation of $\fpop - \sum_{j = 1}^m \sigma_j g_j$.
• scale_pol (bool): when scale_pol = true, solves Problem $(POP)'$ instead of Problem $(POP)$.
• bound_squares_variables (bool) : adds the polynomial inequalities $(b_i - x_i) (x_i - a_i) \geq 0 \ (i=1, \dots, n)$ to the constraints set of $(POP)$.
• mk_archimedean (bool): adds the single polynomial inequality constraint $\sum_{i = 1}^n M - x_i^2 \geq 0$ to the constraints set of $(POP)$.
• eig_tol (float): replaces each $\lambda_{i j}$ by $0$ in \eqref{eq:soscertifconcl} when eig_tol $\geq \lambda_{i j}$.
• eq_tol (float): when eq_tol $= \epsilon > 0$, then each polynomial equality constraint $h (\xb) = 0$ is relaxed into two polynomial inequalities $h (\xb) \geq 0$ and $h (\xb) \geq - \epsilon$.
• sdp_solver_epsilon (int): the accuracy of the SDP solver $\sdpa$ ( for more details, see this research report).
• sdp_solver_print (int): the number of digits displayed in the output of $\sdpa$ files.
• erase_sdpa_files (bool): when erase_sdpa_files = true, the I/O $\sdpa$ files are erased. Otherwise, they are stored in the nlcertify/log folder.