Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-fast0507.opb |
MD5SUM | 2854384016ebafb26c8bfb47f81aee87 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 63009 |
Biggest coefficient in the objective function | 2 |
Number of bits for the biggest coefficient in the objective function | 2 |
Sum of the numbers in the objective function | 122425 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 2 |
Number of bits of the biggest number in a constraint | 2 |
Biggest sum of numbers in a constraint | 122425 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.16 |
Number of variables | 63009 |
Total number of constraints | 63516 |
Number of constraints which are clauses | 507 |
Number of constraints which are cardinality constraints (but not clauses) | 63009 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 7753 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc3 THE 2005-06-09 07:35:22 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=29242 boxname=wulflinc3 idbench=1026 idsolver=21 numberseed=0 MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2 MD5SUM BENCH: 2854384016ebafb26c8bfb47f81aee87 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-fast0507.opb REAL COMMAND: bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-fast0507.opb IDLAUNCH: 29242 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 865100 kB Buffers: 15200 kB Cached: 133304 kB SwapCached: 756 kB Active: 39960 kB Inactive: 110612 kB HighTotal: 131008 kB HighFree: 34972 kB LowTotal: 903652 kB LowFree: 830128 kB SwapTotal: 2097136 kB SwapFree: 2095332 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5036 kB Slab: 13212 kB Committed_AS: 71796 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-09 07:41:28 (client local time) WITH STATUS 0 IN 366.029 SECONDS stats: 29242 7 366.029 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.84 0.89 0.90 2/54 5657 Raw data (stat): 5657 (runsolver) R 5656 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 908509296 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0004 s] Raw data (loadavg): 0.86 0.89 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 5282 0 0 0 985 12 0 0 25 0 1 0 908509296 33894400 5202 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 8275 5202 1111 63 0 8212 0 vsize: 33100 [startup+20.0011 s] Raw data (loadavg): 0.88 0.90 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 10000 0 0 0 1978 20 0 0 25 0 1 0 908509296 53145600 9920 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12975 9920 1111 63 0 12912 0 vsize: 51900 [startup+30.002 s] Raw data (loadavg): 0.90 0.90 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 14780 0 0 0 2970 27 0 0 25 0 1 0 908509296 72822784 14700 4294967295 134512640 134716908 3221224560 3221222912 134567410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17779 14700 1111 63 0 17716 0 vsize: 71116 [startup+40.0028 s] Raw data (loadavg): 0.91 0.90 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 19586 0 0 0 3963 35 0 0 25 0 1 0 908509296 92532736 19506 4294967295 134512640 134716908 3221224560 3221222788 1077414351 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 22591 19506 1111 63 0 22528 0 vsize: 90364 [startup+50.0036 s] Raw data (loadavg): 0.93 0.91 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 24435 0 0 0 4954 44 0 0 25 0 1 0 908509296 112394240 24355 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 27440 24355 1111 63 0 27377 0 vsize: 109760 [startup+60.0035 s] Raw data (loadavg): 0.94 0.91 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 29338 0 0 0 5945 54 0 0 25 0 1 0 908509296 132370432 29258 4294967295 134512640 134716908 3221224560 3221222788 1077414383 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 32317 29258 1111 63 0 32254 0 vsize: 129268 [startup+70.0033 s] Raw data (loadavg): 0.95 0.91 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 34292 0 0 0 6937 62 0 0 25 0 1 0 908509296 152674304 34212 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 37274 34212 1111 63 0 37211 0 vsize: 149096 [startup+80.0042 s] Raw data (loadavg): 0.95 0.91 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 39311 0 0 0 7928 71 0 0 25 0 1 0 908509296 173281280 39231 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 42305 39231 1111 63 0 42242 0 vsize: 169220 [startup+90.004 s] Raw data (loadavg): 0.96 0.92 0.90 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 44391 0 0 0 8921 78 0 0 25 0 1 0 908509296 194035712 44311 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 47372 44311 1111 63 0 47309 0 vsize: 189488 [startup+100.005 s] Raw data (loadavg): 0.97 0.92 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 49547 0 0 0 9912 87 0 0 25 0 1 0 908509296 215232512 49467 4294967295 134512640 134716908 3221224560 3221222788 1077414358 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 52547 49467 1111 63 0 52484 0 vsize: 210188 [startup+110.006 s] Raw data (loadavg): 0.97 0.92 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 54743 0 0 0 10904 96 0 0 25 0 1 0 908509296 236584960 54663 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 57760 54663 1111 63 0 57697 0 vsize: 231040 [startup+120.005 s] Raw data (loadavg): 0.98 0.92 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 60012 0 0 0 11896 103 0 0 25 0 1 0 908509296 258080768 59932 4294967295 134512640 134716908 3221224560 3221222788 1077414435 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 63008 59932 1111 63 0 62945 0 vsize: 252032 [startup+130.005 s] Raw data (loadavg): 0.98 0.92 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 65414 0 0 0 12888 112 0 0 25 0 1 0 908509296 280178688 65334 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 68403 65334 1111 63 0 68340 0 vsize: 273612 [startup+140.006 s] Raw data (loadavg): 0.98 0.93 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 70841 0 0 0 13878 121 0 0 25 0 1 0 908509296 302424064 70761 4294967295 134512640 134716908 3221224560 3221222788 1077414408 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 73834 70761 1111 63 0 73771 0 vsize: 295336 [startup+150.007 s] Raw data (loadavg): 0.98 0.93 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 76330 0 0 0 14871 129 0 0 25 0 1 0 908509296 324972544 76250 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 79339 76250 1111 63 0 79276 0 vsize: 317356 [startup+160.007 s] Raw data (loadavg): 0.99 0.93 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 81890 0 0 0 15862 139 0 0 25 0 1 0 908509296 347664384 81810 4294967295 134512640 134716908 3221224560 3221222788 1077414360 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 84879 81810 1111 63 0 84816 0 vsize: 339516 [startup+170.007 s] Raw data (loadavg): 0.99 0.93 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 87535 0 0 0 16853 148 0 0 25 0 1 0 908509296 370802688 87455 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 90528 87455 1111 63 0 90465 0 vsize: 362112 [startup+180.007 s] Raw data (loadavg): 0.99 0.93 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 93265 0 0 0 17843 158 0 0 25 0 1 0 908509296 394248192 93185 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 96252 93185 1111 63 0 96189 0 vsize: 385008 [startup+190.007 s] Raw data (loadavg): 0.99 0.93 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 99110 0 0 0 18833 168 0 0 25 0 1 0 908509296 418357248 99030 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 102138 99030 1111 63 0 102075 0 vsize: 408552 [startup+200.008 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 105058 0 0 0 19823 179 0 0 25 0 1 0 908509296 442687488 104978 4294967295 134512640 134716908 3221224560 3221222788 1077414376 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 108078 104978 1111 63 0 108015 0 vsize: 432312 [startup+210.009 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 111124 0 0 0 20812 189 0 0 25 0 1 0 908509296 467472384 111044 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 114129 111044 1111 63 0 114066 0 vsize: 456516 [startup+220.009 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 117328 0 0 0 21802 199 0 0 25 0 1 0 908509296 492855296 117248 4294967295 134512640 134716908 3221224560 3221222912 134567410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 120326 117248 1111 63 0 120263 0 vsize: 481304 [startup+230.01 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 123709 0 0 0 22792 209 0 0 25 0 1 0 908509296 518983680 123629 4294967295 134512640 134716908 3221224560 3221222788 1077414420 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 126705 123629 1111 63 0 126642 0 vsize: 506820 [startup+240.012 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 130138 0 0 0 23783 219 0 0 25 0 1 0 908509296 545406976 130058 4294967295 134512640 134716908 3221224560 3221222912 134567410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 133156 130058 1111 63 0 133093 0 vsize: 532624 [startup+250.013 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 136666 0 0 0 24771 231 0 0 25 0 1 0 908509296 572137472 136586 4294967295 134512640 134716908 3221224560 3221222788 1077414374 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 139682 136586 1111 63 0 139619 0 vsize: 558728 [startup+260.013 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 143314 0 0 0 25760 243 0 0 25 0 1 0 908509296 599310336 143234 4294967295 134512640 134716908 3221224560 3221222912 134567410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 146316 143234 1111 63 0 146253 0 vsize: 585264 [startup+270.013 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 150115 0 0 0 26749 254 0 0 25 0 1 0 908509296 627232768 150035 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 153133 150035 1111 63 0 153070 0 vsize: 612532 [startup+280.014 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 157047 0 0 0 27737 266 0 0 25 0 1 0 908509296 655593472 156967 4294967295 134512640 134716908 3221224560 3221222788 1077414435 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 160057 156967 1111 63 0 159994 0 vsize: 640228 [startup+290.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 164092 0 0 0 28725 278 0 0 25 0 1 0 908509296 684412928 164012 4294967295 134512640 134716908 3221224560 3221222788 1077414345 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 167093 164012 1111 63 0 167030 0 vsize: 668372 [startup+300.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 171440 0 0 0 29711 292 0 0 25 0 1 0 908509296 714420224 171360 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 174419 171360 1111 63 0 174356 0 vsize: 697676 [startup+310.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 179043 0 0 0 30699 304 0 0 25 0 1 0 908509296 745631744 178963 4294967295 134512640 134716908 3221224560 3221222788 1077414385 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 182039 178963 1111 63 0 181976 0 vsize: 728156 [startup+320.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 187253 0 0 0 31686 317 0 0 25 0 1 0 908509296 779223040 187173 4294967295 134512640 134716908 3221224560 3221222788 1077414351 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 190240 187173 1111 63 0 190177 0 vsize: 760960 [startup+330.017 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 195586 0 0 0 32670 333 0 0 25 0 1 0 908509296 813629440 195506 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 198640 195506 1111 63 0 198577 0 vsize: 794560 [startup+340.017 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 204044 0 0 0 33656 347 0 0 25 0 1 0 908509296 848265216 203964 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 207096 203964 1111 63 0 207033 0 vsize: 828384 [startup+350.018 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 212759 0 0 0 34642 362 0 0 25 0 1 0 908509296 883949568 212679 4294967295 134512640 134716908 3221224560 3221222788 1077414407 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 215808 212679 1111 63 0 215745 0 vsize: 863232 [startup+360.017 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 221948 0 0 0 35622 381 0 0 25 0 1 0 908509296 921571328 221399 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 224993 221399 1111 63 0 224930 0 vsize: 899972 [startup+366.002 s] Raw data (loadavg): 0.99 0.96 0.91 1/53 5657 Raw data (stat): 5657 (bsolo_lpr_cuts-) R 5656 20224 20223 0 -1 0 221948 0 0 0 35622 381 0 0 25 0 1 0 908509296 921571328 221399 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 224993 221399 1111 63 0 224930 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 366.002 CPU time (s): 366.029 CPU user time (s): 361.647 CPU system time (s): 4.38233 CPU usage (%): 100.008 Max. virtual memory (Kb): 899972 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####