Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:100.opb
MD5SUMf82b685b64af240616b701a750c82883
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers12
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1226.18
Number of variables934
Total number of constraints1996
Number of constraints which are clauses879
Number of constraints which are cardinality constraints (but not clauses)1117
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint20

Trace number 2462

Launcher Data

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

Solver Data

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

Watcher Data

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 Data

Verifier:	OK	406