legacy/oldnonlinear/nonlinear/test_ineq.hl

   1 (*  tests of nonlinear inequalities from ineq.hl *)
   2 (* removed from glpk model OXLZLEZ *)
   3
   4 let do_betas x = all_forall (snd(dest_eq(concl(BETAS_CONV x))));;
   5 let all_forall  =Sphere.all_forall;;
   6
   7
   8
   9 (*
  10 let mk_tm23 i3 i5 i6 =
  11   let x i = List.nth [`&2`; `&2 * hminus`; `&2 * hplus` ; `sqrt8`] i in
  12   let X i = x (i+1) in
  13   let mid i = if (i=1) then 1 else 0 in
  14   let m = mk_small_numeral in
  15   let w1 = 1 +  mid i6 in
  16   let w2 = 1 + mid i3 + mid i5 in
  17     list_mk_comb (template23, [x i3;X i3; x i5;X i5; x i6 ;X i6; m w1; m w2]);;
  18
  19 let mk_ineq23 i3 i5 i6 = all_forall (snd(dest_eq(concl(BETAS_CONV (mk_tm23 i3 i5 i6)))));;
  20
  21 let add23 i3 i5 i6 =
  22   add {
  23     id = Printf.sprintf "ZTGIJCF23 %d %d %d 7907792228" i3 i5 i6;
  24     ineq = mk_ineq23 i3 i5 i6;
  25     doc = "This is the 2&3-cell inequality for five or more leaves.";
  26     tags = [Cfsqp;Flypaper];
  27   };;
  28
  29  for i3=0 to 2 do
  30  for i5 = 0 to 2 do
  31  for i6 = 0 to 2 do
  32    add23 i3 i5 i6 done done done;;
  33 *)
  34
  35
  36 let _ =
  37 {
  38   id = "QITNPEA 9507854632";
  39   ineq = all_forall `ineq
  40    [(&2 * hminus,y1, &2 * hplus);
  41     (&2,y2, &2 * hminus);
  42     (&2,y3, &2 * hminus);
  43     (#2 ,y4, #2.1);
  44     (&2,y5, &2 * hminus);
  45     (&2,y6, &2 * hminus)
  46    ]
  47     ((gamma23f y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #0.00242
  48     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
  49     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
  50     (eta_y y1 y2 y6 > sqrt2 ) \/
  51     (eta_y y1 y3 y5 > sqrt2))`;
  52   doc =   "
  53      Note the upper bound on $y_4$ is $2.1$.
  54      This is an inequality for $23$-cells used to prove the cluster inequality.";
  55   tags = [Tex;Cfsqp;Clusterlp];
  56 };;
  57
  58 let _ =
  59 {
  60   id = "QITNPEA 9507854632";
  61   ineq = all_forall `ineq
  62    [(&2 * hminus,y1, &2 * hplus);
  63     (&2,y2, &2 * hminus);
  64     (&2,y3, &2 * hminus);
  65     (#2 ,y4, #2.1);
  66     (&2,y5, &2 * hminus);
  67     (&2,y6, &2 * hminus)
  68    ]
  69     ((gamma23f y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #0.00242
  70     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
  71     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
  72     (eta_y y1 y2 y6 > sqrt2 ) \/
  73     (eta_y y1 y3 y5 > sqrt2))`;
  74   doc =   "
  75      Note the upper bound on $y_4$ is $2.1$.  The same inequality holds when
  76     $y_4\\ge 2.1$.  In fact, \\ineq{4003532128} is even stronger.
  77      This is an inequality for $23$-cells used to prove the cluster inequality.";
  78   tags = [Tex;Cfsqp;Clusterlp];
  79 };;
  80
  81 test_ineq {
  82   id = "2";
  83   ineq = all_forall `ineq
  84    [(&2 * hminus,y1, &2 * hplus);
  85     (&2,y2, &2 * hminus);
  86     (&2,y3, &2 * hminus);
  87     (#2 ,y4, &2 * hminus);
  88     (&2,y5, &2 * hminus);
  89     (&2,y6, &2 * hminus)
  90    ]
  91   ( (gamma4f y1 y2 y3 y4 y5 y6 lmfun > #0.0) \/
  92     (dih_y y1 y2 y3 y4 y5 y6 < #1.575) )`;
  93   doc =   "test";
  94   tags = [];
  95 };;
  96
  97 let _ =
  98 {
  99   id = "QITNPEA 4 blades, 3 quarters, 1 23-cell";
 100   ineq = all_forall `ineq
 101    [(&2 * hminus,y1, &2 * hplus);
 102     (&2,y2, &2 * hminus);
 103     (&2,y3, &2 * hminus);
 104     (&2,y4, sqrt8);
 105     (&2,y5, &2 * hminus);
 106     (&2,y6, &2 * hminus);
 107     (&2,y7, &2 * hminus);
 108     (&2,y8, &2 * hminus);
 109     (&2,y9, &2 * hminus);
 110     (&2,y10, &2 * hminus);
 111     (&2,y11, &2 * hminus);
 112     (&2,y12, &2 * hminus);
 113     (&2,y13, &2 * hminus)
 114    ]
 115     ((gamma23f y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun
 116     + gamma4f y1 y3 y7 y9 y12 y5 lmfun
 117     + gamma4f y1 y7 y8 y10 y13 y12  lmfun
 118     + gamma4f y1 y8 y2 y11 y6 y13  lmfun > #0.0) \/
 119      (
 120     dih_y y1 y2 y3 y4 y5 y6
 121     + dih_y y1 y3 y7 y9 y12 y5
 122     + dih_y y1 y7 y8 y10 y13 y12
 123     + dih_y y1 y8 y2 y11 y6 y13   < &2 * pi
 124       ) \/
 125      (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2))`;
 126   doc =   "
 127      This is a numerical test of the 4-blade inequality in the case of three quarters
 128      and one 23-cell.  It is too large to be directly checked by rigorous nonlinear
 129      optimization. Instead it is broken into smaller pieces.";
 130   tags = [Cfsqp;Clusterlp;Derived];
 131 };;
 132
 133 let _ =
 134 {
 135   id = "OCTAHEDRON OXLZLEZ TEST 4 blades, 3 quarters, 1 4-cell wt 1/2";
 136   ineq = all_forall `ineq
 137    [(&2 * hminus,y1, &2 * hplus);
 138     (&2,y2, &2 * hminus);
 139     (&2,y3, &2 * hminus);
 140     (&2 * hminus ,y4,  &2 *hplus);
 141     (&2,y5, &2 * hminus);
 142     (&2,y6, &2 * hminus);
 143     (&2,y7, &2 * hminus);
 144     (&2,y8, &2 * hminus);
 145     (&2,y9, &2 * hminus);
 146     (&2,y10, &2 * hminus);
 147     (&2,y11, &2 * hminus);
 148     (&2,y12, &2 * hminus);
 149     (&2,y13, &2 * hminus)
 150    ]
 151     ((gamma4f y1 y2 y3 y4 y5 y6 lmfun / &2 + beta_bump_force_y y1 y2 y3 y4 y5 y6
 152     + gamma4f y1 y3 y7 y9 y12 y5 lmfun
 153     + gamma4f y1 y7 y8 y10 y13 y12  lmfun
 154     + gamma4f y1 y8 y2 y11 y6 y13  lmfun > #0.0) \/
 155      (
 156     dih_y y1 y2 y3 y4 y5 y6
 157     + dih_y y1 y3 y7 y9 y12 y5
 158     + dih_y y1 y7 y8 y10 y13 y12
 159     + dih_y y1 y8 y2 y11 y6 y13   > &2 * pi
 160       ) \/
 161     (
 162     dih_y y1 y2 y3 y4 y5 y6
 163     + dih_y y1 y3 y7 y9 y12 y5
 164     + dih_y y1 y7 y8 y10 y13 y12
 165     + dih_y y1 y8 y2 y11 y6 y13   < &2 * pi - #0.002
 166       ) )`;
 167   doc =   "
 168      This is a numerical test of the 4-blade inequality in the case of three quarters
 169      and one 4-cell of wt 1/2.
 170      This is the most important case of the inequality.
 171      It is too large to be directly checked by rigorous nonlinear
 172      optimization. Instead it is broken into smaller pieces.";
 173   tags = [Cfsqp;Clusterlp;Derived];
 174 };;
 175
 176
 177 let _ =
 178 {
 179 id = "3611774025";
 180 ineq = all_forall `ineq
 181 [
 182 (&2, x12, &2 * h0);
 183 (&2, x13, &2 * h0);
 184 (&2, x14, &2 * h0);
 185 (&2, x15, &2 * h0);
 186 (&2, x23, &2 * h0);
 187 (&2, x24, &2 * h0);
 188 (&2, x25, &2 * h0);
 189 (&2, x34, &2 * h0);
 190 (&2, x35, &2 * h0);
 191 (&2, x45, &2 * h0)
 192 ]
 193   (cayleyR x12 x13 x14 x15  x23 x24 x25  x34 x35 x45 < &0)`;
 194 tags = [];
 195 doc = "A Cayley Menger determinant is positive. This was part of Local Fan, but
 196   is no longer needed.";
 197 };;
 198
 199
 200 (*
 201 let I_1965189142=
 202 all_forall `ineq
 203 [(#1.0,h,#1.26);
 204  (#3.0,k,#34.0)]
 205  (#0.591 - #0.0331 *k + #0.506 * lmfun h <=
 206    regular_spherical_polygon_area (cos (acs (h/ &2) - pi/ &6)) k)`;;
 207
 208
 209
 210
 211 let I_6096597438=
 212 all_forall `ineq
 213  [(#3.0,k,#64.0)]
 214  (#1.591 - #0.0331 *k + #0.506 * lmfun (#1.0) <=
 215    regular_spherical_polygon_area (cos (#0.797)) k)`;;
 216
 217 *)
 218
 219 let ZZ = ();;
 220
 221
 222
 223
 224
 225
 226
 227
 228 add {
 229   id = "8082208587";
 230   doc="We can use extremal edge properties and the tame table D calculations
 231     to reduce to the case where $y_4=\\sqrt8$ and $y_5,y_6$ are extremal.";
 232   tags = [Cfsqp;Lp;Tex];
 233   ineq = all_forall `ineq
 234   [
 235   (&2,y1,#2.52);
 236   (&2,y2,#2.52);
 237   (&2,y3,#2.52);
 238   (#2.52,y5,sqrt8);
 239   (&2,y6,#2.52)
 240   ]
 241 (taum y1 y2 y3 sqrt8 y5 y6 > #0.2759)`;
 242 };;
 243
 244
 245 add {
 246   id = "9620775909";
 247   doc="We can use dimension reduction methods to simplify this inequality.";
 248   tags = [Cfsqp;Lp;Tex;Penalty(5.0,500.0)];
 249   ineq = all_forall `ineq
 250   [
 251   (&2,y1,#2.52);
 252   (&2,y2,#2.52);
 253   (&2,y3,#2.52);
 254   (sqrt8,y4,&2 * #2.52);
 255   (#2.52,y5,sqrt8);
 256   (&2,y6,#2.52);
 257   (&2,y7,#2.52);
 258   (&2,y8,#2.52);
 259   (&2,y9,#2.52)
 260   ]
 261 ((tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.492) \/
 262   (enclosed  y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ))`;
 263 };;
 264
 265 add {
 266  id = "test";
 267  doc = "";
 268  tags=[];
 269  ineq = all_forall `ineq
 270  [
 271   (&2,y1,#2.52);
 272   (&2,y2,#2.52);
 273   (&2,y3,#2.52);
 274   (&2,y4,#2.52);
 275   (#2.52,y5,sqrt8)
 276  ]
 277  (taum y1 y2 y3 y4 y5 sqrt8 > #0.3493)`;
 278 };;
 279
 280 add {
 281  id = "test";
 282  doc = "";
 283  tags=[];
 284  ineq = all_forall `ineq
 285  [
 286   (&2,y1,#2.52);
 287   (&2,y2,#2.52);
 288   (&2,y3,#2.52);
 289   (&2,y4,#2.52);
 290   (#2.52,y5,sqrt8)
 291  ]
 292  (taum y1 y2 y3 y4 y5 sqrt8 > #0.3493)`;
 293 };;
 294
 295 add {
 296   id = "9620775909 fake";
 297   doc="For reference only:
 298     We can use dimension reduction methods to simplify this inequality.
 299    The constant was 0.492.";
 300   tags = [Cfsqp;Lp;Tex;Penalty(5.0,500.0)];
 301   ineq = all_forall `ineq
 302   [
 303   (&2,y1,#2.52);
 304   (&2,y2,#2.52);
 305   (&2,y3,#2.52);
 306   (sqrt8,y4,&2 * #2.52);
 307   (#2.52,y5,sqrt8);
 308   (&2,y6,#2.52);
 309   (&2,y7,#2.52);
 310   (&2,y8,#2.52);
 311   (&2,y9,#2.52)
 312   ]
 313 ((tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.492) \/
 314   (enclosed  y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ))`;
 315 };;
 316
 317
 318
 319
 320
 321 let profile_apex5_d = new_definition
 322   `profile_apex5_d r s = tame_table_d (r-1) (s+1)`;;
 323
 324 let profile_std56_flat_free_d = new_definition
 325   `profile_std56_flat_free_d r s = if (r,s) = (6,0) then #0.91 else
 326      (&2 - &s)* #0.128 + (&r + &2 * &s - &4) * #0.44`;;
 327
 328 let profile_apex4_d = new_definition
 329   `profile_apex4_d r s = if (r,s)=(4,0) then #0.4773 else #0.3493`;;
 330
 331 add {
 332  id = "";
 333  doc = "";
 334  tags=[];
 335  ineq = all_forall `ineq
 336  [
 337   (&2,y1,#2.52);
 338   (&2,y2,#2.52);
 339   (&2,y3,#2.52);
 340   (&2,y4,#2.52);
 341   (#2.52,y5,sqrt8)
 342  ]
 343  (taum y1 y2 y3 y4 y5 sqrt8 > #0.3493)`;
 344 };;
 345
 346 (* In lp2009 but not graph0 *)
 347
 348 (*
 349 let I_3336871894=
 350  all_forall `ineq
 351     [
 352       (#2.0,y1,#2.52);
 353       (#2.0,y2,#2.52);
 354       (#2.0,y3,#2.52);
 355       (#2.0,y4,#2.52);
 356       (#2.0,y5,#2.52);
 357       (#2.0,y6,#2.52)]
 358 ( taum y1 y2 y3 y4 y5 y6 >= #0.0)`;;
 359
 360 let I_8880534953=
 361  all_forall `ineq
 362     [
 363       (#2.0,y1,#2.52);
 364       (#2.0,y2,#2.52);
 365       (#2.0,y3,#2.52);
 366       (#2.0,y4,#2.52);
 367       (#2.52,y5,sqrt8);
 368       (#2.52,y6,sqrt8)]
 369 ( taum y1 y2 y3 y4 y5 y6 -  #0.2759 > #0.0)`;;
 370 *)
 371
 372 (* These are inequalities found in the lp2009.cc file
 373    that were not found in the graph0.mod file *)
 374
 375 (*
 376 add {
 377   id = "5769230427";
 378   doc="deprecated and false";
 379   tags = [Cfsqp];
 380   ineq =  all_forall `ineq
 381     [
 382       (#2.0,y1,#2.52);
 383       (#2.0,y2,#2.52);
 384       (#2.0,y3,#2.52);
 385       (#2.0,y4,#2.52);
 386       (#3.0,y5,#3.3);
 387       (#2.0,y6,#2.52)]
 388 ( (taum y1 y2 y3 y4 y5 y6) -
 389   #0.231 - (#0.622 * (dih_y y1 y2 y3 y4 y5 y6))
 390   - (#2.09 / #2.0) - ((#0.54 / #2.0) * (y1 - #2.0))
 391   + (#0.578 * (y2 + y6 - #4.0))  > #0.0)`;
 392 };;
 393 *)
 394
 395
 396
 397
 398 (*found in lp2009 but not graph0 *)
 399
 400 let I_5464178191=
 401  all_forall `ineq[
 402       (#2.0,y1,#2.52);
 403       (#2.0,y2,#2.52);
 404       (#2.0,y3,#2.52);
 405       (#2.52,y4,#5.04);
 406       (#2.0,y5,#2.52);
 407       (#2.0,y6,#2.52);
 408       (#2.0,y7,#2.52);
 409       (#2.0,y8,#2.52);
 410       (#2.0,y9,#2.52)]
 411 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 - #0.206 > #0.0) \/
 412 ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #2.52 ) \/
 413 ( delta_y y1 y2 y3 y4 y5 y6 < &0) \/
 414 ( delta_y y7 y2 y3 y4 y8 y9 < &0))`;;
 415
 416
 417 (*
 418
 419 add {
 420   id = "181212899";
 421   doc="This original version of the inequality. There are six derived versions.";
 422   tags = [Cfsqp;Tex];
 423   ineq =  all_forall `ineq[
 424       (#2.0, y1, #2.52);
 425       (#2.0, y2, #2.52);
 426       (#2.0, y3, #2.52);
 427       (#2.52, y4, sqrt8);
 428       (#2.0, y5, #2.52);
 429       (#2.52, y6, sqrt8)]
 430 (dih_y y1 y2 y3 y4 y5 y6 - #1.448 -
 431 (#0.266 * (y1 - #2.0)) +
 432 (#0.295 * (y2 - #2.0)) +
 433 (#0.57 * (y3 - #2.0)) -
 434 (#0.745 * (y4 - #2.52)) +
 435 (#0.268 * (y5 - #2.0)) +
 436 (#0.385 * (y6 - #2.52)) > #0.0)`;
 437 };;
 438
 439 *)
 440
 441
 442 let iqd s dart sym t =
 443   let c = mk_mconst (dart,tyR) in {
 444   id = s;
 445   doc = "";
 446   tags = [Cfsqp;Lp;] @ (if sym then [Lpsymmetry] else []);
 447   ineq = Ineq.mk_tplate templateC (c:: t);
 448 };;
 449
 450 1;;
 451
 452 let mk_QITNPEA' i3 i4 i5 i6  =
 453   let template = `\ y3m y3M y4m y4M y5m y5M y6m y6M w m. ineq
 454    [(&2 * hminus, y1, &2 * hplus);
 455     (&2 ,y2, &2 *hminus);
 456     (y3m,y3,y3M);
 457     (y4m,y4,y4M);
 458     (y5m,y5,y5M);
 459     (y6m,y6,y6M)]
 460     ((gamma4f y1 y2 y3 y4 y5 y6 lmfun / &w + &m *beta_bump_y y1 y2 y3 y4 y5 y6
 461         - #0.0105256 +  #0.00522841*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
 462     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))` in
 463   let x i = List.nth [`&2`; `&2 * hminus`; `sqrt8`] i in
 464   let X i = x (i+1) in
 465   let mid i = if (i=1) then 1 else 0 in
 466   let w = 1 + mid i3 + mid i4 + mid i5 + mid i6 in
 467   let m = if (w =2) && (i4 = 1) then `1` else `0` in
 468  Ineq.mk_tplate template [x i3;X i3; x i4;X i4; x i5;X i5; x i6 ;X i6; mk_small_numeral w; m];;
 469
 470 add {
 471     id =  "QITNPEA test";
 472     ineq = mk_QITNPEA' 0 1 0 0;
 473     doc = "This is a $4$-cell (nonquarter) inequality for four blades.";
 474     tags = [Cfsqp;Flypaper;Penalty(50.0,500.0)];
 475   };;
 476
 477 let add = Parse_ineq.execute_cfsqp;;
 478
 479
 480