Name | web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.5:100.opb |
MD5SUM | feaa96df552ef9989407735877840272 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 12 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 776 |
Biggest coefficient in the objective function | 474 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 2127 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 474 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 2127 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1213.45 |
Number of variables | 776 |
Total number of constraints | 1642 |
Number of constraints which are clauses | 701 |
Number of constraints which are cardinality constraints (but not clauses) | 941 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 20 |
LAUNCH ON wulflinc21 THE 2005-09-18 18:04:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=1566 boxname=wulflinc21 idbench=394 idsolver=2 numberseed=0 MD5SUM SOLVER: 1540ae3c74fe6bb56fea7dc39e0baf99 /oldhome/oroussel/solvers/galena MD5SUM BENCH: feaa96df552ef9989407735877840272 /oldhome/oroussel/tmp/wulflinc21/normalized-10:20:4.5:0.5:100.opb REAL COMMAND: galena /oldhome/oroussel/tmp/wulflinc21/normalized-10:20:4.5:0.5:100.opb IDLAUNCH: 1566 /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: 894892 kB Buffers: 35044 kB Cached: 77200 kB SwapCached: 908 kB Active: 78864 kB Inactive: 36092 kB HighTotal: 131008 kB HighFree: 57624 kB LowTotal: 903652 kB LowFree: 837268 kB SwapTotal: 2097892 kB SwapFree: 2096472 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5804 kB Slab: 19160 kB Committed_AS: 64332 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:04:28 (client local time) WITH STATUS 10 IN 1.06684 SECONDS stats: 1566 0 1.06684 10
c Decisions: 2865 c Implications: 13842 c RUNTIME: 1.00385s v -v756 v693 -v588 v262 -v241 v56 -v38 v692 -v590 -v486 v263 -v246 v55 -v37 v757 v700 v589 -v485 -v439 -v266 -v245 v54 v39 -v758 v694 v594 -v487 -v444 -v264 -v52 v40 -v761 v695 -v612 v593 v488 -v443 -v265 v248 -v53 v47 -v759 -v696 v611 -v591 v489 -v401 -v249 v41 -v2 -v760 v613 -v592 v496 v446 -v421 v400 -v252 -v198 -v171 v42 -v1 -v734 -v616 v490 -v447 v420 v406 -v385 -v250 -v176 -v43 -v3 -v733 v615 v491 -v450 v422 v405 -v384 -v273 -v251 v197 -v175 -v137 v4 v620 -v492 -v448 -v425 -v407 -v386 -v366 -v278 v201 -v155 v136 -v18 v5 -v735 v619 -v559 -v510 -v449 v424 v411 v387 -v365 -v277 v178 -v154 v138 -v87 v17 v12 -v737 -v650 -v617 -v515 v429 -v410 v388 -v202 -v179 -v156 -v141 v86 -v23 v6 -v649 -v618 v558 -v514 -v466 v428 -v408 v395 -v367 v280 -v182 v157 v140 v88 -v66 v22 v7 -v738 v562 -v426 -v409 v389 -v369 -v281 -v180 v158 v145 -v91 -v71 -v24 -v8 v740 -v651 v517 v469 -v427 v390 -v318 -v284 -v223 -v181 v165 v144 -v121 v90 -v70 v28 -v741 -v653 -v635 -v563 -v518 -v470 -v391 -v370 v317 -v282 v159 -v142 v95 -v27 -v634 -v521 v372 -v347 v319 -v283 v222 v160 -v143 v120 v94 v73 -v25 -v654 -v519 -v373 -v351 -v322 v226 -v161 -v92 v74 -v26 v656 -v636 -v520 v321 -v124 -v93 -v75 -v657 v639 v323 v227 -v125 -v76 -v753 v703 v64 v755 v704 v587 v267 v240 v60 v754 -v699 v602 v242 -v59 -v50 v762 v598 v438 v247 v51 -v710 -v697 -v597 -v499 v440 v244 v46 -v714 v500 v445 v253 -v495 v442 v44 -v729 v614 v451 v402 v170 v728 v628 -v493 v403 v199 v172 -v15 v624 v423 v404 -v361 v272 v203 v177 v16 v736 -v623 v437 v415 -v398 v360 v274 v174 -v11 v739 -v645 v509 v433 v399 v279 v183 v139 v19 v743 v644 v560 v511 v465 -v432 -v394 v368 v276 v205 -v168 v153 v20 -v9 v742 v564 v516 v371 v285 -v206 v169 v149 v89 v65 v21 v652 v513 v471 -v392 v375 -v164 -v148 -v116 v103 v67 v32 v655 -v630 v522 v374 v99 v72 v659 v629 v566 v346 v224 -v162 v122 -v98 v69 v658 -v567 v350 v320 v228 v77 v637 -v474 v331 v126 v638 v327 -v701 v599 -v105 v63 -v49 v752 v601 v271 -v48 v770 -v498 -v270 -v57 v766 -v497 v243 v765 v709 -v698 -v595 v261 -v58 v713 v441 v257 -v193 v625 -v596 v459 -v302 -v256 v192 -v45 -v14 v627 v455 -v13 -v494 v454 v434 -v418 -v397 v200 v730 -v554 v436 v419 -v396 v204 v173 v731 -v621 v553 -v461 -v414 v208 v191 -v167 v150 v732 v362 v275 v207 v187 -v166 v152 v747 -v622 v561 v467 -v430 -v412 v363 v293 -v186 v100 -v35 -v10 v646 v565 v512 v364 v289 -v218 v102 v36 -v685 v647 v569 v530 v472 -v431 -v393 v379 -v288 v217 -v146 -v31 v648 v568 v526 v115 v68 v663 -v525 -v475 v348 v328 v225 -v163 -v147 v117 -v96 v85 -v29 v631 -v473 v352 v330 v229 v123 v81 v632 v230 v119 -v97 -v80 v633 v326 -v231 -v127 v767 -v702 v600 -v333 v104 v61 v769 -v268 v258 v260 v763 v711 v456 -v299 -v269 v715 -v626 v458 -v764 -v417 v301 -v254 -v435 -v416 v194 v717 v452 -v255 v195 v188 -v718 v196 v190 -v151 -v750 v453 v290 v212 -v34 v751 v555 v460 v292 -v101 -v33 -v746 -v681 v556 v527 v462 -v413 -v382 -v184 v557 v529 v468 v383 -v343 -v744 v684 -v666 v573 v464 -v378 v342 -v286 -v185 v82 v667 v476 -v329 v219 v84 -v662 -v534 -v523 -v376 v349 -v287 v220 -v30 -v538 v353 v221 v118 -v660 -v642 -v604 -v524 v354 v235 v135 -v78 v643 -v608 -v355 v324 v131 v768 v332 v106 -v62 -v706 -v259 v705 -v457 v712 v298 -v108 v716 v720 v303 v719 -v189 -v749 v215 -v748 -v291 v216 -v677 -v381 -v306 v211 -v528 -v380 v680 -v665 v576 v209 -v664 v577 v463 -v83 -v745 v686 -v572 v484 v480 v344 -v641 -v570 v533 -v479 -v377 v345 -v238 v132 -v640 v537 v239 v134 -v689 -v661 v603 -v234 -v79 v607 v325 v130 -v502 -v295 v109 v707 v107 v708 -v546 v335 v300 v771 v724 v304 -v214 -v213 v673 v307 v305 v772 v676 v773 -v575 v574 v682 v481 -v210 v483 v687 -v237 -v236 -v133 -v690 -v571 v535 -v477 v358 -v688 v539 v359 v605 -v478 -v232 v609 v128 v110 v501 v336 v334 v294 v727 v545 v296 -v723 v308 -v721 v672 v582 -v482 v683 -v532 -v679 v531 -v357 v691 v356 v536 v540 v606 -v233 v610 -v129 v337 v114 v726 v503 v113 v725 v547 v297 -v669 -v506 v316 v312 -v722 v674 v581 v549 -v311 v550 v678 v586 -v542 v341 -v541 v504 v340 v111 v548 -v507 v313 v112 -v505 v315 v580 v552 v668 v551 v670 v583 -v309 v675 -v310 v585 v338 v543 v508 v314 v544 v339 v774 v579 v578 v671 v584 v775 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/30471/stat): 30471 (galena) R 30470 30471 20602 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 1720542308 1015808 2 4294967295 134512640 135412752 3221224560 3221224560 134512896 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/30471/statm): 248 2 241 241 0 7 0 [pid=30471] vsize: 992 open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-10:20:4.5:0.5:100.opb One traced child (pid=30471) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1.1474 CPU time (s): 1.06684 CPU user time (s): 1.01584 CPU system time (s): 0.050992 CPU usage (%): 92.9788 Max. virtual memory (cumulated for all children) (Kb): 0
Verifier: OK 277