Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-fast0507.opb |
MD5SUM | 38504d32a17a57a658eee171614b901e |
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.17 |
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 wulflinc7 THE 2005-05-25 02:44:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12522 boxname=wulflinc7 idbench=964 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: 38504d32a17a57a658eee171614b901e /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-fast0507.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-fast0507.opb IDLAUNCH: 12522 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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.050 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: 833732 kB Buffers: 10452 kB Cached: 169716 kB SwapCached: 644 kB Active: 47988 kB Inactive: 134444 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 833480 kB SwapTotal: 2097136 kB SwapFree: 2095780 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5492 kB Slab: 12636 kB Committed_AS: 63564 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 02:50:44 (client local time) WITH STATUS 0 IN 370.308 SECONDS stats: 12522 7 370.308 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### #### 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.88 0.94 0.90 2/54 4327 Raw data (stat): 4327 (runsolver) R 4326 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 777163479 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0007 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 4867 0 0 0 990 8 0 0 25 0 1 0 777163479 32681984 4845 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7979 4845 1111 63 0 7916 0 vsize: 31916 [startup+20.0009 s] Raw data (loadavg): 0.91 0.94 0.90 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 9305 0 0 0 1982 16 0 0 25 0 1 0 777163479 50884608 9283 4294967295 134512640 134714540 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 12423 9283 1111 63 0 12360 0 vsize: 49692 [startup+30.0012 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 13806 0 0 0 2975 24 0 0 25 0 1 0 777163479 69398528 13784 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 16943 13784 1111 63 0 16880 0 vsize: 67772 [startup+40.0021 s] Raw data (loadavg): 0.94 0.95 0.90 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 18345 0 0 0 3969 31 0 0 25 0 1 0 777163479 87912448 18323 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 21463 18323 1111 63 0 21400 0 vsize: 85852 [startup+50.0018 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 22931 0 0 0 4960 39 0 0 25 0 1 0 777163479 106721280 22909 4294967295 134512640 134714540 3221224592 3221222820 1077414351 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 26055 22909 1111 63 0 25992 0 vsize: 104220 [startup+60.0021 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 27592 0 0 0 5951 48 0 0 25 0 1 0 777163479 125833216 27570 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 30721 27570 1111 63 0 30658 0 vsize: 122884 [startup+70.0023 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 32344 0 0 0 6944 56 0 0 25 0 1 0 777163479 145240064 32322 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 35459 32322 1111 63 0 35396 0 vsize: 141836 [startup+80.0037 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 37146 0 0 0 7936 64 0 0 25 0 1 0 777163479 164950016 37124 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 40271 37124 1111 63 0 40208 0 vsize: 161084 [startup+90.003 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 41983 0 0 0 8927 73 0 0 25 0 1 0 777163479 184807424 41961 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 45119 41961 1111 63 0 45056 0 vsize: 180476 [startup+100.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 46861 0 0 0 9920 81 0 0 25 0 1 0 777163479 204812288 46839 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 50003 46839 1111 63 0 49940 0 vsize: 200012 [startup+110.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 51830 0 0 0 10913 88 0 0 25 0 1 0 777163479 225140736 51808 4294967295 134512640 134714540 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 54966 51808 1111 63 0 54903 0 vsize: 219864 [startup+120.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 56880 0 0 0 11903 98 0 0 25 0 1 0 777163479 245895168 56858 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 60033 56858 1111 63 0 59970 0 vsize: 240132 [startup+130.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 62009 0 0 0 12893 108 0 0 25 0 1 0 777163479 266797056 61987 4294967295 134512640 134714540 3221224592 3221222820 1077414401 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 65136 61987 1111 63 0 65073 0 vsize: 260544 [startup+140.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 67308 0 0 0 13883 118 0 0 25 0 1 0 777163479 288595968 67286 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 70458 67291 1111 63 0 70395 0 vsize: 281832 [startup+150.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 72753 0 0 0 14874 128 0 0 25 0 1 0 777163479 310837248 72731 4294967295 134512640 134714540 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 75888 72731 1111 63 0 75825 0 vsize: 303552 [startup+160.006 s] Raw data (loadavg): 1.06 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 78302 0 0 0 15862 140 0 0 25 0 1 0 777163479 333537280 78280 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 81430 78280 1111 63 0 81367 0 vsize: 325720 [startup+170.006 s] Raw data (loadavg): 1.05 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 83917 0 0 0 16852 150 0 0 25 0 1 0 777163479 356528128 83895 4294967295 134512640 134714540 3221224592 3221222820 1077414376 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 87043 83895 1111 63 0 86980 0 vsize: 348172 [startup+180.006 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 89606 0 0 0 17841 161 0 0 25 0 1 0 777163479 379822080 89584 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 92730 89584 1111 63 0 92667 0 vsize: 370920 [startup+190.007 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 95413 0 0 0 18831 172 0 0 25 0 1 0 777163479 403558400 95391 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 98525 95391 1111 63 0 98462 0 vsize: 394100 [startup+200.006 s] Raw data (loadavg): 1.03 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 101350 0 0 0 19821 182 0 0 25 0 1 0 777163479 428113920 101328 4294967295 134512640 134714540 3221224592 3221222820 1077414435 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 104520 101328 1111 63 0 104457 0 vsize: 418080 [startup+210.007 s] Raw data (loadavg): 1.03 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 107439 0 0 0 20810 193 0 0 25 0 1 0 777163479 453046272 107417 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 110607 107417 1111 63 0 110544 0 vsize: 442428 [startup+220.007 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 113656 0 0 0 21798 204 0 0 25 0 1 0 777163479 478429184 113634 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 116804 113634 1111 63 0 116741 0 vsize: 467216 [startup+230.007 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 119989 0 0 0 22788 215 0 0 25 0 1 0 777163479 504406016 119967 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 123146 119967 1111 63 0 123083 0 vsize: 492584 [startup+240.006 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 126576 0 0 0 23776 227 0 0 25 0 1 0 777163479 531279872 126554 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 129707 126554 1111 63 0 129644 0 vsize: 518828 [startup+250.007 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 133268 0 0 0 24764 240 0 0 25 0 1 0 777163479 558755840 133246 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 136415 133246 1111 63 0 136352 0 vsize: 545660 [startup+260.007 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 140086 0 0 0 25752 252 0 0 25 0 1 0 777163479 586674176 140064 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 143231 140064 1111 63 0 143168 0 vsize: 572924 [startup+270.006 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 147106 0 0 0 26741 263 0 0 25 0 1 0 777163479 615342080 147084 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 150230 147084 1111 63 0 150167 0 vsize: 600920 [startup+280.007 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 154222 0 0 0 27729 275 0 0 25 0 1 0 777163479 644603904 154200 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 157374 154200 1111 63 0 157311 0 vsize: 629496 [startup+290.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 161533 0 0 0 28718 287 0 0 25 0 1 0 777163479 674463744 161511 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 164664 161511 1111 63 0 164601 0 vsize: 658656 [startup+300.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 169189 0 0 0 29704 300 0 0 25 0 1 0 777163479 705818624 169167 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 172319 169167 1111 63 0 172256 0 vsize: 689276 [startup+310.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 177000 0 0 0 30692 313 0 0 25 0 1 0 777163479 737771520 176978 4294967295 134512640 134714540 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 180120 176978 1111 63 0 180057 0 vsize: 720480 [startup+320.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 185016 0 0 0 31677 328 0 0 25 0 1 0 777163479 770621440 184994 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 188140 184994 1111 63 0 188077 0 vsize: 752560 [startup+330.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 193155 0 0 0 32666 339 0 0 25 0 1 0 777163479 803909632 193133 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 196267 193133 1111 63 0 196204 0 vsize: 785068 [startup+340.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 201508 0 0 0 33653 353 0 0 25 0 1 0 777163479 838463488 201486 4294967295 134512640 134714540 3221224592 3221222820 1077414336 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 204703 201486 1111 63 0 204640 0 vsize: 818812 [startup+350.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 210022 0 0 0 34636 368 0 0 25 0 1 0 777163479 873254912 209936 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 213197 209936 1111 63 0 213134 0 vsize: 852788 [startup+360.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 218524 0 1 0 35610 391 0 0 25 0 1 0 777163479 908042240 216624 4294967295 134512640 134714540 3221224592 3221222820 1077414370 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 221690 216624 1111 63 0 221627 0 vsize: 886760 [startup+370.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 1028 227235 0 5 0 36573 424 0 0 25 0 1 0 777163479 0 0 4294967295 0 0 0 0 0 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 [startup+370.342 s] Raw data (loadavg): 1.00 0.97 0.91 1/53 4327 Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 1028 227235 0 5 0 36573 424 0 0 25 0 1 0 777163479 0 0 4294967295 0 0 0 0 0 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 370.341 CPU time (s): 370.308 CPU user time (s): 365.735 CPU system time (s): 4.5723 CPU usage (%): 99.9909 Max. virtual memory (Kb): 886760 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####