Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-lseu.opb |
MD5SUM | 99657262afbbfce7034a3ec6b29d9b3b |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1120 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 85 |
Biggest coefficient in the objective function | 517 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 15494 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 1656 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 15494 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02984 |
Number of variables | 89 |
Total number of constraints | 117 |
Number of constraints which are clauses | 2 |
Number of constraints which are cardinality constraints (but not clauses) | 104 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 47 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc24 THE 2005-05-25 01:37:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13496 boxname=wulflinc24 idbench=1039 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: 99657262afbbfce7034a3ec6b29d9b3b /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-lseu.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-lseu.opb IDLAUNCH: 13496 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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 : 3 cpu MHz : 451.080 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: 753000 kB Buffers: 10392 kB Cached: 248884 kB SwapCached: 620 kB Active: 31988 kB Inactive: 229700 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 752748 kB SwapTotal: 2097892 kB SwapFree: 2096776 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5656 kB Slab: 14172 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 01:39:51 (client local time) WITH STATUS 0 IN 146.099 SECONDS stats: 13496 7 146.099 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c Initial problem consists of 89 variables and 28 constraints. c After prepocess the problem consists of 89 variables and 28 constraints. c preprocess terminated 0.069 s c Initial Lower Bound: 777 c Lower Bound Elapsed time: 0.01 c Use computed LB before first solution. c NEW SOLUTION FOUND: 3184 @ 1.334 c NEW SOLUTION FOUND: 3074 @ 1.347 c NEW SOLUTION FOUND: 2879 @ 1.38 c NEW SOLUTION FOUND: 2798 @ 1.443 c NEW SOLUTION FOUND: 2783 @ 1.468 c NEW SOLUTION FOUND: 2681 @ 1.515 c NEW SOLUTION FOUND: 2471 @ 1.528 c NEW SOLUTION FOUND: 2451 @ 2.673 c NEW SOLUTION FOUND: 2393 @ 25.612 c NEW SOLUTION FOUND: 2377 @ 27.439 c NEW SOLUTION FOUND: 2307 @ 39.494 c NEW SOLUTION FOUND: 2283 @ 39.511 c NEW SOLUTION FOUND: 2213 @ 50.779 #### 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.91 0.97 0.93 2/54 11675 Raw data (stat): 11675 (runsolver) R 11674 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834971538 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.93 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 9725 0 0 0 960 37 0 0 25 0 1 0 834971538 11812864 2198 4294967295 134512640 134714508 3221224592 3221223036 1077781665 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 2940 2199 1111 63 0 2877 0 vsize: 11536 [startup+20.0016 s] Raw data (loadavg): 0.94 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 28901 0 0 0 1902 95 0 0 25 0 1 0 834971538 16494592 3301 4294967295 134512640 134714508 3221224592 3221221484 1077386340 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4064 3303 1111 63 0 4001 0 vsize: 16108 [startup+30.0019 s] Raw data (loadavg): 0.95 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 54682 0 0 0 2842 155 0 0 25 0 1 0 834971538 18354176 3801 4294967295 134512640 134714508 3221224592 3221222808 1074153504 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4481 3801 1111 63 0 4418 0 vsize: 17924 [startup+40.0015 s] Raw data (loadavg): 0.95 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 71420 0 0 0 3803 194 0 0 25 0 1 0 834971538 20746240 4121 4294967295 134512640 134714508 3221224592 3221221612 1074950644 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5065 4128 1111 63 0 5002 0 vsize: 20260 [startup+50.0014 s] Raw data (loadavg): 0.96 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 103501 0 0 0 4732 265 0 0 25 0 1 0 834971538 21708800 4611 4294967295 134512640 134714508 3221224592 3221223036 1077781665 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5300 4611 1111 63 0 5237 0 vsize: 21200 [startup+60.0018 s] Raw data (loadavg): 0.97 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 114915 0 0 0 5707 289 0 0 25 0 1 0 834971538 23601152 4890 4294967295 134512640 134714508 3221224592 3221220800 1076079346 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5762 4890 1111 63 0 5699 0 vsize: 23048 [startup+70.0025 s] Raw data (loadavg): 0.97 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 129812 0 0 0 6673 324 0 0 25 0 1 0 834971538 23158784 4979 4294967295 134512640 134714508 3221224592 3221222704 1074867317 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5654 4979 1111 63 0 5591 0 vsize: 22616 [startup+80.0028 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 146615 0 0 0 7631 365 0 0 25 0 1 0 834971538 24977408 5206 4294967295 134512640 134714508 3221224592 3221220960 1075894538 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6098 5206 1111 63 0 6035 0 vsize: 24392 [startup+90.0029 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 186456 0 0 0 8543 454 0 0 25 0 1 0 834971538 26988544 5881 4294967295 134512640 134714508 3221224592 3221223168 134542350 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6589 5881 1111 63 0 6526 0 vsize: 26356 [startup+100.003 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 227713 0 0 0 9447 550 0 0 25 0 1 0 834971538 30625792 6751 4294967295 134512640 134714508 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7477 6751 1111 63 0 7414 0 vsize: 29908 [startup+110.004 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 263902 0 0 0 10366 632 0 0 25 0 1 0 834971538 34353152 7618 4294967295 134512640 134714508 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 8387 7618 1111 63 0 8324 0 vsize: 33548 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 291899 0 0 0 11306 691 0 0 25 0 1 0 834971538 36352000 8105 4294967295 134512640 134714508 3221224592 3221222896 1074153792 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 8875 8105 1111 63 0 8812 0 vsize: 35500 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 310078 0 0 0 12265 733 0 0 25 0 1 0 834971538 38428672 8374 4294967295 134512640 134714508 3221224592 3221220752 1075091317 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 9382 8374 1111 63 0 9319 0 vsize: 37528 [startup+140.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 316354 0 0 0 13248 749 0 0 25 0 1 0 834971538 40783872 9125 4294967295 134512640 134714508 3221224592 3221221360 1076083615 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 9957 9125 1111 63 0 9894 0 vsize: 39828 [startup+146.115 s] Raw data (loadavg): 0.99 0.97 0.93 1/53 11675 Raw data (stat): 11675 (bsolo_lpr_cuts) R 11674 4613 4612 0 -1 0 316354 0 0 0 13248 749 0 0 25 0 1 0 834971538 40783872 9125 4294967295 134512640 134714508 3221224592 3221221360 1076083615 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 9957 9125 1111 63 0 9894 0 vsize: 0 Child ended because it received signal 11 (SIGSEGV) Real time (s): 146.114 CPU time (s): 146.099 CPU user time (s): 138.373 CPU system time (s): 7.72583 CPU usage (%): 99.9895 Max. virtual memory (Kb): 39828 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####