Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-gt2.opb |
MD5SUM | f1382105ee9fb79777762a53cf6a73c1 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 21166 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 304 |
Biggest coefficient in the objective function | 62376 |
Number of bits for the biggest coefficient in the objective function | 16 |
Sum of the numbers in the objective function | 3092598 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 62376 |
Number of bits of the biggest number in a constraint | 16 |
Biggest sum of numbers in a constraint | 3092598 |
Number of bits of the biggest sum of numbers | 22 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.14 |
Number of variables | 556 |
Total number of constraints | 217 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 26 |
Number of constraints which are nor clauses,nor cardinality constraints | 191 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 48 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-21 15:02:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18436 boxname=wulflinc31 idbench=1419 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: f1382105ee9fb79777762a53cf6a73c1 /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-gt2.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-gt2.opb IDLAUNCH: 18436 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 893360 kB Buffers: 24224 kB Cached: 96284 kB SwapCached: 1076 kB Active: 58368 kB Inactive: 64496 kB HighTotal: 131008 kB HighFree: 65996 kB LowTotal: 903652 kB LowFree: 827364 kB SwapTotal: 2097892 kB SwapFree: 2095984 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5356 kB Slab: 12832 kB Committed_AS: 63860 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-21 15:07:43 (client local time) WITH STATUS 0 IN 330.231 SECONDS stats: 18436 7 330.231 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c Initial problem consists of 556 variables and 180 constraints. c After prepocess the problem consists of 556 variables and 193 constraints. c preprocess terminated 0.777 s c Initial Lower Bound: 17011 c Lower Bound Elapsed time: 0.1008 c Use computed LB before first solution. c NEW SOLUTION FOUND: 267669 @ 22.109 c NEW SOLUTION FOUND: 262111 @ 24.574 c NEW SOLUTION FOUND: 261469 @ 24.72 c Warning: NO Unit Constraints after backtrack?? Continuing Execution.... c NEW SOLUTION FOUND: 260717 @ 45.033 c NEW SOLUTION FOUND: 257617 @ 46.632 c Warning: NO Unit Constraints after backtrack?? Continuing Execution.... c NEW SOLUTION FOUND: 255169 @ 107.432 c NEW SOLUTION FOUND: 254507 @ 107.461 #### 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 Raw data (loadavg): 0.84 0.99 0.99 2/55 12061 Raw data (stat): 12061 (runsolver) R 12060 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 805219536 1056768 100 4294967295 134512640 135381576 3221221680 3221216896 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 1032 [startup+10.0008 s] Raw data (loadavg): 0.87 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 3178 0 0 0 986 10 0 0 25 0 1 0 805219536 11984896 2240 4294967295 134512640 134714508 3221221776 3221219560 1077410205 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 2926 2240 1111 63 0 2863 0 vsize: 11704 [startup+20.0016 s] Raw data (loadavg): 0.89 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 3179 0 0 0 1985 11 0 0 25 0 1 0 805219536 11984896 2241 4294967295 134512640 134714508 3221221776 3221219980 1074152822 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 2926 2241 1111 63 0 2863 0 vsize: 11704 [startup+30.0019 s] Raw data (loadavg): 0.90 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 11201 0 0 0 2956 39 0 0 25 0 1 0 805219536 13971456 2728 4294967295 134512640 134714508 3221221776 3221219440 1074866649 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 3485 2731 1111 63 0 3422 0 vsize: 13644 [startup+40.0025 s] Raw data (loadavg): 0.92 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 25039 0 0 0 3913 82 0 0 25 0 1 0 805219536 15945728 3147 4294967295 134512640 134714508 3221221776 3221218016 1075115709 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 3893 3147 1111 63 0 3830 0 vsize: 15572 [startup+50.0024 s] Raw data (loadavg): 0.93 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 37930 0 0 0 4876 119 0 0 25 0 1 0 805219536 17178624 3515 4294967295 134512640 134714508 3221221776 3221220192 1074116570 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 4194 3515 1111 63 0 4131 0 vsize: 16776 [startup+60.0031 s] Raw data (loadavg): 0.94 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 49973 0 0 0 5840 156 0 0 25 0 1 0 805219536 19410944 3979 4294967295 134512640 134714508 3221221776 3221218852 1075863600 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 4739 3979 1111 63 0 4676 0 vsize: 18956 [startup+70.0033 s] Raw data (loadavg): 0.95 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 64684 0 0 0 6802 195 0 0 25 0 1 0 805219536 20455424 4243 4294967295 134512640 134714508 3221221776 3221217788 1074788959 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 4994 4243 1111 63 0 4931 0 vsize: 19976 [startup+80.0032 s] Raw data (loadavg): 0.96 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 78986 0 0 0 7762 234 0 0 25 0 1 0 805219536 22167552 4709 4294967295 134512640 134714508 3221221776 3221218016 1075115715 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 5412 4709 1111 63 0 5349 0 vsize: 21648 [startup+90.0056 s] Raw data (loadavg): 0.96 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 95110 0 0 0 8721 276 0 0 25 0 1 0 805219536 22507520 4822 4294967295 134512640 134714508 3221221776 3221219776 1074918583 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 5495 4822 1111 63 0 5432 0 vsize: 21980 [startup+100.005 s] Raw data (loadavg): 0.97 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 108937 0 0 0 9687 309 0 0 25 0 1 0 805219536 23830528 5027 4294967295 134512640 134714508 3221221776 3221219416 1075850409 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 5818 5027 1111 63 0 5755 0 vsize: 23272 [startup+110.008 s] Raw data (loadavg): 0.97 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 125461 0 0 0 10646 350 0 0 25 0 1 0 805219536 25423872 5534 4294967295 134512640 134714508 3221221776 3221220024 1074138155 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 6207 5534 1111 63 0 6144 0 vsize: 24828 [startup+120.009 s] Raw data (loadavg): 0.98 0.99 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 141824 0 0 0 11607 390 0 0 25 0 1 0 805219536 26984448 5915 4294967295 134512640 134714508 3221221776 3221220236 1077781665 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 6588 5915 1111 63 0 6525 0 vsize: 26352 [startup+130.009 s] Raw data (loadavg): 1.05 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 159317 0 0 0 12564 433 0 0 25 0 1 0 805219536 28663808 6233 4294967295 134512640 134714508 3221221776 3221219240 1074950096 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 6899 6225 1111 63 0 6836 0 vsize: 27992 [startup+140.01 s] Raw data (loadavg): 1.04 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 172723 0 0 0 13531 466 0 0 25 0 1 0 805219536 29245440 6466 4294967295 134512640 134714508 3221221776 3221219708 1077411564 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 7140 6466 1111 63 0 7077 0 vsize: 28560 [startup+150.01 s] Raw data (loadavg): 1.04 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 187277 0 0 0 14494 504 0 0 25 0 1 0 805219536 29913088 6597 4294967295 134512640 134714508 3221221776 3221220064 1074153782 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 7303 6597 1111 63 0 7240 0 vsize: 29212 [startup+160.011 s] Raw data (loadavg): 1.03 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 207795 0 0 0 15443 555 0 0 25 0 1 0 805219536 31309824 6970 4294967295 134512640 134714508 3221221776 3221219504 1075830006 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 7644 6970 1111 63 0 7581 0 vsize: 30576 [startup+170.012 s] Raw data (loadavg): 1.03 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 228381 0 0 0 16395 603 0 0 25 0 1 0 805219536 34283520 7673 4294967295 134512640 134714508 3221221776 3221218968 1074138315 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 8370 7673 1111 63 0 8307 0 vsize: 33480 [startup+180.012 s] Raw data (loadavg): 1.02 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 240399 0 0 0 17360 638 0 0 25 0 1 0 805219536 34611200 7688 4294967295 134512640 134714508 3221221776 3221218368 1074885298 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 8450 7688 1111 63 0 8387 0 vsize: 33800 [startup+190.012 s] Raw data (loadavg): 1.02 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 254996 0 0 0 18325 674 0 0 25 0 1 0 805219536 35049472 7852 4294967295 134512640 134714508 3221221776 3221219976 1074138265 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 8557 7852 1111 63 0 8494 0 vsize: 34228 [startup+200.012 s] Raw data (loadavg): 1.01 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 264376 0 0 0 19301 698 0 0 25 0 1 0 805219536 35495936 7992 4294967295 134512640 134714508 3221221776 3221220012 1077404781 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 8666 7992 1111 63 0 8603 0 vsize: 34664 [startup+210.013 s] Raw data (loadavg): 1.01 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 282063 0 0 0 20254 745 0 0 25 0 1 0 805219536 36679680 8281 4294967295 134512640 134714508 3221221776 3221219688 1074138300 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 8955 8281 1111 63 0 8892 0 vsize: 35820 [startup+220.012 s] Raw data (loadavg): 1.01 1.00 0.99 2/55 12061 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 302929 0 0 0 21201 798 0 0 25 0 1 0 805219536 37818368 8559 4294967295 134512640 134714508 3221221776 3221220000 1074143973 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 9233 8559 1111 63 0 9170 0 vsize: 36932 [startup+230.012 s] Raw data (loadavg): 1.01 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 311661 0 0 0 22181 819 0 0 25 0 1 0 805219536 39399424 8942 4294967295 134512640 134714508 3221221776 3221219776 1074918583 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 9619 8942 1111 63 0 9556 0 vsize: 38476 [startup+240.014 s] Raw data (loadavg): 1.01 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 324278 0 0 0 23151 849 0 0 25 0 1 0 805219536 40652800 9171 4294967295 134512640 134714508 3221221776 3221217660 1074788953 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 9925 9171 1111 63 0 9862 0 vsize: 39700 [startup+250.014 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 336902 0 0 0 24119 881 0 0 25 0 1 0 805219536 40157184 9130 4294967295 134512640 134714508 3221221776 3221220064 1074153782 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 9805 9131 1111 63 0 9742 0 vsize: 39216 [startup+260.014 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 346335 0 0 0 25095 905 0 0 25 0 1 0 805219536 41504768 9162 4294967295 134512640 134714508 3221221776 3221218816 1075971395 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 10133 9168 1111 63 0 10070 0 vsize: 40532 [startup+270.015 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 356619 0 0 0 26069 931 0 0 25 0 1 0 805219536 40394752 9188 4294967295 134512640 134714508 3221221776 3221220560 134622318 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 9862 9188 1111 63 0 9799 0 vsize: 39448 [startup+280.015 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 370889 0 0 0 27035 965 0 0 25 0 1 0 805219536 40394752 9188 4294967295 134512640 134714508 3221221776 3221219776 1074056269 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 9862 9188 1111 63 0 9799 0 vsize: 39448 [startup+290.015 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 378848 0 0 0 28016 985 0 0 25 0 1 0 805219536 41971712 9447 4294967295 134512640 134714508 3221221776 3221217744 1074872824 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 10247 9447 1111 63 0 10184 0 vsize: 40988 [startup+300.015 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 389747 0 0 0 28988 1013 0 0 25 0 1 0 805219536 42995712 9527 4294967295 134512640 134714508 3221221776 3221218896 1074834431 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 10497 9527 1111 63 0 10434 0 vsize: 41988 [startup+310.017 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 404539 0 0 0 29951 1049 0 0 25 0 1 0 805219536 43057152 9668 4294967295 134512640 134714508 3221221776 3221218112 1075114265 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 10512 9668 1111 63 0 10449 0 vsize: 42048 [startup+320.017 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 414136 0 0 0 30929 1072 0 0 25 0 1 0 805219536 43732992 9866 4294967295 134512640 134714508 3221221776 3221218016 1075115768 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 10677 9866 1111 63 0 10614 0 vsize: 42708 [startup+330.016 s] Raw data (loadavg): 1.00 1.00 0.99 2/55 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 425636 0 0 0 31899 1102 0 0 25 0 1 0 805219536 44163072 9964 4294967295 134512640 134714508 3221221776 3221218004 1075115057 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 10782 9964 1111 63 0 10719 0 vsize: 43128 [startup+330.229 s] Raw data (loadavg): 1.00 1.00 0.99 1/54 12063 Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 425636 0 0 0 31899 1102 0 0 25 0 1 0 805219536 44163072 9964 4294967295 134512640 134714508 3221221776 3221218004 1075115057 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 10782 9964 1111 63 0 10719 0 vsize: 0 Child ended because it received signal 11 (SIGSEGV) Real time (s): 330.229 CPU time (s): 330.231 CPU user time (s): 319.182 CPU system time (s): 11.0483 CPU usage (%): 100.001 Max. virtual memory (Kb): 43128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####