# MILP certificate file format version 1.0

## Preliminaries
Before we describe the mixed-integer linear programming (MILP) certificate [file format](#file-format), we introduce some jargon and conventions used in this document.

### Variable indices
Variables of the MILP problem are indexed from $0$ to $n-1$ where $n$ is the total number of variables. Throughout this document, $X_i$ refers to the variable indexed by $i$ regardless of its actual variable name.

### Numbers
We refer to two kinds of numbers: indices and values. Indices are integers. Values are rational numbers expressed as finite decimals or fractions.

### Constraints
The certificate file includes two kinds of constraints: the constraints of the MILP problem and derived constraints. Constraints have unique constraint names and are assigned indices starting from $0$ according to the order in which they appear in the certificate file.

Each constraint is of the form $a_{i_1}X_{i_1}+\dots+a_{i_p}X_{i_p} \text{sense}\ \beta,$ where `sense` is $=,\leq$ or $\geq,\beta$ is a rational value, $p\in\{1,\dots,n\},$ and for $j=1,\dots p,i_j$ is a variable index, $X_{i_j}$ is a variable with index $i_j,$ and $a_{i_j}$ is a rational value.

Bound constraints such as $0\leq\beta\leq 1$ are not treated specially.

### Rounding
Suppose that the constraint $a_{i_1}X_{i_1}+\dots+a_{i_p}X_{i_p} \text{sense}\ \beta,$ where `sense` is $\leq$ or $\geq,$ is such that fpr $j=1,\dots, p,a_{i_j}$
is and integer and is nonzero only if $i_j$ is an integer variable index, then the constraint $a_{i_1}X_{i_1}+\dots+a_{i_p}X_{i_p} \text{sense}\ \beta'$ with
$$\beta' =
\left \{
\begin{array}{ll}
\lfloor\beta\rfloor & \text{if sense is } \leq \\
\lceil\beta\rceil & \text{if sense is } \geq \\
\end{array}
\right.$$
is said to be obtained from rounding.

### Domination of constraints
We use a restricted form of constraint domination. A constraint that is $0\geq \beta$ with $\beta >0$ , $0\leq\beta$ with $\beta<0$, or $0=\beta$ with $\beta\neq 0$ is called an absurdity or falsehood. Such a constraint dominates any other constraint.

The constraint $a^Tx\geq\beta$ or $a^Tx=\beta$ dominates $a'^Tx\geq\beta′$ if $a=a′$ and $\beta\geq\beta'.$

Similarly, the constraint $a^Tx\leq\beta$ or $a^Tx=\beta$ dominates $a′^Tx\leq\beta′$ if $a=a′$ and $\beta\leq\beta'.$

Finally, the constraint $a^Tx=\beta$ dominates $a′^Tx=\beta′$ if $a=a′$ and $\beta=\beta′.$

### Suitable linear combinations of constraints
For a constraint named $C$, define $l(C)$ to be the left-hand side of $C$ and define $r(C)$ to be the right-hand side of $C$, and

$$s(C)=\left\{
\begin{array}{ll}
1 & \text{if } C \text{ is a } \geq\text{-constraint}\\
0 & \text{if } C\text{ is a } =\text{-constraint} \\
-1 & \text{if } C\text{ is a } \leq\text{-constraint} \\
\end{array}
\right. $$
For example, for the constraint $C_1:  2X_1+3X_2\geq 1$, we have $l(C_1)=2X_1+3X_2,r(C_1)=1,s(C_1)=1.$
Let $C_1,\dots,C_k$ be constraint names. Let $\lambda_1,\dots,\lambda_k$ be values such that $\lambda_js(C_j)\geq 0$ for all $j=1,…,k,$ or $\lambda_js(C_j)\leq 0$ for all $j=1,…,k.$
Then $\lambda_1\cdot C_1+\dots +\lambda_k \cdot C_k$ is called a suitable linear combination and denotes the constraint
$$
\left\{
\begin{array}{ll}
\sum_{i=1}^k\lambda_i l(C_i)=\sum_{i=1}^k\lambda_i r(C_i) & \text{if }\lambda_j s(C_j) = 0 \text{ for all } j=1,\dots,k \\
\sum_{i=1}^k\lambda_i l(C_i)\geq\sum_{i=1}^k\lambda_i r(C_i) & \text{if }\lambda_j s(C_j) \geq 0 \text{ for all } j=1,\dots,k \text{ and } \lambda_q s(C_q)\neq 0 \text{ for some } q\in\{1,\dots,k\} \\
\sum_{i=1}^k\lambda_i l(C_i)\leq\sum_{i=1}^k\lambda_i r(C_i) & \text{if }\lambda_j s(C_j) \leq 0 \text{ for all } j=1,\dots,k \text{ and } \lambda_q s(C_q)\neq 0 \text{ for some } q\in\{1,\dots,k\}\\
\end{array}
\right. $$

## Constraint format
Specifying a constraint $a_{i_1}X_{i_1}+\cdots+a_{i_p}X_{i_p}\text{ sense }\beta$ in constraint format means listing the details of the constraint in the following order: the constraint name, then the character representing 𝚜𝚎𝚗𝚜𝚎 (`E` when `sense` is $=,$ `L` when `sense` is $\leq,$ `G` when `sense` is $\geq$), then $\beta$, then
- $p$ $i_1$ $a_{i_1}$ $\cdots$ $i_p$ $a_{i_p}$;
- or the keyword `OBJ` for indicating that $a_{i_1}X_{i_1}+⋯+a_{i_p}X_{i_p}$ is the same as the objective function.

For example, the constraint $−1X_1+6X_2\leq3$ with constraint name `C3` specified in constraint format is

```
C3 L 3  2  1 -1  2 6
```

If the objective function specified in the certificate file is equal to $−1X_1+6X_2,$ no matter whether to be minimized or maximized, then we may also write the shorter form

```
C3 L 3 OBJ
```

### Reason format
Every constraint in the [DER section](#der-section) specified below is associated with a `reason`.
A `reason` associated with a constraint with constraint index `idx` must have one of the following forms:

- { asm }
- {  lin  $p$  $i_1$  $\lambda_1$ $\cdots$  $i_p$  $\lambda_p$  } where $p$ is a nonnegative integer, $i_1,\dots,i_p$ are distinct indices at least $0$ and less than `idx`, and $\lambda_1,\dots,\lambda_p$ are rational values such that $\lambda_1\cdot C_{i_1}+\dots+\lambda_p\cdot C_{i_p}$ is a suitable linear combination that dominates the associated constraint; here $C_{i_j}$ denotes the constraint with index $i_j$ for $j=1,\dots,p.$
- {  rnd  $p$  $i_1$  $\lambda_1$  $\cdots$  $i_p$  $\lambda_p$  } where $p$ is a nonnegative integer, $i_1,\dots,i_p$ are distinct indices at least $0$ and less than `idx`, and $\lambda_1,\dots,\lambda_p$ are rational values such that $\lambda_1\cdot C_{i_1}+⋯+\lambda_p\cdot C_{i_p}$, is a suitable linear combination that can be rounded and the rounded constraint dominates the associated constraint; again $C_{i_j}$ denotes the constraint with index $i_j$ for $j=1,…,p.$
- {  uns  $i_1$  $l_1$  $i_2$  $l_2$  } where $i_1, l_1, i_2, l_2$ are indices at least $0$ and less than `idx` such that the constraints indexed by $i_1$ and $i_2$ both dominate the associated constraint and the constraints indexed by $l_1$ and $l_2$ are, perhaps after reordering, $a_{i_1}X_{i_1}+\cdots a_{i_p}X_{i_p}\leq\beta$ and $a_{i_1}X_{i_1}+\cdots a_{i_p}X_{i_p}\geq\beta +1$ such that $\beta$ is an integer and for $j=1,…,p, a_{i_j}$ is an integer and $X_{i_j}$ is an integer variable.
- { sol }

## File format
The initial lines of the file may be comment lines. Each comment line must begin with the character "%".
The first line, after the comment lines, must be
```
VER 1.0
```
indicating that the certificate file conforms to version 1.0 of the certificate file format.

The remaining content is divided into seven sections and must appear in the following order:
-   `VAR` for the variables,
-   `INT` for integer variables,
-   `OBJ` for the objective function,
-   `CON` for the constraints,
-   `RTP` for the relation to prove,
-   `SOL` for the solutions to check,
-   `DER` for the derivations.

These sections have to be formatted as shown below.

### VAR section
The section begins with
```
VAR n
```
where $n$ is the number of variables, then followed by the n variable names separated by spaces or line breaks.
The variables are assigned indices from $0$ to $n−1$ according to the order in which the variable names are listed.
For example, the following specifies two variables `x` and `y`:
```
VAR 2
x y
```

### INT section

The section begins with
`INT i`
where $i$ is the number of integer variables, then followed by the $i$ integer variable indices separated by spaces or line breaks.
For example, the following specifies our variables `x` and `y` as integer variables:
```
INT 2
0 1
```

### `OBJ` section

The section begins with
`OBJ objsense`
where `objsense` is the keyword `min` for minimization or `max` for maximization, then followed by an integer $k$ and $2k$ numbers $i_1\ c_1\ i_2\ c_2\ \dots\ i_k\ c_k$
separated by spaces or line breaks where for $j=1,…,k, i_j$ is a variable index and $c_k$ is the objective function coefficient for the variable with index $i_j.$

For example, the `OBJ` section for the problem
$$
\begin{array}{ll}
\text{min} & x+y \\
\text{s.t.} & C_1:4x+y\geq 1 \\
 & C_2:4x-y\leq 2\\
\end{array}
$$
could look like the following
```
OBJ min
2  0 1  1 1
```

### CON section
The section begins with

`CON m  b`
where $m$ is the total number of constraints (including bound constraints) and $b$ is the total number of bound constraints, and then followed by $m$ constraints listed in [constraint format](#constraint-format).

The constraints in this section are assigned indices from $0$ to $m−1$ according to the order in which they are listed.
Bound constraints must appear at the beginning of the section **before** the nonbound constraints.

For example, the `CON` section for the problem
$$\begin{array}{ll}
\text{min} & x+y \\
\text{s.t.} & C_1:4x+y\geq 1 \\
 & C_2:4x-y\leq 2\\
\end{array} $$
could look like the following
```
CON 2 0
C1 G 1  2  0 4  1 1
C2 L 2  2  0 4  1 -1
```
Here, there are no bound constraints but any program that outputs a certificate is free to choose arbitrary names for the bound constraints.

### RTP section
The section is either

`RTP infeas`
for indicating infeasibity, or
`RTP range lb  ub`
where `lb` specifies the lower bound on the optimal value to be verified and `ub` specifies the upper bound on the optimal value to be verified. The specified lower bound can be `-inf` if no actual lower bound is to be verified and the specified upper bound can be `inf` if no actual upper bound is to be verified.
For example, if the `RTP` section is
```
RTP range 1 inf
```
only a lower bound of $1$ is to be verified.
In our example, the `RTP` section looks like this:
```
RTP range 1 1
```
### SOL section
The section begins with
`SOL s`
where s is the number of solutions to be verified for feasibility, and then followed by
$S_1 \\ \vdots \\ S_s$
such that for $j=1,…,s, S_j$ is of the form $\text{name } p\ i_1\ v_1\ \cdots\ i_p\ v_p,$ where `name` is the solution name, $p$ is a nonnegative integer, and for $r=1,…,p, i_r$ is a variable index and $v_r$ is the solution value for the variable with index $i_r$. All other variables are assumed to have the value zero.
At least one of the solutions specified should have objective function value at least the lower bound given in the [RTP section](#rtp-section) in the case of maximization and at most the upper bound given in the [RTP section](rtp-section) in the case of minimization.
For example, to specify the two solutions $(x,y)=(1,2)$ (which is feasible) and $(x,y)=(0,1)$ (which is optimal) where $x$ has variable index `0` and $y$ has variable index `1`, the `SOL` section could look like this:
```
SOL 2
feas 2  0 1  1 2
opt 1  1 1
```

### DER section
The section begins with
`DER d`
where `d` is the number of derived constraints to be verified, and then followed by
$D_1\\\vdots\\ D_d$
such that $D_1,\dots,D_d$ are assigned constraint indices from $m$ to $m+d−1$ according to the given order and for $j=1,…,d, D_j$ is of the form
```
constraint reason index
```
where `constraint` is the constraint to be verified in [constraint format](#constraint-format), `reason` is the reason associated with the constraint in [reason format](#reason-format), and `index` is $−1$ or is an index such that no constraint with a larger index refers to this constraint.
Each constraint in this section carries implicitly a set of assumptions deduced as follows:

- If `reason` is {  asm  }, then the set of assumptions contains simply the index of the constraint.
- If `reason` is {  lin  $p\  i_1\  \lambda_1\  \cdots \ i_p\   \lambda_p$  } or {  rnd  $p\  i_1\  \lambda_1\  \cdots\  i_p\  \lambda_p$  }, then the set of assumptions is the union of the sets of assumptions of the constraints indexed by $i_1,…,i_p.$
- If `reason` is {  uns  $i_1\  l_1\  i_2\  l_2$  }, then the set of assumptions is the union of the sets of assumptions of the constraint indexed by $i_1$ without $l_1$ and of the constraint indexed by $i_2$ without $l_2.$

If the `RTP` section is `RTP infeas`, then the last constraint in this section should be an absurdity with an empty set of assumptions.
If the `RTP` section is `RTP range lb ub`, then the last constraint in this section should be a constraint with an empty set of assumptions that dominates $\text{OBJ}\geq  lb$ in the case of minimization or $\text{OBJ}\leq ub$ in the case of maximization where `OBJ` denotes the objective function.

**Remark.** The reason for specifying `index` is to allow a verifier to discard the corresponding constraint from memory once the verifier has completed verifying constraint with index `index`.

For example, the `DER` section for the problem above could look like this:
```
C3 G -1/2  1  1 1   { lin 2  0 1/2  1 -1/2 } 3
C4 G 0     1  1 1   { rnd 1  2 1 } 4
C5 G 1/4   OBJ     { lin 2  0 1/4  3 3/4 } 5
C6 G 1     OBJ     { rnd 1  4 1 } 0
```

For a small example, we refer to the file [paper_eg3.vipr](code/paper_eg3.vipr).