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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0282.opb
MD5SUMa733e9fa1e4e3ac90baf85249f7c3e9a
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 258411
Optimality of the best value was proved NO
Number of terms in the objective function 282
Biggest coefficient in the objective function 160646
Number of bits for the biggest coefficient in the objective function 18
Sum of the numbers in the objective function 1302615
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 160646
Number of bits of the biggest number in a constraint 18
Biggest sum of numbers in a constraint 1302615
Number of bits of the biggest sum of numbers21
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.02084
Number of variables282
Total number of constraints523
Number of constraints which are clauses177
Number of constraints which are cardinality constraints (but not clauses)282
Number of constraints which are nor clauses,nor cardinality constraints64
Minimum length of a constraint1
Maximum length of a constraint57

Trace number 35552 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-28 13:23:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24846 boxname=wulflinc23 idbench=1318 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a733e9fa1e4e3ac90baf85249f7c3e9a  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0282.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0282.opb
IDLAUNCH: 24846
/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:        714824 kB
Buffers:         31500 kB
Cached:         268156 kB
SwapCached:        700 kB
Active:          32136 kB
Inactive:       269640 kB
HighTotal:      131008 kB
HighFree:          588 kB
LowTotal:       903652 kB
LowFree:        714236 kB
SwapTotal:     2097136 kB
SwapFree:      2095556 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5028 kB
Slab:            12412 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:25:06 (client local time) WITH STATUS 1 IN 106.886 SECONDS
stats: 24846 7 106.886 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.90 0.93 0.90 2/54 10400
Raw data (stat): 10400 (runsolver) R 10399 5562 5561 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 865135703 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0004 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 30398 0 0 0 933 65 0 0 25 0 1 0 865135703 90382336 19253 4294967295 134512640 135726644 3221224576 3221144480 134782560 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 22066 19253 300 300 0 21766 0
vsize: 88264
[startup+20.0005 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 59600 0 0 0 1878 120 0 0 25 0 1 0 865135703 177422336 37233 4294967295 134512640 135726644 3221224576 3221174256 135280580 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 43316 37233 300 300 0 43016 0
vsize: 173264
[startup+30.001 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 99318 0 0 0 2793 204 0 0 25 0 1 0 865135703 332308480 54761 4294967295 134512640 135726644 3221224576 3221185600 134780358 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 81130 54761 300 300 0 80830 0
vsize: 324520
[startup+40.0001 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 116165 0 0 0 3760 238 0 0 25 0 1 0 865135703 348667904 71379 4294967295 134512640 135726644 3221224576 3221175752 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 85124 71380 300 300 0 84824 0
vsize: 340496
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 156278 0 0 0 4682 316 0 0 25 0 1 0 865135703 553324544 110506 4294967295 134512640 135726644 3221224576 3221178160 134771705 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 135089 110509 300 300 0 134789 0
vsize: 540356
[startup+60.0018 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 196102 0 0 0 5598 400 0 0 25 0 1 0 865135703 596471808 106956 4294967295 134512640 135726644 3221224576 3221160064 134767136 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 145623 106957 300 300 0 145323 0
vsize: 582492
[startup+70.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 207656 0 0 0 6576 423 0 0 25 0 1 0 865135703 630026240 118304 4294967295 134512640 135726644 3221224576 3221192864 134767136 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 153815 118304 300 300 0 153515 0
vsize: 615260
[startup+80.0024 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 226396 0 0 0 7536 462 0 0 25 0 1 0 865135703 653139968 136812 4294967295 134512640 135726644 3221224576 3221163640 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 159458 136812 300 300 0 159158 0
vsize: 637832
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 243742 0 0 0 8501 498 0 0 25 0 1 0 865135703 728354816 153957 4294967295 134512640 135726644 3221224576 3221196000 134780450 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 177821 153957 300 300 0 177521 0
vsize: 711284
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 262637 0 0 0 9463 536 0 0 25 0 1 0 865135703 755253248 172634 4294967295 134512640 135726644 3221224576 3221170064 134767123 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 184388 172635 300 300 0 184088 0
vsize: 737552
[startup+106.892 s]
Raw data (loadavg): 0.98 0.95 0.91 1/53 10400
Raw data (stat): 10400 (pb2sat) R 10399 5562 5561 0 -1 0 262637 0 0 0 9463 536 0 0 25 0 1 0 865135703 755253248 172634 4294967295 134512640 135726644 3221224576 3221170064 134767123 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 184388 172635 300 300 0 184088 0
vsize: 0

Child status: 1
Real time (s): 106.892
CPU time (s): 106.886
CPU user time (s): 101.109
CPU system time (s): 5.77712
CPU usage (%): 99.9941
Max. virtual memory (Kb): 737552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####