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.5:100.opb
MD5SUMfeaa96df552ef9989407735877840272
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers12
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1213.45
Number of variables776
Total number of constraints1642
Number of constraints which are clauses701
Number of constraints which are cardinality constraints (but not clauses)941
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint20

Trace number 2114

Launcher Data

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

Solver Data

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

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

Verifier:	OK	277