PB'05 competition: run trace

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:

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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-agg.opb
MD5SUM	3acb5fc9a1a51b5b0d62841ba7c01d77
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	3930
Biggest coefficient in the objective function	5373004087296
Number of bits for the biggest coefficient in the objective function	43
Sum of the numbers in the objective function	556141355997381
Number of bits of the sum of numbers in the objective function	49
Biggest number in a constraint	22763326668800000
Number of bits of the biggest number in a constraint	55
Biggest sum of numbers in a constraint	46271983665442689
Number of bits of the biggest sum of numbers	56
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.043992
Number of variables	4890
Total number of constraints	441
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	441
Minimum length of a constraint	30
Maximum length of a constraint	540

Trace number 35025

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-05-28 12:01:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24336 boxname=wulflinc18 idbench=808 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3acb5fc9a1a51b5b0d62841ba7c01d77  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-agg.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-agg.opb
IDLAUNCH: 24336
/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:        710552 kB
Buffers:         33080 kB
Cached:         258188 kB
SwapCached:        792 kB
Active:          20508 kB
Inactive:       272876 kB
HighTotal:      131008 kB
HighFree:        76692 kB
LowTotal:       903652 kB
LowFree:        633860 kB
SwapTotal:     2097892 kB
SwapFree:      2096240 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5120 kB
Slab:            25160 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 12:02:46 (client local time) WITH STATUS 1 IN 105.896 SECONDS
stats: 24336 7 105.896 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 1/54 1216
Raw data (stat): 1216 (runsolver) R 1215 24172 24171 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 864624791 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.0013 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1216
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 29017 0 0 0 934 65 0 0 25 0 1 0 864624791 90472448 17885 4294967295 134512640 135726644 3221224592 3219634968 134784091 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 22088 17885 300 300 0 21788 0
vsize: 88352
[startup+20.0023 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1216
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 57812 0 0 0 1874 126 0 0 25 0 1 0 864624791 177381376 35460 4294967295 134512640 135726644 3221224592 3219638108 134604449 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 43306 35460 300 300 0 43006 0
vsize: 173224
[startup+30.0021 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 97835 0 0 0 2794 205 0 0 25 0 1 0 864624791 299253760 53280 4294967295 134512640 135726644 3221224592 3219692496 134782652 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 73060 53280 300 300 0 72760 0
vsize: 292240
[startup+40.0021 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 115034 0 0 0 3758 241 0 0 25 0 1 0 864624791 351055872 70246 4294967295 134512640 135726644 3221224592 3219668648 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 85707 70246 300 300 0 85407 0
vsize: 342828
[startup+50.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 158815 0 0 0 4680 319 0 0 25 0 1 0 864624791 560320512 112876 4294967295 134512640 135726644 3221224592 3219691296 135287437 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 136797 112876 300 300 0 136497 0
vsize: 547188
[startup+60.0039 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 194220 0 0 0 5605 395 0 0 25 0 1 0 864624791 595763200 105062 4294967295 134512640 135726644 3221224592 3219657396 134608951 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 145450 105062 300 300 0 145150 0
vsize: 581800
[startup+70.0048 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 205845 0 0 0 6580 420 0 0 25 0 1 0 864624791 629317632 116476 4294967295 134512640 135726644 3221224592 3219715212 135297954 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 153642 116476 300 300 0 153342 0
vsize: 614568
[startup+80.0047 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 226890 0 0 0 7537 463 0 0 25 0 1 0 864624791 660590592 137268 4294967295 134512640 135726644 3221224592 3219704908 134604415 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 161277 137268 300 300 0 160977 0
vsize: 645108
[startup+90.0046 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 247113 0 0 0 8496 505 0 0 25 0 1 0 864624791 690192384 157259 4294967295 134512640 135726644 3221224592 3219692544 134554704 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 168504 157259 300 300 0 168204 0
vsize: 674016
[startup+100.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 262739 0 0 0 9468 533 0 0 25 0 1 0 864624791 764145664 172706 4294967295 134512640 135726644 3221224592 3219679424 135104046 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 186559 172706 300 300 0 186259 0
vsize: 746236
[startup+105.885 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 1218
Raw data (stat): 1216 (pb2sat) R 1215 24172 24171 0 -1 0 262739 0 0 0 9468 533 0 0 25 0 1 0 864624791 764145664 172706 4294967295 134512640 135726644 3221224592 3219679424 135104046 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 186559 172706 300 300 0 186259 0
vsize: 0

Child status: 1
Real time (s): 105.884
CPU time (s): 105.896
CPU user time (s): 100.213
CPU system time (s): 5.68314
CPU usage (%): 100.011
Max. virtual memory (Kb): 746236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####