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-ship04l.opb
MD5SUM	2c68ccb202caa7ec35d2be2cf2e849d9
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	63540
Biggest coefficient in the objective function	1977295568896000
Number of bits for the biggest coefficient in the objective function	51
Sum of the numbers in the objective function	435915316225983825
Number of bits of the sum of numbers in the objective function	59
Biggest number in a constraint	1977295568896000
Number of bits of the biggest number in a constraint	51
Biggest sum of numbers in a constraint	435915316225983825
Number of bits of the biggest sum of numbers	59
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.556914
Number of variables	63540
Total number of constraints	352
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	352
Minimum length of a constraint	30
Maximum length of a constraint	2520

Trace number 35111

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-05-28 12:13:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24406 boxname=wulflinc21 idbench=878 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2c68ccb202caa7ec35d2be2cf2e849d9  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-ship04l.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-ship04l.opb
IDLAUNCH: 24406
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        846560 kB
Buffers:         33996 kB
Cached:         130220 kB
SwapCached:        956 kB
Active:          57456 kB
Inactive:       108980 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        846308 kB
SwapTotal:     2097892 kB
SwapFree:      2096012 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5136 kB
Slab:            15892 kB
Committed_AS:    63912 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 12:17:23 (client local time) WITH STATUS 1 IN 206.878 SECONDS
stats: 24406 7 206.878 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.95 0.90 2/55 13383
Raw data (stat): 13383 (runsolver) R 13382 32363 32362 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 741982328 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+9.99996 s]
Raw data (loadavg): 0.92 0.95 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 2198 0 0 0 994 4 0 0 25 0 1 0 741982328 8089600 1523 4294967295 134512640 135726644 3221224576 3221221664 134556187 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1975 1523 300 300 0 1675 0
vsize: 7900
[startup+20.0002 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 2704 0 0 0 1993 6 0 0 25 0 1 0 741982328 9441280 2021 4294967295 134512640 135726644 3221224576 3221221664 134556168 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2305 2021 300 300 0 2005 0
vsize: 9220
[startup+29.9993 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 3871 0 0 0 2990 9 0 0 25 0 1 0 741982328 13410304 2476 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3274 2476 300 300 0 2974 0
vsize: 13096
[startup+40 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 4109 0 0 0 3990 9 0 0 25 0 1 0 741982328 14086144 2709 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3439 2709 300 300 0 3139 0
vsize: 13756
[startup+50.0007 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 4366 0 0 0 4988 11 0 0 25 0 1 0 741982328 14761984 2962 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3604 2962 300 300 0 3304 0
vsize: 14416
[startup+60.0003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 4598 0 0 0 5987 12 0 0 25 0 1 0 741982328 15302656 3190 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3736 3190 300 300 0 3436 0
vsize: 14944
[startup+70 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 4806 0 0 0 6987 12 0 0 25 0 1 0 741982328 15843328 3395 4294967295 134512640 135726644 3221224576 3221221024 134767118 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3868 3395 300 300 0 3568 0
vsize: 15472
[startup+79.9997 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 5003 0 0 0 7986 13 0 0 25 0 1 0 741982328 16384000 3588 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4000 3588 300 300 0 3700 0
vsize: 16000
[startup+89.9994 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 5186 0 0 0 8986 14 0 0 25 0 1 0 741982328 16924672 3768 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4132 3768 300 300 0 3832 0
vsize: 16528
[startup+99.999 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 5358 0 0 0 9985 15 0 0 25 0 1 0 741982328 17330176 3938 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4231 3938 300 300 0 3931 0
vsize: 16924
[startup+109.999 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 30591 0 0 0 10930 70 0 0 25 0 1 0 741982328 101576704 22564 4294967295 134512640 135726644 3221224576 3197260628 135280585 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 24799 22564 300 300 0 24499 0
vsize: 99196
[startup+119.999 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 62774 0 0 0 11863 137 0 0 25 0 1 0 741982328 194445312 40429 4294967295 134512640 135726644 3221224576 3195798456 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 47472 40429 300 300 0 47172 0
vsize: 189888
[startup+129.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 88533 0 0 0 12814 186 0 0 25 0 1 0 741982328 273444864 56254 4294967295 134512640 135726644 3221224576 3196035664 134767237 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 66759 56254 300 300 0 66459 0
vsize: 267036
[startup+139.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 118720 0 0 0 13751 250 0 0 25 0 1 0 741982328 384704512 73922 4294967295 134512640 135726644 3221224576 3195793280 134783024 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 93922 73923 300 300 0 93622 0
vsize: 375688
[startup+149.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 158649 0 0 0 14678 323 0 0 25 0 1 0 741982328 513945600 94246 4294967295 134512640 135726644 3221224576 3195790080 134782631 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 125475 94247 300 300 0 125175 0
vsize: 501900
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 171817 0 0 0 15653 348 0 0 25 0 1 0 741982328 513945600 107157 4294967295 134512640 135726644 3221224576 3197762152 134784091 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 125475 107157 300 300 0 125175 0
vsize: 501900
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 213130 0 0 0 16559 442 0 0 25 0 1 0 741982328 635830272 123656 4294967295 134512640 135726644 3221224576 3195808880 134782642 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 155232 123656 300 300 0 154932 0
vsize: 620928
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 230606 0 0 0 17520 481 0 0 25 0 1 0 741982328 696434688 140912 4294967295 134512640 135726644 3221224576 3195788848 135284693 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 170028 140912 300 300 0 169728 0
vsize: 680112
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 251960 0 0 0 18477 524 0 0 25 0 1 0 741982328 730673152 161997 4294967295 134512640 135726644 3221224576 3195796380 135287584 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 178387 161997 300 300 0 178087 0
vsize: 713548
[startup+200.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 253698 0 0 0 19474 532 0 0 25 0 1 0 741982328 624177152 140216 4294967295 134512640 135726644 3221224576 3221222932 135341057 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 152387 140216 300 300 0 152087 0
vsize: 609548
[startup+206.855 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 13383
Raw data (stat): 13383 (pb2sat) R 13382 32363 32362 0 -1 0 253698 0 0 0 19474 532 0 0 25 0 1 0 741982328 624177152 140216 4294967295 134512640 135726644 3221224576 3221222932 135341057 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 152387 140216 300 300 0 152087 0
vsize: 0

Child status: 1
Real time (s): 206.855
CPU time (s): 206.878
CPU user time (s): 201.266
CPU system time (s): 5.61115
CPU usage (%): 100.011
Max. virtual memory (Kb): 713548
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####