Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0282.opb |
MD5SUM | a733e9fa1e4e3ac90baf85249f7c3e9a |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 258411 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 282 |
Biggest coefficient in the objective function | 160646 |
Number of bits for the biggest coefficient in the objective function | 18 |
Sum of the numbers in the objective function | 1302615 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 160646 |
Number of bits of the biggest number in a constraint | 18 |
Biggest sum of numbers in a constraint | 1302615 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 50.7373 |
Number of variables | 282 |
Total number of constraints | 523 |
Number of constraints which are clauses | 177 |
Number of constraints which are cardinality constraints (but not clauses) | 282 |
Number of constraints which are nor clauses,nor cardinality constraints | 64 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 57 |
LAUNCH ON wulflinc11 THE 2005-09-19 04:18:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4047 boxname=wulflinc11 idbench=531 idsolver=4 numberseed=0 MD5SUM SOLVER: 21c3ffd7205c96d5f0784fd273b92938 /oldhome/oroussel/solvers/PBS4 MD5SUM BENCH: a733e9fa1e4e3ac90baf85249f7c3e9a /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p0282.opb REAL COMMAND: PBS4 /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p0282.opb IDLAUNCH: 4047 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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.028 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: 879208 kB Buffers: 35680 kB Cached: 92244 kB SwapCached: 732 kB Active: 63972 kB Inactive: 66576 kB HighTotal: 131008 kB HighFree: 36932 kB LowTotal: 903652 kB LowFree: 842276 kB SwapTotal: 2097136 kB SwapFree: 2095856 kB Dirty: 32 kB Writeback: 0 kB Mapped: 5716 kB Slab: 19168 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 04:20:49 (client local time) WITH STATUS 30 IN 144.569 SECONDS stats: 4047 0 144.569 30
c PBS v4 by Bashar Al-Rawi & Fadi Aloul c Solving /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p0282.opb ...... c The optimum solution is:258411 s OPTIMUM FOUND v -C1001_bit0 -C1002_bit0 -C1003_bit0 C1004_bit0 -C1005_bit0 -C1006_bit0 -C1007_bit0 -C1008_bit0 -C1009_bit0 -C1010_bit0 -C1011_bit0 C1012_bit0 -C1013_bit0 -C1014_bit0 -C1015_bit0 -C1016_bit0 -C1017_bit0 -C1018_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 -C1022_bit0 -C1023_bit0 -C1024_bit0 -C1025_bit0 -C1026_bit0 -C1027_bit0 -C1028_bit0 -C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 -C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 -C1038_bit0 -C1039_bit0 -C1040_bit0 -C1041_bit0 -C1042_bit0 -C1043_bit0 -C1044_bit0 -C1045_bit0 -C1046_bit0 -C1047_bit0 -C1048_bit0 -C1049_bit0 -C1050_bit0 -C1051_bit0 -C1052_bit0 -C1053_bit0 -C1054_bit0 -C1055_bit0 -C1056_bit0 -C1057_bit0 -C1058_bit0 -C1059_bit0 -C1060_bit0 -C1061_bit0 -C1062_bit0 -C1063_bit0 -C1064_bit0 -C1065_bit0 -C1066_bit0 -C1067_bit0 -C1068_bit0 -C1069_bit0 -C1070_bit0 -C1071_bit0 -C1072_bit0 -C1073_bit0 -C1074_bit0 -C1075_bit0 -C1076_bit0 -C1077_bit0 -C1078_bit0 -C1079_bit0 -C1080_bit0 -C1081_bit0 -C1082_bit0 -C1083_bit0 -C1084_bit0 -C1085_bit0 -C1086_bit0 -C1087_bit0 -C1088_bit0 -C1089_bit0 -C1090_bit0 -C1091_bit0 C1092_bit0 -C1093_bit0 -C1094_bit0 -C1095_bit0 -C1096_bit0 -C1097_bit0 -C1098_bit0 -C1099_bit0 -C1100_bit0 -C1101_bit0 C1102_bit0 -C1103_bit0 C1104_bit0 -C1105_bit0 -C1106_bit0 -C1107_bit0 -C1108_bit0 -C1109_bit0 -C1110_bit0 -C1111_bit0 -C1112_bit0 -C1113_bit0 -C1114_bit0 -C1115_bit0 -C1116_bit0 -C1117_bit0 C1118_bit0 -C1119_bit0 -C1120_bit0 -C1121_bit0 -C1122_bit0 -C1123_bit0 -C1124_bit0 -C1125_bit0 -C1126_bit0 -C1127_bit0 -C1128_bit0 -C1129_bit0 -C1130_bit0 -C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1135_bit0 -C1136_bit0 -C1137_bit0 -C1138_bit0 -C1139_bit0 -C1140_bit0 -C1141_bit0 -C1142_bit0 -C1143_bit0 -C1144_bit0 -C1145_bit0 -C1146_bit0 -C1147_bit0 -C1148_bit0 -C1149_bit0 -C1150_bit0 -C1151_bit0 -C1152_bit0 -C1153_bit0 -C1154_bit0 -C1155_bit0 C1156_bit0 -C1157_bit0 -C1158_bit0 -C1159_bit0 -C1160_bit0 -C1161_bit0 -C1162_bit0 -C1163_bit0 -C1164_bit0 -C1165_bit0 -C1166_bit0 -C1167_bit0 -C1168_bit0 -C1169_bit0 C1170_bit0 -C1171_bit0 -C1172_bit0 -C1173_bit0 -C1174_bit0 -C1175_bit0 -C1176_bit0 -C1177_bit0 -C1178_bit0 -C1179_bit0 -C1180_bit0 -C1181_bit0 -C1182_bit0 -C1183_bit0 -C1184_bit0 -C1185_bit0 -C1186_bit0 -C1187_bit0 -C1188_bit0 -C1189_bit0 -C1190_bit0 -C1191_bit0 C1192_bit0 -C1193_bit0 -C1194_bit0 -C1195_bit0 -C1196_bit0 -C1197_bit0 -C1198_bit0 -C1199_bit0 C1200_bit0 -C1201_bit0 -C1202_bit0 -C1203_bit0 -C1204_bit0 -C1205_bit0 -C1206_bit0 -C1207_bit0 -C1208_bit0 -C1209_bit0 -C1210_bit0 -C1211_bit0 -C1212_bit0 -C1213_bit0 -C1214_bit0 -C1215_bit0 C1216_bit0 -C1217_bit0 -C1218_bit0 -C1219_bit0 -C1220_bit0 -C1221_bit0 -C1222_bit0 -C1223_bit0 C1224_bit0 -C1225_bit0 C1226_bit0 -C1227_bit0 -C1228_bit0 -C1229_bit0 -C1230_bit0 -C1231_bit0 -C1232_bit0 -C1233_bit0 -C1235_bit0 -C1237_bit0 -C1239_bit0 -C1241_bit0 C1243_bit0 -C1245_bit0 -C1247_bit0 C1248_bit0 -C1249_bit0 C1250_bit0 C1251_bit0 C1252_bit0 -C1253_bit0 C1254_bit0 -C1255_bit0 C1256_bit0 -C1257_bit0 -C1258_bit0 C1259_bit0 -C1260_bit0 -C1261_bit0 C1262_bit0 -C1263_bit0 C1264_bit0 C1265_bit0 -C1266_bit0 -C1267_bit0 C1268_bit0 -C1269_bit0 C1270_bit0 C1271_bit0 -C1272_bit0 -C1273_bit0 -C1274_bit0 -C1275_bit0 -C1276_bit0 -C1277_bit0 -C1278_bit0 -C1279_bit0 -C1280_bit0 C1281_bit0 -C1282_bit0 C1283_bit0 C1284_bit0 C1285_bit0 -C1286_bit0 -C1287_bit0 C1288_bit0 C1289_bit0 c Done, CPU Time=144.507
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 1788724228 978944 2 4294967295 134512640 135450776 3221224560 3221224560 134512960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24605/statm): 239 2 232 232 0 7 0 [pid=24605] vsize: 956 open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p0282.opb open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p0282.opb [startup+10.0029 s] Raw data (loadavg): 0.99 0.97 0.91 1/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) T 24604 24605 9854 0 -1 0 517 0 0 0 672 106 0 0 25 0 1 0 1788724228 3641344 500 4294967295 134512640 135450776 3221224560 3221223420 135126769 0 0 5 0 3222434794 0 0 17 0 0 0 Raw data (/proc/24605/statm): 889 500 232 232 0 657 0 [pid=24605] vsize: 3556 Current children cumulated CPU time (s) 7.78 Current children cumulated vsize (Kb) 3556 [startup+20.0037 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 794 0 0 0 1466 173 0 0 22 0 1 0 1788724228 3981312 777 4294967295 134512640 135450776 3221224560 3221223376 134550478 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24605/statm): 972 777 232 232 0 740 0 [pid=24605] vsize: 3888 Current children cumulated CPU time (s) 16.39 Current children cumulated vsize (Kb) 3888 [startup+30.0045 s] Raw data (loadavg): 0.99 0.97 0.91 1/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) T 24604 24605 9854 0 -1 0 899 0 0 0 2304 228 0 0 25 0 1 0 1788724228 4177920 833 4294967295 134512640 135450776 3221224560 3221223420 135126769 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/24605/statm): 1020 833 232 232 0 788 0 [pid=24605] vsize: 4080 Current children cumulated CPU time (s) 25.32 Current children cumulated vsize (Kb) 4080 [startup+40.0053 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 952 0 0 0 3171 272 0 0 22 0 1 0 1788724228 4460544 886 4294967295 134512640 135450776 3221224560 3221223408 134540101 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24605/statm): 1089 886 232 232 0 857 0 [pid=24605] vsize: 4356 Current children cumulated CPU time (s) 34.43 Current children cumulated vsize (Kb) 4356 [startup+50.006 s] Raw data (loadavg): 0.99 0.97 0.91 1/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) T 24604 24605 9854 0 -1 0 1103 0 0 0 4083 303 0 0 24 0 1 0 1788724228 6692864 1037 4294967295 134512640 135450776 3221224560 3221223420 135126769 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/24605/statm): 1634 1037 232 232 0 1402 0 [pid=24605] vsize: 6536 Current children cumulated CPU time (s) 43.86 Current children cumulated vsize (Kb) 6536 [startup+60.0068 s] Raw data (loadavg): 0.99 0.97 0.91 1/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) T 24604 24605 9854 0 -1 0 1268 0 0 0 5007 331 0 0 22 0 1 0 1788724228 7086080 1105 4294967295 134512640 135450776 3221224560 3221223420 135126769 0 0 5 0 3222434794 0 0 17 0 0 0 Raw data (/proc/24605/statm): 1730 1105 232 232 0 1498 0 [pid=24605] vsize: 6920 Current children cumulated CPU time (s) 53.38 Current children cumulated vsize (Kb) 6920 [startup+70.0076 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 1332 0 0 0 5943 352 0 0 25 0 1 0 1788724228 7229440 1169 4294967295 134512640 135450776 3221224560 3221223376 134550447 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24605/statm): 1765 1169 232 232 0 1533 0 [pid=24605] vsize: 7060 Current children cumulated CPU time (s) 62.95 Current children cumulated vsize (Kb) 7060 [startup+80.0074 s] Raw data (loadavg): 0.99 0.97 0.91 1/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) T 24604 24605 9854 0 -1 0 1498 0 0 0 6859 380 0 0 24 0 1 0 1788724228 7393280 1335 4294967295 134512640 135450776 3221224560 3221223420 135126769 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/24605/statm): 1805 1335 232 232 0 1573 0 [pid=24605] vsize: 7220 Current children cumulated CPU time (s) 72.39 Current children cumulated vsize (Kb) 7220 [startup+90.0082 s] Raw data (loadavg): 0.99 0.97 0.91 1/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) T 24604 24605 9854 0 -1 0 1601 0 0 0 7764 412 0 0 25 0 1 0 1788724228 7540736 1438 4294967295 134512640 135450776 3221224560 3221223420 135126769 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/24605/statm): 1841 1438 232 232 0 1609 0 [pid=24605] vsize: 7364 Current children cumulated CPU time (s) 81.76 Current children cumulated vsize (Kb) 7364 [startup+100.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 1717 0 0 0 8681 440 0 0 22 0 1 0 1788724228 7692288 1554 4294967295 134512640 135450776 3221224560 3221223376 134550433 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24605/statm): 1878 1554 232 232 0 1646 0 [pid=24605] vsize: 7512 Current children cumulated CPU time (s) 91.21 Current children cumulated vsize (Kb) 7512 [startup+110.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 1896 0 0 0 9646 451 0 0 25 0 1 0 1788724228 11886592 1733 4294967295 134512640 135450776 3221224560 3221223264 134536576 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24605/statm): 2902 1733 232 232 0 2670 0 [pid=24605] vsize: 11608 Current children cumulated CPU time (s) 100.97 Current children cumulated vsize (Kb) 11608 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 2040 0 0 0 10587 471 0 0 25 0 1 0 1788724228 12050432 1877 4294967295 134512640 135450776 3221224560 3221223280 134539323 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24605/statm): 2942 1877 232 232 0 2710 0 [pid=24605] vsize: 11768 Current children cumulated CPU time (s) 110.58 Current children cumulated vsize (Kb) 11768 [startup+130.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 2294 0 0 0 11507 495 0 0 25 0 1 0 1788724228 12480512 2131 4294967295 134512640 135450776 3221224560 3221223152 134538585 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24605/statm): 3047 2131 232 232 0 2815 0 [pid=24605] vsize: 12188 Current children cumulated CPU time (s) 120.02 Current children cumulated vsize (Kb) 12188 [startup+140.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) R 24604 24605 9854 0 -1 0 2564 0 0 0 12438 517 0 0 25 0 1 0 1788724228 13266944 2208 4294967295 134512640 135450776 3221224560 3221223244 134538691 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24605/statm): 3239 2208 232 232 0 3007 0 [pid=24605] vsize: 12956 Current children cumulated CPU time (s) 129.55 Current children cumulated vsize (Kb) 12956 [startup+150.012 s] Raw data (loadavg): 0.99 0.97 0.91 1/56 24605 Raw data (/proc/24605/stat): 24605 (PBS4) T 24604 24605 9854 0 -1 0 2601 0 0 0 13300 564 0 0 21 0 1 0 1788724228 13402112 2245 4294967295 134512640 135450776 3221224560 3221223420 135126769 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/24605/statm): 3272 2245 232 232 0 3040 0 [pid=24605] vsize: 13088 Current children cumulated CPU time (s) 138.64 Current children cumulated vsize (Kb) 13088 One traced child (pid=24605) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 157.097 CPU time (s): 144.569 CPU user time (s): 138.4 CPU system time (s): 6.16906 CPU usage (%): 92.025 Max. virtual memory (cumulated for all children) (Kb): 13088
Verifier: OK 258411