Name | normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb |
MD5SUM | dd81121db7c1c4b8597dd9571c707a87 |
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 | 372 |
Biggest coefficient in the objective function | 220 |
Number of bits for the biggest coefficient in the objective function | 8 |
Sum of the numbers in the objective function | 983 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 220 |
Number of bits of the biggest number in a constraint | 8 |
Biggest sum of numbers in a constraint | 983 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.03484 |
Number of variables | 372 |
Total number of constraints | 792 |
Number of constraints which are clauses | 345 |
Number of constraints which are cardinality constraints (but not clauses) | 447 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 18 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc19 THE 2005-04-13 08:16:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3289 boxname=wulflinc19 idbench=366 idsolver=4 numberseed=0 MD5SUM SOLVER: 1540ae3c74fe6bb56fea7dc39e0baf99 /oldhome/oroussel/solvers/galena MD5SUM BENCH: dd81121db7c1c4b8597dd9571c707a87 /oldhome/oroussel/tmp/wulflinc19/normalized-10:10:4.5:0.5:100.opb REAL COMMAND: galena /oldhome/oroussel/tmp/wulflinc19/normalized-10:10:4.5:0.5:100.opb IDLAUNCH: 3289 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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.037 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: 888220 kB Buffers: 16596 kB Cached: 96008 kB SwapCached: 72 kB Active: 23892 kB Inactive: 91960 kB HighTotal: 131008 kB HighFree: 30296 kB LowTotal: 903652 kB LowFree: 857924 kB SwapTotal: 2097892 kB SwapFree: 2097820 kB Dirty: 40 kB Writeback: 0 kB Mapped: 7392 kB Slab: 24968 kB Committed_AS: 64048 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-13 08:16:18 (client local time) WITH STATUS 10 IN SECONDS stats: 3289 0 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Decisions: 5627 c Implications: 23779 c RUNTIME: 1.00085s v v287 -v229 -v148 -v112 v97 v75 -v45 -v23 v285 -v270 -v233 -v147 -v128 -v113 -v44 -v28 -v269 -v232 v196 -v149 -v127 -v117 -v98 v79 -v46 -v27 -v2 v286 -v271 -v253 -v234 v195 -v166 -v152 -v133 -v115 -v99 v77 -v47 -v7 -v291 -v272 -v252 -v238 v197 -v165 -v151 -v132 -v116 v102 -v54 -v30 -v6 -v343 v273 -v237 v200 -v171 -v156 -v134 v100 -v78 -v48 -v31 -v342 v280 -v254 -v235 v199 -v170 -v155 -v138 v101 -v82 -v49 -v34 -v9 -v344 v274 v256 -v236 -v203 v172 -v153 -v137 -v50 -v32 -v10 -v345 v275 -v201 v173 -v154 -v135 -v33 -v11 -v346 v276 v257 -v202 v174 -v136 -v12 -v305 v288 -v114 v94 v74 -v309 -v228 -v118 v96 -v22 -v292 -v230 v95 v80 -v57 -v24 -v290 -v248 -v231 -v150 -v129 v103 -v58 -v29 -v1 v283 -v247 -v242 -v164 -v130 -v83 -v53 -v26 -v3 v284 v198 -v167 -v160 -v131 -v81 -v35 -v8 v279 v255 -v221 -v211 -v168 -v159 -v142 -v51 -v5 v258 -v207 v169 -v13 -v349 v277 -v259 -v206 v188 v178 -v350 -v260 v192 -v304 v289 -v126 v72 -v56 -v308 v293 -v122 v93 v76 -v55 -v282 -v245 -v161 -v121 v111 v73 v281 -v246 -v163 v107 -v84 -v25 -v360 -v241 v217 -v208 -v145 v106 -v43 -v249 -v210 -v146 -v39 -v4 -v348 -v250 -v239 -v220 v181 -v157 -v141 -v52 -v38 -v21 -v347 v251 v182 -v17 v278 v264 -v204 v187 v177 -v158 -v139 -v16 v191 -v306 v301 -v244 -v125 v108 -v310 v297 -v243 -v162 v110 v71 -v356 v296 -v144 -v119 v92 -v40 -v209 -v143 v88 -v42 -v359 -v312 v216 v180 -v120 -v104 v87 -v64 -v18 -v313 v179 -v20 v267 -v240 -v222 -v105 -v36 v268 -v336 v263 -v205 v189 v175 -v140 -v37 -v14 -v340 v193 -v307 v300 -v123 v109 v89 -v311 v91 -v41 -v355 -v315 v294 -v213 -v60 -v314 -v19 -v361 v295 v266 v218 v85 -v63 v265 -v184 -v223 -v183 v86 v364 -v335 v261 v190 -v176 -v15 -v339 v194 v352 -v303 v298 -v124 v90 -v302 -v357 -v319 -v59 v212 -v362 v328 v214 -v65 v219 v365 v363 -v185 -v337 v262 -v186 -v68 -v341 -v322 v299 v351 -v323 v353 v325 -v318 -v61 -v358 v327 -v316 -v66 v366 -v332 v215 -v331 -v227 v69 -v67 -v338 -v320 v324 v354 -v62 v329 -v317 -v224 v370 -v226 v70 v369 -v333 -v334 -v321 v326 -v225 v330 v367 -v368 v371 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.96 0.97 0.91 2/55 19288 Raw data (stat): 19288 (runsolver) R 19287 10867 10866 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 474433836 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.0439 s] Raw data (loadavg): 0.97 0.97 0.91 1/54 19288 Raw data (stat): 19288 (runsolver) R 19287 10867 10866 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 474433836 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.04328 CPU time (s): 1.03484 CPU user time (s): 1.01085 CPU system time (s): 0.023996 CPU usage (%): 99.1914 Max. virtual memory (Kb): 1032 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 17 #### END VERIFIER DATA ####