Name | normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:98.opb |
MD5SUM | ac510382bae6003fe0373ad32fd0064f |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 5 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 411 |
Biggest coefficient in the objective function | 268 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 1129 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 268 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 1129 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.03584 |
Number of variables | 411 |
Total number of constraints | 887 |
Number of constraints which are clauses | 387 |
Number of constraints which are cardinality constraints (but not clauses) | 500 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 16 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc20 THE 2005-04-13 08:23:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3307 boxname=wulflinc20 idbench=368 idsolver=4 numberseed=0 MD5SUM SOLVER: 1540ae3c74fe6bb56fea7dc39e0baf99 /oldhome/oroussel/solvers/galena MD5SUM BENCH: ac510382bae6003fe0373ad32fd0064f /oldhome/oroussel/tmp/wulflinc20/normalized-10:10:4.5:0.95:98.opb REAL COMMAND: galena /oldhome/oroussel/tmp/wulflinc20/normalized-10:10:4.5:0.95:98.opb IDLAUNCH: 3307 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 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: 880080 kB Buffers: 17100 kB Cached: 101912 kB SwapCached: 2640 kB Active: 19772 kB Inactive: 105024 kB HighTotal: 131008 kB HighFree: 24780 kB LowTotal: 903652 kB LowFree: 855300 kB SwapTotal: 2097892 kB SwapFree: 2095252 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7288 kB Slab: 24112 kB Committed_AS: 63824 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-13 08:23:27 (client local time) WITH STATUS 10 IN SECONDS stats: 3307 0 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Decisions: 2948 c Implications: 18837 c RUNTIME: 1.00185s v v294 -v230 -v205 v190 v138 v293 v210 v191 -v142 -v358 v301 -v278 -v234 v209 v195 v295 -v232 v194 v357 v296 v212 -v192 -v118 v361 -v297 -v233 v213 -v193 v179 -v82 -v237 -v216 v178 -v163 v117 -v81 -v362 -v214 v121 v83 -v215 v180 v162 v84 -v183 v167 v122 v85 -v304 -v274 v229 v189 v137 -v305 v204 v188 v141 -v384 -v300 v277 -v235 v206 -v199 v211 v359 -v312 -v298 -v238 v208 -v36 v363 -v316 -v236 v217 -v174 v173 v119 v123 -v365 v181 v164 -v88 -v366 -v182 v166 v89 -v380 -v302 -v273 v227 v202 v139 -v353 v231 v203 v143 v383 v352 v279 v228 -v198 -v32 -v239 v207 -v113 v360 v311 -v299 v225 -v196 v145 v112 v35 v364 v315 -v221 -v158 -v146 -v368 -v282 -v220 v157 v120 -v87 -v367 v175 v124 -v86 -v341 v176 v165 v125 -v70 v177 v168 -v126 v74 -v379 -v303 -v275 v200 v140 v226 v144 -v396 v385 v280 v247 v222 v148 v31 -v400 v354 -v243 v224 v147 v355 v313 -v283 -v242 -v197 v37 -v7 v356 v317 -v281 v114 -v11 -v388 -v372 -v337 -v218 v115 -v100 v159 v116 -v340 v319 -v219 -v186 v160 v130 v69 -v40 -v320 v187 v161 v73 -v381 -v271 v244 v201 v136 -v27 -v307 -v276 v246 -v223 v135 v395 v386 v306 v272 -v152 v33 v399 -v284 -v389 -v375 v314 -v240 -v96 v38 v6 -v387 -v376 v318 v10 -v371 v336 v322 -v241 -v185 -v133 v99 -v41 v321 -v184 -v134 -v39 -v369 -v342 -v254 -v171 v129 v71 -v258 v172 v75 -v378 -v264 v245 v155 v382 -v270 v156 v26 v397 -v374 v292 -v151 v28 v401 v390 -v373 v308 -v288 v34 -v332 v309 -v287 -v149 -v132 v95 v30 v8 v310 -v131 -v65 -v42 v12 -v403 v338 -v326 -v170 v101 -v64 -v404 -v169 -v370 -v343 -v253 v127 v72 -v60 v14 v257 v76 -v15 v289 v263 -v153 v377 v291 -v2 v398 -v91 v1 v402 v394 v29 v406 -v393 -v329 -v285 -v150 v97 v50 v9 -v405 v331 -v330 -v46 v13 v333 -v325 -v286 v102 -v56 -v45 v17 v339 -v66 v16 v335 -v323 -v255 -v128 -v103 v67 -v59 v344 v259 -v104 v68 -v290 v265 -v154 -v328 v47 -v327 v90 v49 v3 v410 -v391 -v267 v92 v4 -v249 v98 v5 -v392 v248 v94 v55 -v43 -v21 v334 -v105 v351 -v324 -v256 -v79 v61 -v44 v347 v260 v80 -v48 -v268 -v266 -v409 v53 v24 v93 v25 -v407 v348 v111 -v78 v57 -v20 v350 v250 -v108 -v77 v251 -v106 v62 -v18 v345 v252 v269 v23 v22 v110 -v349 v109 v52 -v408 v51 v58 v262 -v107 v54 -v19 v346 v261 v63 one s SATISFIABLE #### 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 24913 Raw data (stat): 24913 (runsolver) R 24912 16631 16630 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 474480592 1056768 100 4294967295 134512640 135381576 3221221744 3221216500 135158418 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 1032 [startup+1.04563 s] Raw data (loadavg): 0.92 0.95 0.90 1/53 24913 Raw data (stat): 24913 (runsolver) R 24912 16631 16630 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 474480592 1056768 100 4294967295 134512640 135381576 3221221744 3221216500 135158418 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 0 Child status: 10 Real time (s): 1.04501 CPU time (s): 1.03584 CPU user time (s): 1.01185 CPU system time (s): 0.023996 CPU usage (%): 99.1227 Max. virtual memory (Kb): 1032 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 99 #### END VERIFIER DATA ####