Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10c.opb |
MD5SUM | 31a8734340f0544712ef974997c104b2 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2677632 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2100 |
Biggest coefficient in the objective function | 4718592 |
Number of bits for the biggest coefficient in the objective function | 23 |
Sum of the numbers in the objective function | 515723936 |
Number of bits of the sum of numbers in the objective function | 29 |
Biggest number in a constraint | 4718592 |
Number of bits of the biggest number in a constraint | 23 |
Biggest sum of numbers in a constraint | 515723936 |
Number of bits of the biggest sum of numbers | 29 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 2100 |
Total number of constraints | 120 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 120 |
Minimum length of a constraint | 21 |
Maximum length of a constraint | 200 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc13 THE 2005-05-24 17:51:41 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=19216 boxname=wulflinc13 idbench=1479 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: 31a8734340f0544712ef974997c104b2 /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-ran10x10c.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-ran10x10c.opb IDLAUNCH: 19216 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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.242 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: 899292 kB Buffers: 18948 kB Cached: 91460 kB SwapCached: 5124 kB Active: 24140 kB Inactive: 93440 kB HighTotal: 131008 kB HighFree: 35532 kB LowTotal: 903652 kB LowFree: 863760 kB SwapTotal: 2097136 kB SwapFree: 2091632 kB Dirty: 1140 kB Writeback: 0 kB Mapped: 6164 kB Slab: 12076 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-24 17:56:59 (client local time) WITH STATUS 0 IN 317.274 SECONDS stats: 19216 7 317.274 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c Initial problem consists of 2100 variables and 140 constraints. c After prepocess the problem consists of 1087 variables and 186 constraints. c preprocess terminated 1.717 s c Initial Lower Bound: 1434039 c Lower Bound Elapsed time: 0.3326 c Use computed LB before first solution. c NEW SOLUTION FOUND: 6892928 @ 145.082 c NEW SOLUTION FOUND: 6811904 @ 145.594 c NEW SOLUTION FOUND: 6799872 @ 145.6 c NEW SOLUTION FOUND: 6780800 @ 145.723 c NEW SOLUTION FOUND: 6640064 @ 147.034 c NEW SOLUTION FOUND: 6532096 @ 260.913 #### 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.98 0.94 2/54 3327 Raw data (stat): 3327 (runsolver) R 3326 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 773964113 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 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.001 s] Raw data (loadavg): 0.93 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 9877 0 6 0 961 27 0 0 25 0 1 0 773964113 19611648 4086 4294967295 134512640 134714508 3221224576 3221222880 1074153770 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4788 4086 1111 63 0 4725 0 vsize: 19152 [startup+20.0013 s] Raw data (loadavg): 0.94 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 13364 0 6 0 1952 36 0 0 25 0 1 0 773964113 19611648 4088 4294967295 134512640 134714508 3221224576 3221213576 1077380592 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4788 4088 1111 63 0 4725 0 vsize: 19152 [startup+30.0006 s] Raw data (loadavg): 0.95 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 16789 0 6 0 2943 45 0 0 25 0 1 0 773964113 19791872 4121 4294967295 134512640 134714508 3221224576 3221222304 1075828441 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4832 4121 1111 63 0 4769 0 vsize: 19328 [startup+40.0007 s] Raw data (loadavg): 0.96 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 20276 0 6 0 3933 55 0 0 25 0 1 0 773964113 19865600 4121 4294967295 134512640 134714508 3221224576 3221221648 1075895997 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4850 4121 1111 63 0 4787 0 vsize: 19400 [startup+50.0013 s] Raw data (loadavg): 0.96 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 23661 0 6 0 4924 64 0 0 25 0 1 0 773964113 19927040 4136 4294967295 134512640 134714508 3221224576 3221220712 1077410279 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4865 4136 1111 63 0 4802 0 vsize: 19460 [startup+60.0017 s] Raw data (loadavg): 0.97 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26093 0 6 0 5917 71 0 0 25 0 1 0 773964113 19611648 4089 4294967295 134512640 134714508 3221224576 3221222256 1075895023 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4788 4089 1111 63 0 4725 0 vsize: 19152 [startup+70.0026 s] Raw data (loadavg): 0.97 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26585 0 6 0 6915 74 0 0 25 0 1 0 773964113 19611648 4089 4294967295 134512640 134714508 3221224576 3221222956 1077781665 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4788 4089 1111 63 0 4725 0 vsize: 19152 [startup+80.0033 s] Raw data (loadavg): 0.98 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26725 0 6 0 7914 75 0 0 25 0 1 0 773964113 19611648 4089 4294967295 134512640 134714508 3221224576 3221221856 1074140035 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4788 4089 1111 63 0 4725 0 vsize: 19152 [startup+90.0036 s] Raw data (loadavg): 0.98 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26808 0 6 0 8913 76 0 0 25 0 1 0 773964113 19611648 4089 4294967295 134512640 134714508 3221224576 3221222576 1074918280 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4788 4089 1111 63 0 4725 0 vsize: 19152 [startup+100.004 s] Raw data (loadavg): 0.98 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26845 0 6 0 9912 78 0 0 25 0 1 0 773964113 19611648 4089 4294967295 134512640 134714508 3221224576 3221223216 134649184 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4788 4089 1111 63 0 4725 0 vsize: 19152 [startup+110.004 s] Raw data (loadavg): 0.98 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26845 0 6 0 10911 78 0 0 25 0 1 0 773964113 19611648 4089 4294967295 134512640 134714508 3221224576 3221222928 1074153770 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4788 4089 1111 63 0 4725 0 vsize: 19152 [startup+120.005 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26845 0 6 0 11910 79 0 0 25 0 1 0 773964113 19611648 4089 4294967295 134512640 134714508 3221224576 3221222576 1074918591 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4788 4089 1111 63 0 4725 0 vsize: 19152 [startup+130.005 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26847 0 6 0 12910 80 0 0 25 0 1 0 773964113 19574784 4082 4294967295 134512640 134714508 3221224576 3221222792 1074138150 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4779 4082 1111 63 0 4716 0 vsize: 19116 [startup+140.005 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 26847 0 6 0 13909 81 0 0 25 0 1 0 773964113 19574784 4082 4294967295 134512640 134714508 3221224576 3221222152 1077410205 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4779 4082 1111 63 0 4716 0 vsize: 19116 [startup+150.006 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 27306 0 6 0 14906 84 0 0 25 0 1 0 773964113 20430848 4293 4294967295 134512640 134714508 3221224576 3221223016 1077374433 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4988 4293 1111 63 0 4925 0 vsize: 19952 [startup+160.007 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 35495 0 6 0 15882 108 0 0 25 0 1 0 773964113 27357184 5919 4294967295 134512640 134714508 3221224576 3221222728 1074950077 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6679 5919 1111 63 0 6616 0 vsize: 26716 [startup+170.008 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 42622 0 6 0 16859 131 0 0 25 0 1 0 773964113 30769152 6818 4294967295 134512640 134714508 3221224576 3221221496 1074950108 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7512 6818 1111 63 0 7449 0 vsize: 30048 [startup+180.007 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 47067 0 6 0 17842 148 0 0 25 0 1 0 773964113 34217984 7573 4294967295 134512640 134714508 3221224576 3221221604 1075277451 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 8354 7573 1111 63 0 8291 0 vsize: 33416 [startup+190.008 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 56685 0 6 0 18815 175 0 0 25 0 1 0 773964113 44052480 10062 4294967295 134512640 134714508 3221224576 3221222348 1077411564 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 10755 10062 1111 63 0 10692 0 vsize: 43020 [startup+200.009 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 58330 0 6 0 19809 181 0 0 25 0 1 0 773964113 45101056 10318 4294967295 134512640 134714508 3221224576 3221222576 1074918536 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 11011 10318 1111 63 0 10948 0 vsize: 44044 [startup+210.009 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 63729 0 6 0 20794 196 0 0 25 0 1 0 773964113 45813760 10492 4294967295 134512640 134714508 3221224576 3221222928 1074115298 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 11185 10492 1111 63 0 11122 0 vsize: 44740 [startup+220.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 73206 0 6 0 21768 222 0 0 25 0 1 0 773964113 52862976 12144 4294967295 134512640 134714508 3221224576 3221221168 1074885264 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 12906 12144 1111 63 0 12843 0 vsize: 51624 [startup+230.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 79291 0 6 0 22751 239 0 0 25 0 1 0 773964113 57106432 13249 4294967295 134512640 134714508 3221224576 3221222928 1074115298 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 13942 13249 1111 63 0 13879 0 vsize: 55768 [startup+240.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 84605 0 6 0 23734 256 0 0 25 0 1 0 773964113 60579840 14097 4294967295 134512640 134714508 3221224576 3221222976 1074118815 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 14790 14097 1111 63 0 14727 0 vsize: 59160 [startup+250.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 94436 0 6 0 24706 284 0 0 25 0 1 0 773964113 67293184 15736 4294967295 134512640 134714508 3221224576 3221222944 1074153537 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 16429 15736 1111 63 0 16366 0 vsize: 65716 [startup+260.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 106047 0 6 0 25674 316 0 0 25 0 1 0 773964113 77733888 18285 4294967295 134512640 134714508 3221224576 3221222772 1077782939 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18978 18285 1111 63 0 18915 0 vsize: 75912 [startup+270.012 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 118083 0 6 0 26640 350 0 0 25 0 1 0 773964113 85102592 20084 4294967295 134512640 134714508 3221224576 3221222844 1077410225 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20777 20084 1111 63 0 20714 0 vsize: 83108 [startup+280.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 129597 0 6 0 27610 380 0 0 25 0 1 0 773964113 93077504 21957 4294967295 134512640 134714508 3221224576 3221220484 1074786571 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 22724 21957 1111 63 0 22661 0 vsize: 90896 [startup+290.012 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 133799 0 6 0 28600 391 0 0 25 0 1 0 773964113 95047680 22512 4294967295 134512640 134714508 3221224576 3221222576 1074918591 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 23205 22512 1111 63 0 23142 0 vsize: 92820 [startup+300.012 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 140818 0 6 0 29582 408 0 0 25 0 1 0 773964113 98922496 23458 4294967295 134512640 134714508 3221224576 3221222832 1074153782 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 24151 23458 1111 63 0 24088 0 vsize: 96604 [startup+310.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 148937 0 6 0 30562 429 0 0 25 0 1 0 773964113 103788544 24557 4294967295 134512640 134714508 3221224576 3221220540 1074860608 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 25339 24558 1111 63 0 25276 0 vsize: 101356 [startup+317.366 s] Raw data (loadavg): 0.99 0.98 0.94 1/53 3327 Raw data (stat): 3327 (bsolo_lpr_cuts) R 3326 1269 1268 0 -1 0 148937 0 6 0 30562 429 0 0 25 0 1 0 773964113 103788544 24557 4294967295 134512640 134714508 3221224576 3221220540 1074860608 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 25339 24558 1111 63 0 25276 0 vsize: 0 Child ended because it received signal 11 (SIGSEGV) Real time (s): 317.366 CPU time (s): 317.274 CPU user time (s): 312.747 CPU system time (s): 4.52631 CPU usage (%): 99.9711 Max. virtual memory (Kb): 101356 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####