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