Name | 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 | 7 |
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 | 1205.78 |
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 |
LAUNCH ON wulflinc22 THE 2005-09-18 18:04:22 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=1565 boxname=wulflinc22 idbench=393 idsolver=2 numberseed=0 MD5SUM SOLVER: 1540ae3c74fe6bb56fea7dc39e0baf99 /oldhome/oroussel/solvers/galena MD5SUM BENCH: ac510382bae6003fe0373ad32fd0064f /oldhome/oroussel/tmp/wulflinc22/normalized-10:10:4.5:0.95:98.opb REAL COMMAND: galena /oldhome/oroussel/tmp/wulflinc22/normalized-10:10:4.5:0.95:98.opb IDLAUNCH: 1565 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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.031 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: 912552 kB Buffers: 34596 kB Cached: 59932 kB SwapCached: 536 kB Active: 66736 kB Inactive: 30304 kB HighTotal: 131008 kB HighFree: 69076 kB LowTotal: 903652 kB LowFree: 843476 kB SwapTotal: 2097892 kB SwapFree: 2096832 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5864 kB Slab: 19416 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:04:24 (client local time) WITH STATUS 10 IN 1.07084 SECONDS stats: 1565 0 1.07084 10
c Decisions: 2970 c Implications: 18970 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
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/32209/stat): 32209 (galena) R 32208 32209 21452 0 -1 0 18 0 0 0 0 0 0 0 22 0 1 0 1843272554 1015808 2 4294967295 134512640 135412752 3221224560 3221224560 134512896 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/32209/statm): 248 2 241 241 0 7 0 [pid=32209] vsize: 992 open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-10:10:4.5:0.95:98.opb One traced child (pid=32209) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1.15799 CPU time (s): 1.07084 CPU user time (s): 1.01185 CPU system time (s): 0.058991 CPU usage (%): 92.474 Max. virtual memory (cumulated for all children) (Kb): 0
Verifier: OK 99