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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-stp3d.opb
MD5SUM	bd41ba4f2ddbc80664ba643e2dc93b96
Bench Category	optimization, medium integers (OPTMEDINT)
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	75648
Biggest coefficient in the objective function	100303
Number of bits for the biggest coefficient in the objective function	17
Sum of the numbers in the objective function	7576279200
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	100303
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	7576279200
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	2.75158
Number of variables	204880
Total number of constraints	364368
Number of constraints which are clauses	129232
Number of constraints which are cardinality constraints (but not clauses)	210685
Number of constraints which are nor clauses,nor cardinality constraints	24451
Minimum length of a constraint	1
Maximum length of a constraint	120

Trace number 35616

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-05-28 13:30:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24916 boxname=wulflinc20 idbench=1388 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bd41ba4f2ddbc80664ba643e2dc93b96  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-stp3d.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-stp3d.opb
IDLAUNCH: 24916
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        665968 kB
Buffers:         32788 kB
Cached:         311872 kB
SwapCached:        644 kB
Active:          48308 kB
Inactive:       298396 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        665716 kB
SwapTotal:     2097892 kB
SwapFree:      2096312 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            16356 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 13:35:09 (client local time) WITH STATUS 1 IN 264.983 SECONDS
stats: 24916 7 264.983 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): 1.09 0.97 0.92 2/54 12775
Raw data (stat): 12775 (runsolver) R 12774 25399 25398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 865177544 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.0005 s]
Raw data (loadavg): 1.15 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 134 0 0 0 997 2 0 0 25 0 1 0 865177544 1540096 124 4294967295 134512640 135726644 3221224576 3221221776 134574514 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 376 124 300 300 0 76 0
vsize: 1504
[startup+20.0016 s]
Raw data (loadavg): 1.12 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 134 0 0 0 1994 5 0 0 25 0 1 0 865177544 1540096 124 4294967295 134512640 135726644 3221224576 3221221776 134574451 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 376 124 300 300 0 76 0
vsize: 1504
[startup+30.0019 s]
Raw data (loadavg): 1.10 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 2172 0 0 0 2989 10 0 0 25 0 1 0 865177544 7954432 1496 4294967295 134512640 135726644 3221224576 3221221024 134767064 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1942 1496 300 300 0 1642 0
vsize: 7768
[startup+40.0027 s]
Raw data (loadavg): 1.09 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 2720 0 0 0 3987 12 0 0 25 0 1 0 865177544 9441280 2035 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2305 2035 300 300 0 2005 0
vsize: 9220
[startup+50.0057 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 3876 0 0 0 4984 14 0 0 25 0 1 0 865177544 13410304 2479 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3274 2479 300 300 0 2974 0
vsize: 13096
[startup+60.0062 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 4125 0 0 0 5983 15 0 0 25 0 1 0 865177544 14086144 2724 4294967295 134512640 135726644 3221224576 3221221520 134541148 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3439 2724 300 300 0 3139 0
vsize: 13756
[startup+70.0062 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 4387 0 0 0 6983 15 0 0 25 0 1 0 865177544 14761984 2981 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3604 2981 300 300 0 3304 0
vsize: 14416
[startup+80.0069 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 4618 0 0 0 7983 16 0 0 25 0 1 0 865177544 15302656 3209 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3736 3209 300 300 0 3436 0
vsize: 14944
[startup+90.0074 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 4830 0 0 0 8982 16 0 0 25 0 1 0 865177544 15978496 3417 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3901 3417 300 300 0 3601 0
vsize: 15604
[startup+100.007 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 5026 0 0 0 9981 17 0 0 25 0 1 0 865177544 16384000 3610 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4000 3610 300 300 0 3700 0
vsize: 16000
[startup+110.008 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 5211 0 0 0 10981 17 0 0 25 0 1 0 865177544 16924672 3792 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4132 3792 300 300 0 3832 0
vsize: 16528
[startup+120.009 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 5388 0 0 0 11981 18 0 0 25 0 1 0 865177544 17330176 3966 4294967295 134512640 135726644 3221224576 3221221664 134556179 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4231 3966 300 300 0 3931 0
vsize: 16924
[startup+130.01 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 7454 0 0 0 12976 23 0 0 25 0 1 0 865177544 25403392 4620 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4620 300 300 0 5902 0
vsize: 24808
[startup+140.01 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 7510 0 0 0 13976 23 0 0 25 0 1 0 865177544 25403392 4673 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4673 300 300 0 5902 0
vsize: 24808
[startup+150.011 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 7563 0 0 0 14976 23 0 0 25 0 1 0 865177544 25403392 4724 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4724 300 300 0 5902 0
vsize: 24808
[startup+160.012 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 7615 0 0 0 15975 24 0 0 25 0 1 0 865177544 25403392 4773 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4773 300 300 0 5902 0
vsize: 24808
[startup+170.013 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 8214 0 0 0 16974 25 0 0 25 0 1 0 865177544 27566080 5370 4294967295 134512640 135726644 3221224576 3221221148 134604446 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6730 5370 300 300 0 6430 0
vsize: 26920
[startup+180.012 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 46278 0 0 0 17885 114 0 0 25 0 1 0 865177544 159801344 30195 4294967295 134512640 135726644 3221224576 3211329600 134780450 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 39014 30195 300 300 0 38714 0
vsize: 156056
[startup+190.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 81765 0 0 0 18809 190 0 0 25 0 1 0 865177544 278962176 49586 4294967295 134512640 135726644 3221224576 3201658400 134780450 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 68106 49586 300 300 0 67806 0
vsize: 272424
[startup+200.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 108431 0 0 0 19745 254 0 0 25 0 1 0 865177544 395173888 75973 4294967295 134512640 135726644 3221224576 3196475792 134784885 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 96478 75977 300 300 0 96178 0
vsize: 385912
[startup+210.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 140613 0 0 0 20679 321 0 0 25 0 1 0 865177544 569122816 95216 4294967295 134512640 135726644 3221224576 3192549360 134771796 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 138946 95218 300 300 0 138646 0
vsize: 555784
[startup+220.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 166658 0 0 0 21627 373 0 0 25 0 1 0 865177544 521744384 102037 4294967295 134512640 135726644 3221224576 3204108152 135281813 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 127379 102037 300 300 0 127079 0
vsize: 509516
[startup+230.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 205150 0 0 0 22541 458 0 0 25 0 1 0 865177544 731590656 140283 4294967295 134512640 135726644 3221224576 3208786192 134784996 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 178611 140283 300 300 0 178311 0
vsize: 714444
[startup+240.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 226550 0 0 0 23486 514 0 0 25 0 1 0 865177544 698675200 136823 4294967295 134512640 135726644 3221224576 3203315600 134780344 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 170575 136823 300 300 0 170275 0
vsize: 682300
[startup+250.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 245546 0 0 0 24443 557 0 0 25 0 1 0 865177544 730169344 155584 4294967295 134512640 135726644 3221224576 3209561432 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 178264 155584 300 300 0 177964 0
vsize: 713056
[startup+260.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 251868 0 0 0 25420 580 0 0 25 0 1 0 865177544 430891008 104757 4294967295 134512640 135726644 3221224576 3221222764 135277555 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 105198 104757 300 300 0 104898 0
vsize: 420792
[startup+264.992 s]
Raw data (loadavg): 1.00 0.99 0.93 1/53 12775
Raw data (stat): 12775 (pb2sat) R 12774 25399 25398 0 -1 0 251868 0 0 0 25420 580 0 0 25 0 1 0 865177544 430891008 104757 4294967295 134512640 135726644 3221224576 3221222764 135277555 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 105198 104757 300 300 0 104898 0
vsize: 0

Child status: 1
Real time (s): 264.991
CPU time (s): 264.983
CPU user time (s): 258.963
CPU system time (s): 6.02008
CPU usage (%): 99.9967
Max. virtual memory (Kb): 714444
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####