\( \def\sc#1{\dosc#1\csod} \def\dosc#1#2\csod{{\rm #1{\small #2}}} \def\nlcertify{\textrm{NLCertify}} \def\xb{\mathbf{x}} \def\yb{\mathbf{y}} \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}} \newcommand{\R}{\mathbb{R}} \newcommand{\fpop}{f_{\text{pop}}} \newcommand{\linfnorm}[1]{\Vert #1 \Vert_{\infty}} \)

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$: \begin{equation} \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. \end{equation}
  • 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.