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/miplib3/normalized-mps-v2-20-10-p0282.opb
MD5SUM1a8deb577df7e72871b7e1004c098336
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.01984
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 42535 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-06-16 10:05:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25756 boxname=wulflinc5 idbench=1056 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1a8deb577df7e72871b7e1004c098336  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-p0282.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-p0282.opb
IDLAUNCH: 25756
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        771024 kB
Buffers:         27780 kB
Cached:         212932 kB
SwapCached:        688 kB
Active:          28604 kB
Inactive:       214216 kB
HighTotal:      131008 kB
HighFree:        41300 kB
LowTotal:       903652 kB
LowFree:        729724 kB
SwapTotal:     2097136 kB
SwapFree:      2095520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5156 kB
Slab:            15128 kB
Committed_AS:    63716 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 10:07:26 (client local time) WITH STATUS 1 IN 110.448 SECONDS
stats: 25756 7 110.448 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...
c got solution with objective value: 746317
c small objective detected

	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.87 0.93 0.90 2/54 12567
Raw data (stat): 12567 (runsolver) R 12566 7266 7265 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 969907485 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.0014 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 12567
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 28448 0 0 0 937 62 0 0 25 0 1 0 969907485 87191552 17488 4294967295 134512640 135730672 3221224576 3221142896 134546366 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 21287 17488 301 301 0 20986 0
vsize: 85148
[startup+20.0021 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 56819 0 0 0 1881 118 0 0 25 0 1 0 969907485 173019136 34647 4294967295 134512640 135730672 3221224576 3221183816 134787727 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 42241 34648 301 301 0 41940 0
vsize: 168964
[startup+30.0022 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 97063 0 0 0 2801 198 0 0 25 0 1 0 969907485 297463808 52705 4294967295 134512640 135730672 3221224576 3221174864 134786435 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 72623 52705 301 301 0 72322 0
vsize: 290492
[startup+40.0023 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 112198 0 0 0 3770 229 0 0 25 0 1 0 969907485 342511616 67621 4294967295 134512640 135730672 3221224576 3221146696 134787727 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 83621 67621 301 301 0 83320 0
vsize: 334484
[startup+50.003 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 134090 0 0 0 4729 270 0 0 25 0 1 0 969907485 517160960 89213 4294967295 134512640 135730672 3221224576 3221190320 134775356 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 126260 89215 301 301 0 125959 0
vsize: 505040
[startup+60.0025 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 192907 0 0 0 5619 381 0 0 25 0 1 0 969907485 595046400 103974 4294967295 134512640 135730672 3221224576 3221160592 134610914 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 145275 103975 301 301 0 144974 0
vsize: 581100
[startup+70.0026 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 203835 0 0 0 6599 401 0 0 25 0 1 0 969907485 628600832 114709 4294967295 134512640 135730672 3221224576 3221181408 134770772 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 153467 114711 301 301 0 153166 0
vsize: 613868
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 220115 0 0 0 7565 435 0 0 25 0 1 0 969907485 643739648 130767 4294967295 134512640 135730672 3221224576 3221159136 134770685 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 157163 130767 301 301 0 156862 0
vsize: 628652
[startup+90.0027 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 239587 0 0 0 8528 472 0 0 25 0 1 0 969907485 671584256 150013 4294967295 134512640 135730672 3221224576 3221192784 134813861 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 163961 150013 301 301 0 163660 0
vsize: 655844
[startup+100.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 255097 0 0 0 9500 500 0 0 25 0 1 0 969907485 743813120 165345 4294967295 134512640 135730672 3221224576 3221176768 134770870 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 181595 165345 301 301 0 181294 0
vsize: 726380
[startup+110.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 264796 0 0 0 10466 534 0 0 25 0 1 0 969907485 397725696 96681 4294967295 134512640 135730672 3221224576 3221222976 134782612 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 97101 96681 301 301 0 96800 0
vsize: 388404
[startup+110.443 s]
Raw data (loadavg): 0.98 0.95 0.91 1/53 12569
Raw data (stat): 12567 (pb2sat-v2) R 12566 7266 7265 0 -1 0 264796 0 0 0 10466 534 0 0 25 0 1 0 969907485 397725696 96681 4294967295 134512640 135730672 3221224576 3221222976 134782612 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 97101 96681 301 301 0 96800 0
vsize: 0

Child status: 1
Real time (s): 110.442
CPU time (s): 110.448
CPU user time (s): 104.895
CPU system time (s): 5.55315
CPU usage (%): 100.005
Max. virtual memory (Kb): 726380
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####