Name | submitted/een/normalized-p0282.opb |
MD5SUM | dd62132555621025f45a5a6099c90742 |
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 | 24.5993 |
Number of variables | 282 |
Total number of constraints | 221 |
Number of constraints which are clauses | 177 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 44 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 57 |
LAUNCH ON wulflinc21 THE 2005-09-18 19:46:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3790 boxname=wulflinc21 idbench=274 idsolver=4 numberseed=0 MD5SUM SOLVER: 21c3ffd7205c96d5f0784fd273b92938 /oldhome/oroussel/solvers/PBS4 MD5SUM BENCH: dd62132555621025f45a5a6099c90742 /oldhome/oroussel/tmp/wulflinc21/normalized-p0282.opb REAL COMMAND: PBS4 /oldhome/oroussel/tmp/wulflinc21/normalized-p0282.opb IDLAUNCH: 3790 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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 : 3 cpu MHz : 451.161 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: 895060 kB Buffers: 35156 kB Cached: 77496 kB SwapCached: 908 kB Active: 79036 kB Inactive: 36240 kB HighTotal: 131008 kB HighFree: 57400 kB LowTotal: 903652 kB LowFree: 837660 kB SwapTotal: 2097892 kB SwapFree: 2096472 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5804 kB Slab: 18656 kB Committed_AS: 64368 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:49:51 (client local time) WITH STATUS 30 IN 188.727 SECONDS stats: 3790 0 188.727 30
c PBS v4 by Bashar Al-Rawi & Fadi Aloul c Solving /oldhome/oroussel/tmp/wulflinc21/normalized-p0282.opb ...... c The optimum solution is:258411 s OPTIMUM FOUND v -x0 -x1 -x10 -x100 x101 -x102 x103 -x104 -x105 -x106 -x107 -x108 -x109 x11 -x110 -x111 -x112 -x113 -x114 -x115 -x116 x117 -x118 -x119 -x12 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x13 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x14 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x15 -x150 -x151 -x152 -x153 -x154 x155 -x156 -x157 -x158 -x159 -x16 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 x169 -x17 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x18 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x19 -x190 x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 x199 -x2 -x20 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x21 -x210 -x211 -x212 -x213 -x214 x215 -x216 -x217 -x218 -x219 -x22 -x220 -x221 -x222 x223 -x224 x225 -x226 -x227 -x228 -x229 -x23 -x230 -x231 -x232 -x233 -x234 -x235 -x236 x237 -x238 -x239 -x24 x240 -x241 x242 x243 x244 -x245 x246 -x247 x248 -x249 -x25 -x250 x251 -x252 -x253 x254 -x255 x256 x257 -x258 -x259 -x26 x260 -x261 x262 x263 -x264 -x265 -x266 -x267 -x268 -x269 -x27 -x270 -x271 -x272 x273 -x274 x275 x276 x277 -x278 -x279 -x28 x280 x281 -x29 x3 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x4 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x5 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x6 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x7 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x8 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x9 -x90 x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 c Done, CPU Time=188.692
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/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 1721154509 978944 2 4294967295 134512640 135450776 3221224576 3221224576 134512960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 239 2 232 232 0 7 0 [pid=31362] vsize: 956 open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-p0282.opb open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-p0282.opb [startup+10.0019 s] Raw data (loadavg): 0.93 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 517 0 0 0 722 86 0 0 18 0 1 0 1721154509 3633152 500 4294967295 134512640 135450776 3221224576 3221223280 134536656 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 887 500 232 232 0 655 0 [pid=31362] vsize: 3548 Current children cumulated CPU time (s) 8.08 Current children cumulated vsize (Kb) 3548 [startup+20.0026 s] Raw data (loadavg): 0.94 0.98 0.92 1/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) T 31361 31362 20602 0 -1 0 754 0 0 0 1561 139 0 0 16 0 1 0 1721154509 3973120 737 4294967295 134512640 135450776 3221224576 3221223436 135126769 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/31362/statm): 970 737 232 232 0 738 0 [pid=31362] vsize: 3880 Current children cumulated CPU time (s) 17 Current children cumulated vsize (Kb) 3880 [startup+30.0033 s] Raw data (loadavg): 0.95 0.98 0.92 1/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) T 31361 31362 20602 0 -1 0 973 0 0 0 2409 189 0 0 16 0 1 0 1721154509 6406144 907 4294967295 134512640 135450776 3221224576 3221223436 135126769 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/31362/statm): 1564 907 232 232 0 1332 0 [pid=31362] vsize: 6256 Current children cumulated CPU time (s) 25.98 Current children cumulated vsize (Kb) 6256 [startup+40.003 s] Raw data (loadavg): 0.96 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1073 0 0 0 3267 236 0 0 17 0 1 0 1721154509 6545408 1007 4294967295 134512640 135450776 3221224576 3221223392 134550433 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 1598 1007 232 232 0 1366 0 [pid=31362] vsize: 6392 Current children cumulated CPU time (s) 35.03 Current children cumulated vsize (Kb) 6392 [startup+50.0036 s] Raw data (loadavg): 0.96 0.98 0.92 1/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) T 31361 31362 20602 0 -1 0 1111 0 0 0 4144 276 0 0 16 0 1 0 1721154509 6684672 1045 4294967295 134512640 135450776 3221224576 3221223436 135126769 0 0 5 0 3222434794 0 0 17 0 0 0 Raw data (/proc/31362/statm): 1632 1045 232 232 0 1400 0 [pid=31362] vsize: 6528 Current children cumulated CPU time (s) 44.2 Current children cumulated vsize (Kb) 6528 [startup+60.0043 s] Raw data (loadavg): 0.97 0.98 0.92 1/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) T 31361 31362 20602 0 -1 0 1217 0 0 0 5018 316 0 0 16 0 1 0 1721154509 6819840 1151 4294967295 134512640 135450776 3221224576 3221223436 135126769 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/31362/statm): 1665 1151 232 232 0 1433 0 [pid=31362] vsize: 6660 Current children cumulated CPU time (s) 53.34 Current children cumulated vsize (Kb) 6660 [startup+70.005 s] Raw data (loadavg): 0.97 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1369 0 0 0 5928 344 0 0 18 0 1 0 1721154509 7213056 1206 4294967295 134512640 135450776 3221224576 3221223392 134550480 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 1761 1206 232 232 0 1529 0 [pid=31362] vsize: 7044 Current children cumulated CPU time (s) 62.72 Current children cumulated vsize (Kb) 7044 [startup+80.0057 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1532 0 0 0 6857 369 0 0 17 0 1 0 1721154509 7507968 1369 4294967295 134512640 135450776 3221224576 3221223392 134550808 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 1833 1369 232 232 0 1601 0 [pid=31362] vsize: 7332 Current children cumulated CPU time (s) 72.26 Current children cumulated vsize (Kb) 7332 [startup+90.0054 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1602 0 0 0 7782 393 0 0 17 0 1 0 1721154509 7507968 1439 4294967295 134512640 135450776 3221224576 3221223392 134550478 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 1833 1439 232 232 0 1601 0 [pid=31362] vsize: 7332 Current children cumulated CPU time (s) 81.75 Current children cumulated vsize (Kb) 7332 [startup+100.005 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1643 0 0 0 8718 414 0 0 17 0 1 0 1721154509 7643136 1480 4294967295 134512640 135450776 3221224576 3221223392 134550478 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 1866 1480 232 232 0 1634 0 [pid=31362] vsize: 7464 Current children cumulated CPU time (s) 91.32 Current children cumulated vsize (Kb) 7464 [startup+110.006 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1663 0 0 0 9617 448 0 0 17 0 1 0 1721154509 7643136 1500 4294967295 134512640 135450776 3221224576 3221223280 134536567 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 1866 1500 232 232 0 1634 0 [pid=31362] vsize: 7464 Current children cumulated CPU time (s) 100.65 Current children cumulated vsize (Kb) 7464 [startup+120.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1681 0 0 0 10507 484 0 0 17 0 1 0 1721154509 7643136 1518 4294967295 134512640 135450776 3221224576 3221223408 134540208 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 1866 1518 232 232 0 1634 0 [pid=31362] vsize: 7464 Current children cumulated CPU time (s) 109.91 Current children cumulated vsize (Kb) 7464 [startup+130.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1715 0 0 0 11444 504 0 0 17 0 1 0 1721154509 7794688 1552 4294967295 134512640 135450776 3221224576 3221223436 135126769 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/31362/statm): 1903 1552 232 232 0 1671 0 [pid=31362] vsize: 7612 Current children cumulated CPU time (s) 119.48 Current children cumulated vsize (Kb) 7612 [startup+140.008 s] Raw data (loadavg): 1.06 1.00 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 1988 0 0 0 12391 522 0 0 24 0 1 0 1721154509 8728576 1632 4294967295 134512640 135450776 3221224576 3221223392 134550433 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 2131 1632 232 232 0 1899 0 [pid=31362] vsize: 8524 Current children cumulated CPU time (s) 129.13 Current children cumulated vsize (Kb) 8524 [startup+150.008 s] Raw data (loadavg): 1.05 1.00 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 2103 0 0 0 13334 542 0 0 25 0 1 0 1721154509 8888320 1747 4294967295 134512640 135450776 3221224576 3221223296 134539307 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 2170 1747 232 232 0 1938 0 [pid=31362] vsize: 8680 Current children cumulated CPU time (s) 138.76 Current children cumulated vsize (Kb) 8680 [startup+160.011 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 2254 0 0 0 14282 559 0 0 19 0 1 0 1721154509 13082624 1898 4294967295 134512640 135450776 3221224576 3221223392 134550433 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 3194 1898 232 232 0 2962 0 [pid=31362] vsize: 12776 Current children cumulated CPU time (s) 148.41 Current children cumulated vsize (Kb) 12776 [startup+170.011 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 2393 0 0 0 15245 572 0 0 25 0 1 0 1721154509 13082624 2037 4294967295 134512640 135450776 3221224576 3221223392 134550469 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/31362/statm): 3194 2037 232 232 0 2962 0 [pid=31362] vsize: 12776 Current children cumulated CPU time (s) 158.17 Current children cumulated vsize (Kb) 12776 [startup+180.012 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 2607 0 0 0 16182 594 0 0 25 0 1 0 1721154509 13516800 2251 4294967295 134512640 135450776 3221224576 3221223088 134545179 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 3300 2251 232 232 0 3068 0 [pid=31362] vsize: 13200 Current children cumulated CPU time (s) 167.76 Current children cumulated vsize (Kb) 13200 [startup+190.012 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 2640 0 0 0 17113 619 0 0 17 0 1 0 1721154509 13684736 2284 4294967295 134512640 135450776 3221224576 3221222912 134534084 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 3341 2284 232 232 0 3109 0 [pid=31362] vsize: 13364 Current children cumulated CPU time (s) 177.32 Current children cumulated vsize (Kb) 13364 [startup+200.012 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 31362 Raw data (/proc/31362/stat): 31362 (PBS4) R 31361 31362 20602 0 -1 0 2678 0 0 0 18014 650 0 0 17 0 1 0 1721154509 13684736 2322 4294967295 134512640 135450776 3221224576 3221223392 134550441 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31362/statm): 3341 2322 232 232 0 3109 0 [pid=31362] vsize: 13364 Current children cumulated CPU time (s) 186.64 Current children cumulated vsize (Kb) 13364 One traced child (pid=31362) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 202.441 CPU time (s): 188.727 CPU user time (s): 182.07 CPU system time (s): 6.65699 CPU usage (%): 93.2256 Max. virtual memory (cumulated for all children) (Kb): 13364
Verifier: OK 258411