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:10:4.5:0.5:100.opb
MD5SUMdd81121db7c1c4b8597dd9571c707a87
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3
Optimality of the best value was proved YES
Number of terms in the objective function 372
Biggest coefficient in the objective function 220
Number of bits for the biggest coefficient in the objective function 8
Sum of the numbers in the objective function 983
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 220
Number of bits of the biggest number in a constraint 8
Biggest sum of numbers in a constraint 983
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 benchmark19.3841
Number of variables372
Total number of constraints792
Number of constraints which are clauses345
Number of constraints which are cardinality constraints (but not clauses)447
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint18

Trace number 2109

Launcher Data

LAUNCH ON wulflinc18 THE 2005-09-18 18:04:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1564 boxname=wulflinc18 idbench=392 idsolver=2 numberseed=0
MD5SUM SOLVER: 1540ae3c74fe6bb56fea7dc39e0baf99  /oldhome/oroussel/solvers/galena
MD5SUM BENCH:  dd81121db7c1c4b8597dd9571c707a87  /oldhome/oroussel/tmp/wulflinc18/normalized-10:10:4.5:0.5:100.opb
REAL COMMAND:  galena /oldhome/oroussel/tmp/wulflinc18/normalized-10:10:4.5:0.5:100.opb
IDLAUNCH: 1564
/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:        916852 kB
Buffers:         35224 kB
Cached:          47708 kB
SwapCached:        844 kB
Active:          66168 kB
Inactive:        19392 kB
HighTotal:      131008 kB
HighFree:        80360 kB
LowTotal:       903652 kB
LowFree:        836492 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            26568 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:23 (client local time) WITH STATUS 10 IN 1.07983 SECONDS
stats: 1564 0 1.07983 10

Solver Data

c Decisions:	5455
c Implications:	22733
c RUNTIME:	1.00085s
v v287 -v229 -v148 -v112 v97 v75 -v45 -v23 v285 -v270 -v233 -v147 -v128 -v113 -v44 -v28 -v269 -v232 v196 -v149 -v127 -v117 -v98 v79 -v46 -v27 -v2 v286 -v271 -v253 -v234 v195 -v166 -v152 -v133 -v115 -v99 v77 -v47 -v7 -v291 -v272 -v252 -v238 v197 -v165 -v151 -v132 -v116 v102 -v54 -v30 -v6 -v343 v273 -v237 v200 -v171 -v156 -v134 v100 -v78 -v48 -v31 -v342 v280 -v254 -v235 v199 -v170 -v155 -v138 v101 -v82 -v49 -v34 -v9 -v344 v274 v256 -v236 -v203 v172 -v153 -v137 -v50 -v32 -v10 -v345 v275 -v201 v173 -v154 -v135 -v33 -v11 -v346 v276 v257 -v202 v174 -v136 -v12 -v305 v288 -v114 v94 v74 -v309 -v228 -v118 v96 -v22 -v292 -v230 v95 v80 -v57 -v24 -v290 -v248 -v231 -v150 -v129 v103 -v58 -v29 -v1 v283 -v247 -v242 -v164 -v130 -v83 -v53 -v26 -v3 v284 v198 -v167 -v160 -v131 -v81 -v35 -v8 v279 v255 -v221 -v211 -v168 -v159 -v142 -v51 -v5 v258 -v207 v169 -v13 -v349 v277 -v259 -v206 v188 v178 -v350 -v260 v192 -v304 v289 -v126 v72 -v56 -v308 v293 -v122 v93 v76 -v55 -v282 -v245 -v161 -v121 v111 v73 v281 -v246 -v163 v107 -v84 -v25 -v360 -v241 v217 -v208 -v145 v106 -v43 -v249 -v210 -v146 -v39 -v4 -v348 -v250 -v239 -v220 v181 -v157 -v141 -v52 -v38 -v21 -v347 v251 v182 -v17 v278 v264 -v204 v187 v177 -v158 -v139 -v16 v191 -v306 v301 -v244 -v125 v108 -v310 v297 -v243 -v162 v110 v71 -v356 v296 -v144 -v119 v92 -v40 -v209 -v143 v88 -v42 -v359 -v312 v216 v180 -v120 -v104 v87 -v64 -v18 -v313 v179 -v20 v267 -v240 -v222 -v105 -v36 v268 -v336 v263 -v205 v189 v175 -v140 -v37 -v14 -v340 v193 -v307 v300 -v123 v109 v89 -v311 v91 -v41 -v355 -v315 v294 -v213 -v60 -v314 -v19 -v361 v295 v266 v218 v85 -v63 v265 -v184 -v223 -v183 v86 v364 -v335 v261 v190 -v176 -v15 -v339 v194 v352 -v303 v298 -v124 v90 -v302 -v357 -v319 -v59 v212 -v362 v328 v214 -v65 v219 v365 v363 -v185 -v337 v262 -v186 -v68 -v341 -v322 v299 v351 -v323 v353 v325 -v318 -v61 -v358 v327 -v316 -v66 v366 -v332 v215 -v331 -v227 v69 -v67 -v338 -v320 v324 v354 -v62 v329 -v317 -v224 v370 -v226 v70 v369 -v333 -v334 -v321 v326 -v225 v330 v367 -v368 v371 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/4654/stat): 4654 (galena) R 4653 4654 31027 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 1843238245 1015808 2 4294967295 134512640 135412752 3221224560 3221224560 134512896 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/4654/statm): 248 2 241 241 0 7 0
[pid=4654] vsize: 992
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-10:10:4.5:0.5:100.opb
One traced child (pid=4654) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1.20611
CPU time (s): 1.07983
CPU user time (s): 1.01085
CPU system time (s): 0.068989
CPU usage (%): 89.5302
Max. virtual memory (cumulated for all children) (Kb): 0

Verifier Data

Verifier:	OK	17