Merge pull request #6 from scipopt/alexhoen-patch-1

fix ReadME

Author: alexhoen

cert_spec_v1_1.md

@@ -96,8 +96,8 @@ A `reason` associated with a constraint with constraint index `idx` must have on
 - { sol }
 
 #### New in version 1.1: incomplete keywords
-- { lin weak {$n$ $t_1$ $j_1$ $\nu_1$ $\cdots$ $t_n$ $j_n$ $\nu_n$} $p$  $i_1$  $\lambda_1$ $\cdots$  $i_p$  $\lambda_p$ } where $p, \lambda, i$ are the same as for `lin`, except that the linear compbination only weakly dominates the associated constraint. The additional inner brackets describe a set of local bounds to be used during completion of this constraint. $t_1,\cdots,t_n$ are either $U$ (upper bound) or $L$ (lower bound). $j_1,\cdots,j_n$ are variable indices, and $\nu_1,\cdots,\nu_n$ are the certificate line indices for the corresponding bound constraints. Alternatively, the inner brackets can be { 0 } to use global bounds.
-- { lin incomplete $i_1, \cdots i_n$ } where $i_1, \cdots i_n$ are constraint indices that are active, such that an exact linear program should be solved using the model constraints as well as these additional constraint to find correct multipliers to prove validity of the associated constraint.
+- { lin weak {$n$ $t_1$ $j_1$ $\nu_1$ $\v_1$ $\cdots$ $t_n$ $j_n$ $\nu_n$ $\v_n$} $p$  $i_1$  $\lambda_1$ $\cdots$  $i_p$  $\lambda_p$ } where $p, i, \lambda$ are the same as for `lin`, except that the linear combination only weakly dominates the associated constraint. The additional inner brackets specify a set of local bounds to be used during the completion of this constraint. $t_1,\cdots,t_n$ are either $U$ (upper bound) or $L$ (lower bound). $j_1,\cdots,j_n$ are variable indices, $\nu_1,\cdots,\nu_n$ are the certificate line indices for the corresponding bound constraints, and $\v_1,\cdots,\v_n$ are the corresponding bounds. Alternatively, the inner brackets can be { 0 } to use global bounds.
+- { lin incomplete $i_1 \cdots i_n$ } where $i_1, \cdots, i_n$ are constraint indices that are active, such that an exact linear program should be solved using the model constraints as well as these additional constraints to find correct multipliers to prove the validity of the associated constraint.
 
 Examples of the usage of these incomplete keywords can be found in the files [paper_eg3_weak.vipr](code/paper_eg3_weak.vipr) and [paper_eg3_incomplete.vipr](code/paper_eg3_incomplete.vipr). These are incomplete toy versions of [paper_eg3.vipr](code/paper_eg3.vipr).
 

examples/paper_eg3.vipr

@@ -1,4 +1,4 @@
-% Example 3 in the paper
+% Example 3 in the paper "Safe and Verified Gomory Mixed Integer Cuts in a Rational MIP Framework"
 VER 1.0
 VAR 2
 x y

examples/paper_eg3_incomplete.vipr

@@ -1,4 +1,5 @@
-% Example 3 in the paper - incomplete version that needs to be completed prior to verification
+% Example 3 in the paper "Safe and Verified Gomory Mixed Integer Cuts in a Rational MIP Framework"
+% incomplete version that needs to be completed prior to verification
 VER 1.1
 VAR 2
 x y
@@ -13,14 +14,14 @@ C3  L 3  2  0 -1  1 6
 RTP infeas
 SOL 0
 DER 11
-A1  L 0   1  0 1  { asm } -1
-A2  G 1   1  0 1  { asm } -1
-A3  L 0   1  1 1  { asm } -1
-C4  G 1   0       { lin incomplete 3 5 } 12 % A1 and A3 are active
-A4  G 1   1  1 1  { asm } -1
-C5  G 1   0       { lin incomplete 3 7 } 12 % A4 is active
-C6  G 1/4 1  1 1  { lin incomplete 4 } 10 % A2 is active
-C7  G 1   1  1 1  { rnd 1  9 1 } 11
-C8  G 1   0       { lin incomplete 10 } 13 % C7 is active - not only bound constraints are possible with the incomplete keyword
-C9  G 1   0       { uns 6 5  8 7 } 13
+A1  L 0   1  0 1  { asm } -1                                    % vipr id 3
+A2  G 1   1  0 1  { asm } -1                                    % vipr id 4
+A3  L 0   1  1 1  { asm } -1                                    % vipr id 5
+C4  G 1   0       { lin incomplete 3 5 } 12                     % A1 and A3 are active
+A4  G 1   1  1 1  { asm } -1                                    % vipr id 7
+C5  G 1   0       { lin incomplete 3 7 } 12                     % A4 is active
+C6  G 1/4 1  1 1  { lin incomplete 4 } 10                       % A2 is active
+C7  G 1   1  1 1  { rnd 1  9 1 } 11                             % vipr id 10
+C8  G 1   0       { lin incomplete 10 } 13                      % C7 is active - not only bound constraints are possible with the incomplete keyword
+C9  G 1   0       { uns 6 5  8 7 } 13                           % vipr id 12
 C10 G 1   0       { uns 11 4  12 3 } -1

examples/paper_eg3_weak.vipr

@@ -1,4 +1,5 @@
-% Example 3 in the paper - weak version that needs to be completed prior to verification
+% Example 3 in the paper "Safe and Verified Gomory Mixed Integer Cuts in a Rational MIP Framework"
+% weak version that needs to be completed prior to verification
 VER 1.1
 VAR 2
 x y
@@ -13,14 +14,15 @@ C3  L 3  2  0 -1  1 6
 RTP infeas
 SOL 0
 DER 11
-A1  L 0   1  0 1  { asm } -1
-A2  G 1   1  0 1  { asm } -1
-A3  L 0   1  1 1  { asm } -1
+A1  L 0   1  0 1  { asm } -1                                    % vipr id 3
+A2  G 1   1  0 1  { asm } -1                                    % vipr id 4
+A3  L 0   1  1 1  { asm } -1                                    % vipr id 5
 C4  G 1   0       { lin weak { 2 U 0 3 0 U 1 5 0 } 2  0 1  5 -29/10 } 12 % both A1 and A3 need to be used to complete
-A4  G 1   1  1 1  { asm } -1
-C5  G 1   0       { lin 3  2 -1/3  3 -1/3  7 2 } 12
-C6  G 1/4 1  1 1  { lin weak { 1 L 0 4 1 } 1  1 -1/4 } } 10 % A2 needs to be used to complete
-C7  G 1   1  1 1  { rnd 1  9 1 } 11
+A4  G 1   1  1 1  { asm } -1                                    % vipr id 7
+C5  G 1   0       { lin 3  2 -1/3  3 -1/3  7 2 } 12             % vipr id 8
+C6  G 1/4 1  1 1  { lin weak { 1 L 0 4 1 } 1  1 -1/4 } } 10     % A2 needs to be used to complete
+C7  G 1   1  1 1  { rnd 1  9 1 } 11                             % vipr id 10
 C8  G 1   0       { lin weak { 0 } 3 1 -1/3  2 -1  10 14/3 } 13 % can be completed using only global bounds
-C9  G 1   0       { uns 6 5  8 7 } 13
+C9  G 1   0       { uns 6 5  8 7 } 13                           % vipr id 12
 C10 G 1   0       { uns 11 4  12 3 } -1
+