Name | web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-5.opb |
MD5SUM | 6049145b9f1adfd7114adf044503d587 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2642 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 748 |
Biggest coefficient in the objective function | 240 |
Number of bits for the biggest coefficient in the objective function | 8 |
Sum of the numbers in the objective function | 33855 |
Number of bits of the sum of numbers in the objective function | 16 |
Biggest number in a constraint | 240 |
Number of bits of the biggest number in a constraint | 8 |
Biggest sum of numbers in a constraint | 33855 |
Number of bits of the biggest sum of numbers | 16 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 965.053 |
Number of variables | 907 |
Total number of constraints | 1309 |
Number of constraints which are clauses | 126 |
Number of constraints which are cardinality constraints (but not clauses) | 1183 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 134 |
LAUNCH ON wulflinc18 THE 2005-09-18 18:04:14 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=1556 boxname=wulflinc18 idbench=384 idsolver=2 numberseed=0 MD5SUM SOLVER: 1540ae3c74fe6bb56fea7dc39e0baf99 /oldhome/oroussel/solvers/galena MD5SUM BENCH: 6049145b9f1adfd7114adf044503d587 /oldhome/oroussel/tmp/wulflinc18/normalized-ws97-5.opb REAL COMMAND: galena /oldhome/oroussel/tmp/wulflinc18/normalized-ws97-5.opb IDLAUNCH: 1556 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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.177 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: 917124 kB Buffers: 35216 kB Cached: 47716 kB SwapCached: 844 kB Active: 65208 kB Inactive: 20356 kB HighTotal: 131008 kB HighFree: 80360 kB LowTotal: 903652 kB LowFree: 836764 kB SwapTotal: 2097892 kB SwapFree: 2096548 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5764 kB Slab: 26456 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:04:16 (client local time) WITH STATUS 10 IN 1.05484 SECONDS stats: 1556 0 1.05484 10
c Decisions: 1842 c Implications: 9248 c RUNTIME: 1.00085s v v1 -v127 -v505 v640 -v774 -v4 v256 v508 -v5 v131 -v257 -v383 v509 -v6 v132 -v258 v510 -v7 v133 v512 -v8 v134 v513 v388 -v516 v11 -v137 -v517 -v12 v138 v518 -v14 v392 v520 -v15 v141 -v267 v521 -v16 v394 v522 -v17 v143 v523 -v18 v396 v524 v19 -v525 v659 -v20 v146 v526 -v21 v273 v527 v22 -v528 v662 -v23 v149 v529 -v24 v150 v530 -v25 v151 -v403 v531 -v26 v152 v532 -v27 v153 v533 -v28 v406 v534 -v29 v407 v535 v30 -v156 -v536 -v31 v157 v537 v32 -v158 v672 -v806 v33 -v159 -v285 -v539 -v34 v160 v540 v287 -v413 v36 -v162 -v542 -v37 v163 v543 -v38 v164 v544 v39 -v545 v679 -v813 -v40 v166 v546 v41 -v419 -v547 -v42 v168 v548 -v43 v421 v549 -v44 v170 v550 v551 v45 -v171 -v552 v686 v46 -v172 -v553 -v47 v173 -v425 v554 -v48 v174 -v426 v555 -v49 v175 v556 v428 -v51 v177 v558 -v52 v178 v559 v431 v694 -v828 -v54 v180 -v432 v561 -v55 v433 v562 v56 -v308 -v563 v697 -v831 -v57 v435 v564 v58 -v436 -v565 v566 -v59 v185 v567 v568 v60 -v569 v703 -v837 -v61 v187 v570 v62 -v314 -v440 -v571 v705 -v839 -v63 v189 v572 -v64 v316 v573 -v65 v317 -v574 -v66 v318 v575 v67 -v193 -v576 v710 -v68 -v194 v320 -v577 v711 -v845 -v69 -v195 v447 -v578 -v70 v196 v579 v71 -v580 v714 v72 -v198 -v581 -v73 -v582 v74 -v200 -v583 v75 -v201 -v584 v76 -v202 -v585 -v78 -v204 v330 -v456 -v587 -v79 v457 -v588 v722 -v589 -v81 -v207 v333 -v459 -v590 -v82 v334 -v591 -v83 v335 -v461 -v592 v726 v727 -v861 v85 -v211 -v594 v728 -v862 -v86 -v212 v464 -v595 v87 -v213 -v596 v730 -v864 v88 -v214 -v597 -v89 v467 -v598 v732 -v90 -v216 v468 -v599 -v600 -v92 -v218 -v602 v93 -v219 -v603 v94 -v220 -v604 v738 -v872 -v96 -v222 -v606 v349 -v475 v741 v98 -v224 -v608 -v99 v351 -v477 -v609 v743 -v877 v226 v744 -v878 v227 v745 -v879 -v102 -v228 v354 -v480 -v612 -v103 -v229 v355 -v481 -v613 -v104 -v614 v748 -v105 -v231 v357 -v483 -v615 -v106 -v616 -v107 -v233 v485 -v617 v108 -v234 -v618 v109 -v235 -v619 v753 -v110 -v236 v362 -v488 -v620 v754 -v888 v756 -v890 -v113 v365 -v623 v240 -v115 -v241 v493 -v625 v759 v116 -v242 -v626 -v627 v761 -v895 -v117 v495 -v628 -v118 v370 -v630 v764 -v898 -v119 -v631 v765 -v899 v120 -v246 -v632 v766 -v900 -v121 v373 -v633 -v122 v374 -v500 -v634 v123 -v635 v903 -v124 v376 -v502 -v636 v770 -v904 v771 -v905 v126 -v638 v772 -v2 -v128 -v506 -v3 -v507 -v641 -v130 -v642 -v776 -v643 -v777 -v384 -v644 -v778 -v645 -v779 -v259 -v646 -v780 -v260 -v386 -v647 -v781 -v261 -v387 -v136 -v389 -v264 -v390 -v652 -v786 -v654 -v788 -v655 -v789 -v142 -v656 -v790 -v269 -v657 -v791 -v270 -v658 -v792 -v145 -v271 -v272 -v398 -v660 -v794 -v147 -v399 -v661 -v795 -v148 -v400 -v275 -v663 -v797 -v276 -v402 -v664 -v798 -v277 -v665 -v799 -v278 -v404 -v666 -v800 -v279 -v405 -v667 -v801 -v154 -v280 -v668 -v802 -v155 -v281 -v669 -v803 -v283 -v409 -v671 -v805 -v411 -v286 -v412 -v674 -v808 -v675 -v809 -v289 -v415 -v677 -v811 -v290 -v416 -v678 -v812 -v165 -v291 -v417 -v292 -v680 -v814 -v294 -v420 -v682 -v816 -v169 -v683 -v817 -v296 -v422 -v684 -v818 -v685 -v819 -v297 -v423 -v820 -v299 -v688 -v822 -v300 -v689 -v823 -v301 -v427 -v690 -v824 -v50 -v176 -v302 -v557 -v691 v825 -v303 -v429 -v692 -v826 -v304 -v430 -v693 -v827 -v53 -v179 -v305 -v560 -v306 -v695 -v829 -v181 -v696 -v830 -v182 -v434 -v183 -v309 -v698 -v832 -v184 -v310 -v700 -v834 -v311 -v437 -v701 -v835 -v702 -v836 -v186 -v312 -v438 -v313 -v439 -v704 -v838 -v188 -v315 -v706 -v840 -v190 -v442 -v707 -v841 -v191 -v443 -v192 -v444 -v709 -v843 -v319 -v445 -v844 -v446 -v321 -v846 -v322 -v448 -v713 -v847 -v197 -v323 -v449 -v324 -v450 -v715 v849 -v325 -v716 v850 -v326 -v452 -v717 v851 -v327 -v453 -v718 v852 -v328 -v454 -v719 v853 -v721 v855 -v205 -v331 -v856 -v206 -v724 v858 -v208 -v460 -v337 -v463 -v338 -v729 v863 -v339 -v465 -v340 -v466 -v731 v865 -v215 -v341 -v866 -v342 -v733 v867 -v217 -v344 -v736 v870 -v345 -v471 -v737 v871 -v346 -v472 -v347 -v739 v873 -v348 -v740 v874 -v350 -v476 -v742 v876 -v225 -v352 -v478 -v353 -v479 -v746 v880 -v747 v881 -v749 v883 -v484 -v750 v884 -v359 -v360 -v486 -v752 v886 -v361 -v487 -v887 -v755 v889 -v238 -v490 -v491 -v757 v891 -v114 -v366 -v492 -v624 -v367 -v893 -v368 -v494 -v760 v894 -v243 -v369 -v762 v896 -v245 -v497 -v372 -v498 -v247 -v499 -v767 v901 -v375 -v501 -v125 -v637 -v252 -v378 -v504 -v906 one -v9 -v10 -v13 -v35 -v77 -v80 -v84 -v91 -v95 -v97 -v100 -v101 -v111 -v112 -v129 v135 -v139 -v140 -v144 -v161 -v167 -v199 -v203 -v209 -v210 -v221 -v223 -v230 -v232 -v237 -v239 -v244 -v248 -v249 -v250 -v251 -v253 v254 v255 -v262 -v263 v265 -v266 -v268 -v274 -v282 -v284 -v288 -v293 -v295 -v298 -v307 -v329 v332 v336 v343 v356 v358 v363 v364 v371 v377 -v379 -v380 -v381 -v382 -v385 -v391 -v393 -v395 -v397 -v401 -v408 -v410 -v414 -v418 -v424 -v441 v451 v455 -v458 -v462 -v469 v470 v473 v474 -v482 -v489 -v496 -v503 v511 -v514 -v515 -v519 -v538 v541 v586 -v593 -v601 -v605 -v607 -v610 -v611 -v621 -v622 -v629 v639 v648 v649 v650 v651 v653 v670 v673 v676 v681 v687 -v699 -v708 v712 -v720 -v723 -v725 -v734 -v735 -v751 -v758 -v763 -v768 -v769 -v773 v775 -v782 -v783 -v784 -v785 -v787 -v793 -v796 -v804 -v807 -v810 -v815 -v821 v833 v842 -v848 -v854 v857 v859 -v860 v868 v869 -v875 -v882 v885 v892 v897 v902 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/4558/stat): 4558 (galena) R 4557 4558 31027 0 -1 0 18 0 0 0 0 0 0 0 21 0 1 0 1843237480 1015808 2 4294967295 134512640 135412752 3221224576 3221224576 134512896 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/4558/statm): 248 2 241 241 0 7 0 [pid=4558] vsize: 992 open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-ws97-5.opb One traced child (pid=4558) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1.10733 CPU time (s): 1.05484 CPU user time (s): 1.01384 CPU system time (s): 0.040993 CPU usage (%): 95.2592 Max. virtual memory (cumulated for all children) (Kb): 0
Verifier: OK 2650