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