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/course-ass/normalized-ws97-5.opb
MD5SUM6049145b9f1adfd7114adf044503d587
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers16
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark965.053
Number of variables907
Total number of constraints1309
Number of constraints which are clauses126
Number of constraints which are cardinality constraints (but not clauses)1183
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint134

Trace number 2103

Launcher Data

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

Solver Data

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

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/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 Data

Verifier:	OK	2650