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/miplib3/normalized-mps-v2-13-7-p0548.opb
MD5SUM	10547c6c0f11ab5df74fcaff6ba6d160
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	14938
Optimality of the best value was proved	NO
Number of terms in the objective function	416
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	96797
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	96797
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1244.18
Number of variables	548
Total number of constraints	724
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	550
Number of constraints which are nor clauses,nor cardinality constraints	134
Minimum length of a constraint	1
Maximum length of a constraint	143

Trace number 42922

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-06-16 18:32:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=26141 boxname=wulflinc4 idbench=1441 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-p0548.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-p0548.opb
IDLAUNCH: 26141
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 2
cpu MHz		: 451.169
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:        836088 kB
Buffers:          9812 kB
Cached:         167172 kB
SwapCached:        904 kB
Active:          27048 kB
Inactive:       152040 kB
HighTotal:      131008 kB
HighFree:        45164 kB
LowTotal:       903652 kB
LowFree:        790924 kB
SwapTotal:     2097136 kB
SwapFree:      2095236 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           4996 kB
Slab:            13680 kB
Committed_AS:    71908 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 18:36:33 (client local time) WITH STATUS 1 IN 258.911 SECONDS
stats: 26141 7 258.911 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

c Decision: 12464/174694	Time: 97.2822/86400
c got solution with objective value: 71025
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.84 0.94 0.90 2/54 31278
Raw data (stat): 31278 (runsolver) R 31277 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 972937486 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.0013 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 26542 0 0 0 940 58 0 0 25 0 1 0 972937486 85610496 15206 4294967295 134512640 135730672 3221224576 3221222896 134732476 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 20901 15206 301 301 0 20600 0
vsize: 83604
[startup+20.0021 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 27424 0 0 0 1938 59 0 0 25 0 1 0 972937486 88666112 15696 4294967295 134512640 135730672 3221224576 3221223072 134747568 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 21647 15696 301 301 0 21346 0
vsize: 86588
[startup+30.0032 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 28249 0 0 0 2937 61 0 0 25 0 1 0 972937486 91680768 16309 4294967295 134512640 135730672 3221224576 3221223072 134747967 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 22383 16309 301 301 0 22082 0
vsize: 89532
[startup+40.0038 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 28657 0 0 0 3936 62 0 0 25 0 1 0 972937486 93265920 16602 4294967295 134512640 135730672 3221224576 3221223232 134734759 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 22770 16602 301 301 0 22469 0
vsize: 91080
[startup+50.0037 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 28833 0 0 0 4936 62 0 0 25 0 1 0 972937486 94339072 16778 4294967295 134512640 135730672 3221224576 3221223072 134747568 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 23032 16778 301 301 0 22731 0
vsize: 92128
[startup+60.0041 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 28849 0 0 0 5935 63 0 0 25 0 1 0 972937486 94339072 16794 4294967295 134512640 135730672 3221224576 3221223072 134747543 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 23032 16794 301 301 0 22731 0
vsize: 92128
[startup+70.0044 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 28887 0 0 0 6935 63 0 0 25 0 1 0 972937486 94339072 16832 4294967295 134512640 135730672 3221224576 3221223216 134748259 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 23032 16832 301 301 0 22731 0
vsize: 92128
[startup+80.0053 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 29351 0 0 0 7935 64 0 0 25 0 1 0 972937486 96468992 17165 4294967295 134512640 135730672 3221224576 3221223072 134747651 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 23552 17165 301 301 0 23251 0
vsize: 94208
[startup+90.0054 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 29524 0 0 0 8934 65 0 0 25 0 1 0 972937486 97001472 17305 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 23682 17305 301 301 0 23381 0
vsize: 94728
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 29775 0 0 0 9934 65 0 0 25 0 1 0 972937486 98332672 17523 4294967295 134512640 135730672 3221224576 3221223072 134747751 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 24007 17523 301 301 0 23706 0
vsize: 96028
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 30485 0 0 0 10932 67 0 0 25 0 1 0 972937486 99868672 17825 4294967295 134512640 135730672 3221224576 3221223200 134748158 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24382 17825 301 301 0 24081 0
vsize: 97528
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 30666 0 0 0 11931 68 0 0 25 0 1 0 972937486 100536320 17940 4294967295 134512640 135730672 3221224576 3221222896 134732476 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 24545 17940 301 301 0 24244 0
vsize: 98180
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 30731 0 0 0 12931 68 0 0 25 0 1 0 972937486 100667392 17972 4294967295 134512640 135730672 3221224576 3221223232 134734759 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 24577 17972 301 301 0 24276 0
vsize: 98308
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 30852 0 0 0 13930 69 0 0 25 0 1 0 972937486 101199872 18060 4294967295 134512640 135730672 3221224576 3221223072 134747636 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 24707 18060 301 301 0 24406 0
vsize: 98828
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 31120 0 0 0 14930 69 0 0 25 0 1 0 972937486 102526976 18262 4294967295 134512640 135730672 3221224576 3221223072 134747644 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 25031 18262 301 301 0 24730 0
vsize: 100124
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 45504 0 0 0 15900 99 0 0 25 0 1 0 972937486 185262080 27685 4294967295 134512640 135730672 3221224576 3221133280 134788521 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 45230 27689 301 301 0 44929 0
vsize: 180920
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 67633 0 0 0 16856 143 0 0 25 0 1 0 972937486 192954368 43436 4294967295 134512640 135730672 3221224576 3221123312 134770034 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 47108 43438 301 301 0 46807 0
vsize: 188432
[startup+180.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 103906 0 0 0 17786 214 0 0 25 0 1 0 972937486 336084992 57538 4294967295 134512640 135730672 3221224576 3221136952 134787727 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 82052 57538 301 301 0 81751 0
vsize: 328208
[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 123803 0 0 0 18745 255 0 0 25 0 1 0 972937486 363118592 77196 4294967295 134512640 135730672 3221224576 3221172984 135284287 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 88652 77196 301 301 0 88351 0
vsize: 354608
[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 165662 0 0 0 19664 336 0 0 25 0 1 0 972937486 499855360 100488 4294967295 134512640 135730672 3221224576 3221174600 135284832 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 122035 100488 301 301 0 121734 0
vsize: 488140
[startup+210.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 200644 0 0 0 20588 412 0 0 25 0 1 0 972937486 642465792 110728 4294967295 134512640 135730672 3221224576 3221177104 134784071 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 156852 110728 301 301 0 156551 0
vsize: 627408
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 213566 0 0 0 21564 436 0 0 25 0 1 0 972937486 642465792 123423 4294967295 134512640 135730672 3221224576 3221147160 134787727 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 156852 123423 301 301 0 156551 0
vsize: 627408
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 232506 0 0 0 22526 475 0 0 25 0 1 0 972937486 666255360 142132 4294967295 134512640 135730672 3221224576 3221197184 134770759 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 162660 142133 301 301 0 162359 0
vsize: 650640
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 248603 0 0 0 23492 509 0 0 25 0 1 0 972937486 739430400 158044 4294967295 134512640 135730672 3221224576 3221180016 134770700 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 180525 158045 301 301 0 180224 0
vsize: 722100
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 267432 0 0 0 24454 547 0 0 25 0 1 0 972937486 767107072 176657 4294967295 134512640 135730672 3221224576 3221222704 135284078 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 187282 176657 301 301 0 186981 0
vsize: 749128
[startup+258.915 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 31278
Raw data (stat): 31278 (pb2sat-v2) R 31277 21152 21151 0 -1 0 267432 0 0 0 24454 547 0 0 25 0 1 0 972937486 767107072 176657 4294967295 134512640 135730672 3221224576 3221222704 135284078 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 187282 176657 301 301 0 186981 0
vsize: 0

Child status: 1
Real time (s): 258.914
CPU time (s): 258.911
CPU user time (s): 253.079
CPU system time (s): 5.83211
CPU usage (%): 99.9987
Max. virtual memory (Kb): 749128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####