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

Namesubmitted/manquinho/routing/normalized-s4-4-3-7pb.opb
MD5SUM24909033929a72aa74b2fd8b12f27bce
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 64
Optimality of the best value was proved YES
Number of terms in the objective function 672
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 672
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 3
Number of bits of the biggest number in a constraint 2
Biggest sum of numbers in a constraint 672
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark16.5375
Number of variables672
Total number of constraints2030
Number of constraints which are clauses2006
Number of constraints which are cardinality constraints (but not clauses)24
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint28

Trace number 9696

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-23 15:05:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8449 boxname=wulflinc27 idbench=245 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  24909033929a72aa74b2fd8b12f27bce  /oldhome/oroussel/tmp/wulflinc27/normalized-s4-4-3-7pb.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc27/normalized-s4-4-3-7pb.opb
IDLAUNCH: 8449
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.039
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.039
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        944036 kB
Buffers:         11084 kB
Cached:          62764 kB
SwapCached:          0 kB
Active:          44880 kB
Inactive:        31840 kB
HighTotal:      131008 kB
HighFree:        63840 kB
LowTotal:       903652 kB
LowFree:        880196 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6976 kB
Slab:             8292 kB
Committed_AS:    63652 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-23 15:07:49 (client local time) WITH STATUS 30 IN 140.046 SECONDS
stats: 8449 0 140.046 30

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

c Decision: 621/3082	Time: 0.603908/86400
c Decision: 621/3082	Time: 0.965853/86400
c Decision: 621/3082	Time: 1.39179/86400
c Decision: 622/3082	Time: 1.9787/86400
c Decision: 625/3082	Time: 2.67159/86400
c got solution with objective value: 72
c small objective detected
c CONFLICT during preprocess 

c [startup+5.93898 s]  setting bit 9 to 0
c CONFLICT during preprocess 

c [startup+6.08422 s]  setting bit 8 to 0
c CONFLICT during preprocess 

c [startup+6.22899 s]  setting bit 7 to 0

c [startup+6.6083 s]  setting bit 6 to 0

c Decision: 22853/48987	Time: 3.64944/86400
c Decision: 22853/48987	Time: 8.50571/86400
c Decision: 22857/48987	Time: 12.5541/86400
c Decision: 22858/48987	Time: 20.3419/86400
c Decision: 22874/48987	Time: 26.325/86400
c [startup+43.9994 s]  setting bit 5 to 0

c Decision: 13090/48987	Time: 7.02393/86400
c Decision: 13092/48987	Time: 14.3288/86400
c Decision: 13092/48987	Time: 18.6762/86400
c Decision: 13093/48987	Time: 28.5067/86400
c [startup+101.305 s]  setting bit 4 to 0

c [startup+129.285 s]  setting bit 3 to 0

c got solution with objective value: 66
c [startup+133.122 s]  setting bit 2 to 1

c got solution with objective value: 64
c [startup+140.877 s]  setting bit 1 to 1

c got solution with objective value: 64
c [startup+141.185 s]  setting bit 0 to 1
s OPTIMUM FOUND
v -v1 -v10 v100 v101 -v102 -v103 -v104 -v105 -v106 -v107 -v108 v109 -v11 -v110 -v111 -v112 -v113 -v114 v115 -v116 -v117 -v118 v119 -v12 -v120 -v121 -v122 -v123 -v124 v125 v126 -v127 -v128 -v129 -v13 -v130 -v131 -v132 -v133 v134 -v135 -v136 -v137 -v138 -v139 -v14 v140 -v141 -v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v15 -v150 -v151 -v152 -v153 -v154 -v155 -v156 -v157 v158 -v159 -v16 -v160 -v161 -v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v17 v170 -v171 -v172 -v173 -v174 -v175 -v176 v177 -v178 -v179 -v18 -v180 -v181 -v182 v183 -v184 -v185 -v186 v187 -v188 -v189 -v19 -v190 -v191 v192 -v193 -v194 -v195 v196 -v197 -v198 -v199 -v2 -v20 -v200 -v201 -v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 -v21 v210 -v211 -v212 -v213 v214 -v215 -v216 -v217 -v218 -v219 -v22 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 -v229 v23 v230 -v231 -v232 -v233 v234 -v235 -v236 -v237 v238 -v239 -v24 -v240 -v241 -v242 -v243 -v244 -v245 -v246 -v247 -v248 -v249 -v25 -v250 -v251 -v252 v253 -v254 -v255 -v256 v257 -v258 -v259 -v26 -v260 v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v27 -v270 v271 v272 v273 -v274 -v275 -v276 -v277 -v278 -v279 -v28 -v280 -v281 -v282 -v283 -v284 -v285 -v286 -v287 -v288 -v289 -v29 -v290 -v291 -v292 -v293 -v294 -v295 -v296 -v297 -v298 -v299 -v3 -v30 -v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v308 v309 -v31 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 v319 -v32 v320 v321 -v322 -v323 -v324 -v325 -v326 -v327 v328 -v329 -v33 -v330 -v331 v332 -v333 -v334 -v335 -v336 -v337 -v338 -v339 -v34 -v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 v35 -v350 -v351 -v352 v353 -v354 -v355 -v356 v357 -v358 -v359 -v36 -v360 -v361 v362 v363 -v364 -v365 -v366 -v367 -v368 -v369 -v37 -v370 -v371 -v372 -v373 -v374 -v375 v376 -v377 -v378 -v379 -v38 -v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 -v388 -v389 -v39 -v390 v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v4 -v40 -v400 v401 -v402 -v403 -v404 -v405 -v406 -v407 -v408 -v409 -v41 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v418 -v419 -v42 v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 v428 -v429 -v43 -v430 -v431 v432 -v433 -v434 -v435 v436 -v437 -v438 -v439 -v44 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v45 -v450 -v451 -v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v46 -v460 -v461 -v462 -v463 -v464 -v465 v466 v467 -v468 -v469 -v47 -v470 -v471 -v472 -v473 -v474 v475 -v476 -v477 -v478 v479 -v48 -v480 -v481 -v482 -v483 -v484 v485 v486 -v487 -v488 -v489 -v49 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v5 -v50 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v51 -v510 -v511 -v512 -v513 -v514 v515 -v516 -v517 -v518 -v519 -v52 -v520 -v521 -v522 -v523 -v524 -v525 v526 -v527 -v528 v529 -v53 -v530 -v531 -v532 -v533 -v534 -v535 -v536 -v537 -v538 -v539 -v54 -v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 -v55 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v56 -v560 -v561 -v562 -v563 -v564 -v565 -v566 v567 -v568 -v569 -v57 -v570 -v571 -v572 -v573 -v574 -v575 -v576 -v577 -v578 -v579 -v58 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v59 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v6 -v60 v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 v61 -v610 -v611 v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v62 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 -v63 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 -v64 -v640 -v641 v642 -v643 -v644 -v645 -v646 -v647 -v648 -v649 -v65 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 -v66 v660 -v661 -v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v67 -v670 -v671 -v672 -v68 -v69 -v7 -v70 -v71 -v72 -v73 v74 v75 -v76 -v77 -v78 -v79 v8 -v80 -v81 -v82 -v83 -v84 -v85 -v86 -v87 -v88 -v89 -v9 -v90 -v91 -v92 -v93 -v94 -v95 -v96 -v97 -v98 -v99

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/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 18 0 0 0 0 0 0 0 24 0 1 0 21093970 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 373 2 364 364 0 9 0
[pid=8043] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-s4-4-3-7pb.opb

[startup+10.002 s]
Raw data (loadavg): 0.87 0.97 0.99 2/55 8043
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 8775 0 0 0 939 33 0 0 25 0 1 0 21093970 27340800 5547 4294967295 134512640 135987407 3221224560 3221223136 134814273 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 6675 5547 364 364 0 6311 0
[pid=8043] vsize: 26700
Current children cumulated CPU time (s) 9.72
Current children cumulated vsize (Kb) 26700

[startup+20.0028 s]
Raw data (loadavg): 0.89 0.97 0.99 1/55 8043
Raw data (/proc/8043/stat): 8043 (pb2sat) T 8042 8043 4005 0 -1 0 9320 0 0 0 1923 39 0 0 25 0 1 0 21093970 28360704 5804 4294967295 134512640 135987407 3221224560 3221223244 135541329 0 0 5 16384 3222434794 0 0 17 0 0 0
Raw data (/proc/8043/statm): 6924 5804 364 364 0 6560 0
[pid=8043] vsize: 27696
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 27696

[startup+30.0036 s]
Raw data (loadavg): 0.91 0.97 0.99 2/55 8043
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 9481 0 0 0 2909 43 0 0 25 0 1 0 21093970 28360704 5869 4294967295 134512640 135987407 3221224560 3221222976 134788454 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 6924 5869 364 364 0 6560 0
[pid=8043] vsize: 27696
Current children cumulated CPU time (s) 29.52
Current children cumulated vsize (Kb) 27696

[startup+40.0035 s]
Raw data (loadavg): 0.92 0.97 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 9834 0 0 0 3894 49 0 0 25 0 1 0 21093970 29401088 6126 4294967295 134512640 135987407 3221224560 3221222980 134788428 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 7178 6126 364 364 0 6814 0
[pid=8043] vsize: 28712
Current children cumulated CPU time (s) 39.43
Current children cumulated vsize (Kb) 28712

[startup+50.0033 s]
Raw data (loadavg): 0.93 0.97 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 9996 0 0 0 4881 54 0 0 25 0 1 0 21093970 29401088 6192 4294967295 134512640 135987407 3221224560 3221223104 134811803 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 7178 6192 364 364 0 6814 0
[pid=8043] vsize: 28712
Current children cumulated CPU time (s) 49.35
Current children cumulated vsize (Kb) 28712

[startup+60.0041 s]
Raw data (loadavg): 0.94 0.97 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 10246 0 0 0 5870 58 0 0 25 0 1 0 21093970 29671424 6250 4294967295 134512640 135987407 3221224560 3221223104 134811775 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 7244 6250 364 364 0 6880 0
[pid=8043] vsize: 28976
Current children cumulated CPU time (s) 59.28
Current children cumulated vsize (Kb) 28976

[startup+70.0049 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 10429 0 0 0 6858 62 0 0 25 0 1 0 21093970 34000896 6337 4294967295 134512640 135987407 3221224560 3221223104 134811735 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 8301 6337 364 364 0 7937 0
[pid=8043] vsize: 33204
Current children cumulated CPU time (s) 69.2
Current children cumulated vsize (Kb) 33204

[startup+80.0057 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 10635 0 0 0 7847 67 0 0 25 0 1 0 21093970 34271232 6447 4294967295 134512640 135987407 3221224560 3221223104 134811805 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 8367 6447 364 364 0 8003 0
[pid=8043] vsize: 33468
Current children cumulated CPU time (s) 79.14
Current children cumulated vsize (Kb) 33468

[startup+90.0056 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 10746 0 0 0 8837 70 0 0 25 0 1 0 21093970 34406400 6558 4294967295 134512640 135987407 3221224560 3221223232 134824238 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 8400 6558 364 364 0 8036 0
[pid=8043] vsize: 33600
Current children cumulated CPU time (s) 89.07
Current children cumulated vsize (Kb) 33600

[startup+100.005 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 10850 0 0 0 9827 74 0 0 25 0 1 0 21093970 34406400 6662 4294967295 134512640 135987407 3221224560 3221223104 134812056 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 8400 6662 364 364 0 8036 0
[pid=8043] vsize: 33600
Current children cumulated CPU time (s) 99.01
Current children cumulated vsize (Kb) 33600

[startup+110.006 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 11073 0 0 0 10817 78 0 0 25 0 1 0 21093970 34537472 6756 4294967295 134512640 135987407 3221224560 3221223104 134811775 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 8432 6756 364 364 0 8068 0
[pid=8043] vsize: 33728
Current children cumulated CPU time (s) 108.95
Current children cumulated vsize (Kb) 33728

[startup+120.007 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 11198 0 0 0 11805 83 0 0 25 0 1 0 21093970 34668544 6848 4294967295 134512640 135987407 3221224560 3221223104 134811805 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 8464 6848 364 364 0 8100 0
[pid=8043] vsize: 33856
Current children cumulated CPU time (s) 118.88
Current children cumulated vsize (Kb) 33856

[startup+130.008 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 11388 0 0 0 12797 86 0 0 25 0 1 0 21093970 34668544 6942 4294967295 134512640 135987407 3221224560 3221223104 134811807 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 8464 6942 364 364 0 8100 0
[pid=8043] vsize: 33856
Current children cumulated CPU time (s) 128.83
Current children cumulated vsize (Kb) 33856

[startup+140.008 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 8045
Raw data (/proc/8043/stat): 8043 (pb2sat) R 8042 8043 4005 0 -1 0 11586 0 0 0 13789 89 0 0 25 0 1 0 21093970 34668544 7044 4294967295 134512640 135987407 3221224560 3221223104 134812056 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8043/statm): 8464 7044 364 364 0 8100 0
[pid=8043] vsize: 33856
Current children cumulated CPU time (s) 138.78
Current children cumulated vsize (Kb) 33856
One traced child (pid=8043) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 141.288
CPU time (s): 140.046
CPU user time (s): 139.126
CPU system time (s): 0.91986
CPU usage (%): 99.1204
Max. virtual memory (cumulated for all children) (Kb): 33856

Verifier Data

Verifier:	OK	64