Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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.18 |
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 wulflinc27 THE 2005-05-24 19:29:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18320 boxname=wulflinc27 idbench=1410 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: 2854384016ebafb26c8bfb47f81aee87 /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-fast0507.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-fast0507.opb IDLAUNCH: 18320 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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.169 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: 848076 kB Buffers: 32484 kB Cached: 131924 kB SwapCached: 628 kB Active: 49728 kB Inactive: 117072 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 847824 kB SwapTotal: 2097892 kB SwapFree: 2096768 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5644 kB Slab: 14024 kB Committed_AS: 63580 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-24 19:35:58 (client local time) WITH STATUS 0 IN 387.827 SECONDS stats: 18320 7 387.827 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.92 0.95 0.90 2/54 6944 Raw data (stat): 6944 (runsolver) R 6943 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 832760643 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.0008 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 4742 0 0 0 987 12 0 0 25 0 1 0 832760643 32235520 4720 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7870 4720 1111 63 0 7807 0 vsize: 31480 [startup+20.002 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 9052 0 0 0 1980 19 0 0 25 0 1 0 832760643 49840128 9030 4294967295 134512640 134714540 3221224592 3221222820 1077414410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 12168 9030 1111 63 0 12105 0 vsize: 48672 [startup+30.0017 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 13437 0 0 0 2972 27 0 0 25 0 1 0 832760643 67903488 13415 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 16578 13415 1111 63 0 16515 0 vsize: 66312 [startup+40.0042 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 17897 0 0 0 3964 35 0 0 25 0 1 0 832760643 86114304 17875 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 21024 17875 1111 63 0 20961 0 vsize: 84096 [startup+50.0053 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 22399 0 0 0 4957 43 0 0 25 0 1 0 832760643 104484864 22377 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 25509 22377 1111 63 0 25446 0 vsize: 102036 [startup+60.0051 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 26950 0 0 0 5950 51 0 0 25 0 1 0 832760643 123142144 26928 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 30064 26928 1111 63 0 30001 0 vsize: 120256 [startup+70.0056 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 31545 0 0 0 6942 58 0 0 25 0 1 0 832760643 141959168 31523 4294967295 134512640 134714540 3221224592 3221222820 1077414395 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 34658 31523 1111 63 0 34595 0 vsize: 138632 [startup+80.0057 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 36187 0 0 0 7937 64 0 0 25 0 1 0 832760643 161067008 36165 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 39323 36165 1111 63 0 39260 0 vsize: 157292 [startup+90.0065 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 40903 0 0 0 8929 71 0 0 25 0 1 0 832760643 180330496 40881 4294967295 134512640 134714540 3221224592 3221222820 1077414424 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 44026 40881 1111 63 0 43963 0 vsize: 176104 [startup+100.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 45678 0 0 0 9921 80 0 0 25 0 1 0 832760643 199884800 45656 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 48800 45656 1111 63 0 48737 0 vsize: 195200 [startup+110.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 50519 0 0 0 10914 87 0 0 25 0 1 0 832760643 219766784 50497 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 53654 50497 1111 63 0 53591 0 vsize: 214616 [startup+120.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 55412 0 0 0 11906 95 0 0 25 0 1 0 832760643 239775744 55390 4294967295 134512640 134714540 3221224592 3221222820 1077414424 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 58539 55390 1111 63 0 58476 0 vsize: 234156 [startup+130.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 60351 0 0 0 12898 104 0 0 25 0 1 0 832760643 260075520 60329 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 63495 60329 1111 63 0 63432 0 vsize: 253980 [startup+140.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 65402 0 0 0 13890 112 0 0 25 0 1 0 832760643 280678400 65380 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 68525 65380 1111 63 0 68462 0 vsize: 274100 [startup+150.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 70495 0 0 0 14883 119 0 0 25 0 1 0 832760643 301584384 70473 4294967295 134512640 134714540 3221224592 3221222820 1077414349 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 73629 70473 1111 63 0 73566 0 vsize: 294516 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 75642 0 0 0 15872 130 0 0 25 0 1 0 832760643 322633728 75620 4294967295 134512640 134714540 3221224592 3221222820 1077414435 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 78768 75620 1111 63 0 78705 0 vsize: 315072 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 80862 0 0 0 16863 139 0 0 25 0 1 0 832760643 343986176 80840 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 83981 80840 1111 63 0 83918 0 vsize: 335924 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 86143 0 0 0 17855 147 0 0 25 0 1 0 832760643 365633536 86121 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 89266 86121 1111 63 0 89203 0 vsize: 357064 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 91496 0 0 0 18846 157 0 0 25 0 1 0 832760643 387579904 91474 4294967295 134512640 134714540 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 94624 91474 1111 63 0 94561 0 vsize: 378496 [startup+200.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 96929 0 0 0 19837 165 0 0 25 0 1 0 832760643 409833472 96907 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 100057 96907 1111 63 0 99994 0 vsize: 400228 [startup+210.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 102446 0 0 0 20830 173 0 0 25 0 1 0 832760643 432590848 102424 4294967295 134512640 134714540 3221224592 3221222820 1077414358 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 105613 102424 1111 63 0 105550 0 vsize: 422452 [startup+220.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 108042 0 0 0 21822 181 0 0 25 0 1 0 832760643 455434240 108020 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 111190 108020 1111 63 0 111127 0 vsize: 444760 [startup+230.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 113768 0 0 0 22814 189 0 0 25 0 1 0 832760643 478875648 113746 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 116913 113746 1111 63 0 116850 0 vsize: 467652 [startup+240.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 119675 0 0 0 23805 199 0 0 25 0 1 0 832760643 503066624 119653 4294967295 134512640 134714540 3221224592 3221222820 1077414336 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 122819 119653 1111 63 0 122756 0 vsize: 491276 [startup+250.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 125763 0 0 0 24794 210 0 0 25 0 1 0 832760643 527994880 125741 4294967295 134512640 134714540 3221224592 3221222820 1077414432 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 128905 125741 1111 63 0 128842 0 vsize: 515620 [startup+260.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 131895 0 0 0 25783 221 0 0 25 0 1 0 832760643 553078784 131873 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 135029 131873 1111 63 0 134966 0 vsize: 540116 [startup+270.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 138161 0 0 0 26772 232 0 0 25 0 1 0 832760643 578756608 138139 4294967295 134512640 134714540 3221224592 3221222924 1077399562 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 141298 138143 1111 63 0 141235 0 vsize: 565192 [startup+280.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 144591 0 0 0 27763 242 0 0 25 0 1 0 832760643 605040640 144569 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 147715 144569 1111 63 0 147652 0 vsize: 590860 [startup+290.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 151172 0 0 0 28752 253 0 0 25 0 1 0 832760643 632061952 151150 4294967295 134512640 134714540 3221224592 3221222820 1077414408 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 154312 151150 1111 63 0 154249 0 vsize: 617248 [startup+300.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 157899 0 0 0 29741 264 0 0 25 0 1 0 832760643 659533824 157877 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 161019 157877 1111 63 0 160956 0 vsize: 644076 [startup+310.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 164853 0 0 0 30729 276 0 0 25 0 1 0 832760643 688050176 164831 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 167981 164831 1111 63 0 167918 0 vsize: 671924 [startup+320.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 172103 0 0 0 31717 289 0 0 25 0 1 0 832760643 717762560 172081 4294967295 134512640 134714540 3221224592 3221222820 1077414336 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 175235 172081 1111 63 0 175172 0 vsize: 700940 [startup+330.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 179541 0 0 0 32705 300 0 0 25 0 1 0 832760643 748220416 179519 4294967295 134512640 134714540 3221224592 3221222924 1077399562 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 182671 179521 1111 63 0 182608 0 vsize: 730684 [startup+340.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 187314 0 0 0 33692 313 0 0 25 0 1 0 832760643 780025856 187292 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 190436 187292 1111 63 0 190373 0 vsize: 761744 [startup+350.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 195250 0 0 0 34680 325 0 0 25 0 1 0 832760643 812781568 195228 4294967295 134512640 134714540 3221224592 3221222820 1077414395 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 198433 195228 1111 63 0 198370 0 vsize: 793732 [startup+360.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 203448 0 0 0 35667 339 0 0 25 0 1 0 832760643 846376960 203426 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 206635 203426 1111 63 0 206572 0 vsize: 826540 [startup+370.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 211957 0 0 0 36650 355 0 0 25 0 1 0 832760643 881164288 211935 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 215128 211935 1111 63 0 215065 0 vsize: 860512 [startup+380.015 s] Raw data (loadavg): 0.99 0.97 0.91 3/54 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 220678 0 0 0 37625 380 0 0 25 0 1 0 832760643 916852736 218476 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 223841 218461 1111 63 0 223778 0 vsize: 895364 [startup+387.863 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 6944 Raw data (stat): 6944 (bsolo_mis) R 6943 3394 3393 0 -1 0 220678 0 0 0 37625 380 0 0 25 0 1 0 832760643 916852736 218476 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 223841 218461 1111 63 0 223778 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 387.862 CPU time (s): 387.827 CPU user time (s): 383.421 CPU system time (s): 4.40633 CPU usage (%): 99.9909 Max. virtual memory (Kb): 895364 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####