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).
  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

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-nw04.opb
MD5SUM5a18ff1f45b144b201f1f80233dc9b6b
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 30407
Optimality of the best value was proved NO
Number of terms in the objective function 87482
Biggest coefficient in the objective function 5220
Number of bits for the biggest coefficient in the objective function 13
Sum of the numbers in the objective function 120189580
Number of bits of the sum of numbers in the objective function 27
Biggest number in a constraint 5220
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 120189580
Number of bits of the biggest sum of numbers27
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1197.16
Number of variables87482
Total number of constraints87518
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)87518
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint42032

Trace number 35227 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-28 12:26:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24518 boxname=wulflinc23 idbench=990 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 24518
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        750156 kB
Buffers:         32708 kB
Cached:         230772 kB
SwapCached:        700 kB
Active:          64160 kB
Inactive:       201400 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        749876 kB
SwapTotal:     2097136 kB
SwapFree:      2095556 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5028 kB
Slab:            13372 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 12:31:58 (client local time) WITH STATUS 1 IN 308.721 SECONDS
stats: 24518 7 308.721 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified

	Unexpected exception :
	St9bad_alloc
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.94 0.95 0.91 2/54 8856
Raw data (stat): 8856 (runsolver) R 8855 5562 5561 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 864796713 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0156 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 757 0 0 0 998 2 0 0 25 0 1 0 864796713 3592192 627 4294967295 134512640 135726644 3221224576 3221221664 134556179 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 877 627 300 300 0 577 0
vsize: 3508
[startup+20.0363 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 2342 0 0 0 1996 6 0 0 25 0 1 0 864796713 8359936 1663 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2041 1663 300 300 0 1741 0
vsize: 8164
[startup+30.0438 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 3774 0 0 0 2993 10 0 0 25 0 1 0 864796713 13410304 2382 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2382 300 300 0 2974 0
vsize: 13096
[startup+40.0516 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 3906 0 0 0 3994 10 0 0 25 0 1 0 864796713 13545472 2508 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3307 2508 300 300 0 3007 0
vsize: 13228
[startup+50.059 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 4196 0 0 0 4992 12 0 0 25 0 1 0 864796713 14221312 2793 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3472 2793 300 300 0 3172 0
vsize: 13888
[startup+60.0593 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 4451 0 0 0 5991 13 0 0 25 0 1 0 864796713 14897152 3044 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3637 3044 300 300 0 3337 0
vsize: 14548
[startup+70.0595 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 4680 0 0 0 6990 14 0 0 25 0 1 0 864796713 15572992 3270 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3802 3270 300 300 0 3502 0
vsize: 15208
[startup+80.0676 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 4895 0 0 0 7990 14 0 0 25 0 1 0 864796713 16113664 3481 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3934 3481 300 300 0 3634 0
vsize: 15736
[startup+90.0767 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 5088 0 0 0 8991 15 0 0 25 0 1 0 864796713 16654336 3671 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4066 3671 300 300 0 3766 0
vsize: 16264
[startup+100.076 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 5270 0 0 0 9990 16 0 0 25 0 1 0 864796713 17059840 3850 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4165 3850 300 300 0 3865 0
vsize: 16660
[startup+110.082 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 5443 0 0 0 10990 16 0 0 25 0 1 0 864796713 17600512 4020 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4297 4020 300 300 0 3997 0
vsize: 17188
[startup+120.082 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 7473 0 0 0 11986 20 0 0 25 0 1 0 864796713 25403392 4638 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4638 300 300 0 5902 0
vsize: 24808
[startup+130.081 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 7528 0 0 0 12986 21 0 0 25 0 1 0 864796713 25403392 4690 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4690 300 300 0 5902 0
vsize: 24808
[startup+140.082 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 7581 0 0 0 13986 21 0 0 25 0 1 0 864796713 25403392 4741 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4741 300 300 0 5902 0
vsize: 24808
[startup+150.085 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 7644 0 0 0 14987 21 0 0 25 0 1 0 864796713 25403392 4802 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4802 300 300 0 5902 0
vsize: 24808
[startup+160.086 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 7709 0 0 0 15986 21 0 0 25 0 1 0 864796713 25403392 4864 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4864 300 300 0 5902 0
vsize: 24808
[startup+170.087 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 7799 0 0 0 16985 22 0 0 25 0 1 0 864796713 25673728 4952 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6268 4952 300 300 0 5968 0
vsize: 25072
[startup+180.19 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 7933 0 0 0 17995 22 0 0 25 0 1 0 864796713 25944064 5084 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6334 5084 300 300 0 6034 0
vsize: 25336
[startup+190.19 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 8062 0 0 0 18995 23 0 0 25 0 1 0 864796713 26349568 5211 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6433 5211 300 300 0 6133 0
vsize: 25732
[startup+200.19 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 8188 0 0 0 19994 23 0 0 25 0 1 0 864796713 26619904 5335 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6499 5335 300 300 0 6199 0
vsize: 25996
[startup+210.191 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 8312 0 0 0 20994 24 0 0 25 0 1 0 864796713 27025408 5457 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6598 5457 300 300 0 6298 0
vsize: 26392
[startup+220.191 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 42447 0 0 0 21923 95 0 0 25 0 1 0 864796713 146104320 29461 4294967295 134512640 135726644 3221224576 3186771536 134556995 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 35670 29462 300 300 0 35370 0
vsize: 142680
[startup+230.194 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 74595 0 0 0 22856 162 0 0 25 0 1 0 864796713 293556224 51915 4294967295 134512640 135726644 3221224576 3187101960 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 71669 51917 300 300 0 71369 0
vsize: 286676
[startup+240.194 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 95327 0 0 0 23809 210 0 0 25 0 1 0 864796713 292184064 62929 4294967295 134512640 135726644 3221224576 3207297032 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 71334 62930 300 300 0 71034 0
vsize: 285336
[startup+250.194 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 126805 0 0 0 24735 283 0 0 25 0 1 0 864796713 407564288 81863 4294967295 134512640 135726644 3221224576 3196684936 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 99503 81864 300 300 0 99203 0
vsize: 398012
[startup+260.195 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 163356 0 0 0 25662 356 0 0 25 0 1 0 864796713 522801152 98796 4294967295 134512640 135726644 3221224576 3194016464 134767052 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 127637 98796 300 300 0 127337 0
vsize: 510548
[startup+270.194 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 179565 0 0 0 26626 393 0 0 25 0 1 0 864796713 531451904 114709 4294967295 134512640 135726644 3221224576 3197971656 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 129749 114709 300 300 0 129449 0
vsize: 518996
[startup+280.194 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 223209 0 0 0 27528 491 0 0 25 0 1 0 864796713 664690688 133534 4294967295 134512640 135726644 3221224576 3193250664 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 162278 133534 300 300 0 161978 0
vsize: 649112
[startup+290.195 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 241239 0 0 0 28487 533 0 0 25 0 1 0 864796713 726900736 151327 4294967295 134512640 135726644 3221224576 3190001864 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 177466 151327 300 300 0 177166 0
vsize: 709864
[startup+300.194 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 251056 0 0 0 29462 558 0 0 25 0 1 0 864796713 740040704 160680 4294967295 134512640 135726644 3221224576 3221222800 135280475 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 180674 160680 300 300 0 180374 0
vsize: 722696
[startup+308.722 s]
Raw data (loadavg): 1.00 0.98 0.91 1/53 8856
Raw data (stat): 8856 (pb2sat) R 8855 5562 5561 0 -1 0 251056 0 0 0 29462 558 0 0 25 0 1 0 864796713 740040704 160680 4294967295 134512640 135726644 3221224576 3221222800 135280475 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 180674 160680 300 300 0 180374 0
vsize: 0

Child status: 1
Real time (s): 308.721
CPU time (s): 308.721
CPU user time (s): 302.818
CPU system time (s): 5.9031
CPU usage (%): 99.9999
Max. virtual memory (Kb): 722696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####