Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare1.opb |
MD5SUM | c8b965306fec2c21edee64824d12f378 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 63488 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 180 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 6442450938 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 6442450938 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.08 |
Number of variables | 230 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-05-25 01:43:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13510 boxname=wulflinc6 idbench=1040 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: c8b965306fec2c21edee64824d12f378 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-markshare1.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-markshare1.opb IDLAUNCH: 13510 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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 : 2 cpu MHz : 451.042 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: 777480 kB Buffers: 31580 kB Cached: 203088 kB SwapCached: 408 kB Active: 68880 kB Inactive: 168104 kB HighTotal: 131008 kB HighFree: 1120 kB LowTotal: 903652 kB LowFree: 776360 kB SwapTotal: 2097136 kB SwapFree: 2096040 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5692 kB Slab: 14508 kB Committed_AS: 63732 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 01:46:50 (client local time) WITH STATUS 0 IN 226.436 SECONDS stats: 13510 7 226.436 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Initial problem consists of 230 variables and 12 constraints. c After prepocess the problem consists of 176 variables and 12 constraints. c preprocess terminated 0.07 s c Initial Lower Bound: 0 c Lower Bound Elapsed time: 0 c Use computed LB before first solution. #### 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.70 0.82 0.86 2/54 781 Raw data (stat): 781 (runsolver) R 780 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 776785584 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 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+9.99946 s] Raw data (loadavg): 0.75 0.82 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 11985 0 0 0 970 29 0 0 25 0 1 0 776785584 53522432 11878 4294967295 134512640 134714540 3221224592 3221223232 134535032 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 13067 11878 1111 63 0 13004 0 vsize: 52268 [startup+19.9996 s] Raw data (loadavg): 0.79 0.83 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 23389 0 0 0 1943 56 0 0 25 0 1 0 776785584 101367808 23112 4294967295 134512640 134714540 3221224592 3221223376 134558521 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 24748 23112 1111 63 0 24685 0 vsize: 98992 [startup+29.9997 s] Raw data (loadavg): 0.82 0.83 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 32933 0 0 0 2919 80 0 0 25 0 1 0 776785584 140201984 32589 4294967295 134512640 134714540 3221224592 3221223176 134543614 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 34229 32589 1111 63 0 34166 0 vsize: 136916 [startup+40.0004 s] Raw data (loadavg): 0.85 0.84 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 42784 0 0 0 3892 107 0 0 25 0 1 0 776785584 183390208 42051 4294967295 134512640 134714540 3221224592 3221223340 134558476 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 44773 42051 1111 63 0 44710 0 vsize: 179092 [startup+50 s] Raw data (loadavg): 0.87 0.84 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 53319 0 0 0 4865 134 0 0 25 0 1 0 776785584 227381248 52440 4294967295 134512640 134714540 3221224592 3221223000 134697471 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 55513 52440 1111 63 0 55450 0 vsize: 222052 [startup+60.001 s] Raw data (loadavg): 0.89 0.85 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 62114 0 0 0 5840 159 0 0 25 0 1 0 776785584 262459392 61207 4294967295 134512640 134714540 3221224592 3221223324 134518100 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 64077 61207 1111 63 0 64014 0 vsize: 256308 [startup+70.0016 s] Raw data (loadavg): 0.91 0.85 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 74401 0 0 0 6811 189 0 0 25 0 1 0 776785584 312385536 71135 4294967295 134512640 134714540 3221224592 3221222920 1077378037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 76266 71135 1111 63 0 76203 0 vsize: 305064 [startup+80.0013 s] Raw data (loadavg): 0.92 0.86 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 84198 0 0 0 7786 214 0 0 25 0 1 0 776785584 351739904 80701 4294967295 134512640 134714540 3221224592 3221223152 134542350 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 85874 80701 1111 63 0 85811 0 vsize: 343496 [startup+90.0008 s] Raw data (loadavg): 0.93 0.86 0.86 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 94435 0 0 0 8760 241 0 0 25 0 1 0 776785584 393293824 90850 4294967295 134512640 134714540 3221224592 3221223200 134543724 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 96019 90850 1111 63 0 95956 0 vsize: 384076 [startup+100.001 s] Raw data (loadavg): 0.94 0.86 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 104074 0 0 0 9735 266 0 0 25 0 1 0 776785584 430481408 100141 4294967295 134512640 134714540 3221224592 3221223540 134575027 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 105098 100141 1111 63 0 105035 0 vsize: 420392 [startup+110.001 s] Raw data (loadavg): 0.95 0.87 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 114223 0 0 0 10710 291 0 0 25 0 1 0 776785584 470962176 109755 4294967295 134512640 134714540 3221224592 3221222920 1077378037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 114981 109755 1111 63 0 114918 0 vsize: 459924 [startup+120.002 s] Raw data (loadavg): 0.96 0.87 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 123229 0 0 0 11685 316 0 0 25 0 1 0 776785584 507027456 118596 4294967295 134512640 134714540 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 123786 118596 1111 63 0 123723 0 vsize: 495144 [startup+130.001 s] Raw data (loadavg): 0.96 0.88 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 128116 0 0 0 12674 328 0 0 25 0 1 0 776785584 525922304 123305 4294967295 134512640 134714540 3221224592 3221223160 1077378037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 128399 123306 1111 63 0 128336 0 vsize: 513596 [startup+140.001 s] Raw data (loadavg): 0.97 0.88 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 145950 0 0 0 13635 368 0 0 25 0 1 0 776785584 595017728 134997 4294967295 134512640 134714540 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 145268 134997 1111 63 0 145205 0 vsize: 581072 [startup+150.002 s] Raw data (loadavg): 0.97 0.88 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 157591 0 0 0 14608 395 0 0 25 0 1 0 776785584 639422464 145500 4294967295 134512640 134714540 3221224592 3221223160 1077378037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 156109 145500 1111 63 0 156046 0 vsize: 624436 [startup+160.002 s] Raw data (loadavg): 0.98 0.89 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 168434 0 0 0 15582 421 0 0 25 0 1 0 776785584 681877504 156158 4294967295 134512640 134714540 3221224592 3221222920 1077378037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 166474 156158 1111 63 0 166411 0 vsize: 665896 [startup+170.002 s] Raw data (loadavg): 0.98 0.89 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 177324 0 0 0 16560 444 0 0 25 0 1 0 776785584 716595200 164883 4294967295 134512640 134714540 3221224592 3221223216 134543097 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 174950 164883 1111 63 0 174887 0 vsize: 699800 [startup+180.001 s] Raw data (loadavg): 0.98 0.89 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 187420 0 0 0 17535 469 0 0 25 0 1 0 776785584 756764672 174295 4294967295 134512640 134714540 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 184757 174296 1111 63 0 184694 0 vsize: 739028 [startup+190.001 s] Raw data (loadavg): 0.98 0.90 0.87 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 198284 0 0 0 18509 495 0 0 25 0 1 0 776785584 800182272 185060 4294967295 134512640 134714540 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 195357 185060 1111 63 0 195294 0 vsize: 781428 [startup+200.001 s] Raw data (loadavg): 0.99 0.90 0.88 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 211894 0 0 0 19479 526 0 0 25 0 1 0 776785584 850771968 196324 4294967295 134512640 134714540 3221224592 3221223128 134543023 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 207708 196324 1111 63 0 207645 0 vsize: 830832 [startup+210.002 s] Raw data (loadavg): 0.99 0.90 0.88 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 220379 0 1 0 20453 551 0 0 25 0 1 0 776785584 883888128 204730 4294967295 134512640 134714540 3221224592 3221223196 134536817 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 215793 204730 1111 63 0 215730 0 vsize: 863172 [startup+220.002 s] Raw data (loadavg): 0.99 0.90 0.88 2/54 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 229557 0 1 0 21425 579 0 0 25 0 1 0 776785584 920911872 212796 4294967295 134512640 134714540 3221224592 3221223360 134592137 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 224832 212796 1111 63 0 224769 0 vsize: 899328 [startup+226.439 s] Raw data (loadavg): 0.99 0.91 0.88 1/53 781 Raw data (stat): 781 (bsolo_mis) R 780 25568 25567 0 -1 0 229557 0 1 0 21425 579 0 0 25 0 1 0 776785584 920911872 212796 4294967295 134512640 134714540 3221224592 3221223360 134592137 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 224832 212796 1111 63 0 224769 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 226.439 CPU time (s): 226.436 CPU user time (s): 220.035 CPU system time (s): 6.40103 CPU usage (%): 99.9987 Max. virtual memory (Kb): 899328 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####