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/MIPLIB/miplib3/normalized-mps-v2-20-10-fast0507.opb
MD5SUM	2854384016ebafb26c8bfb47f81aee87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	324
Optimality of the best value was proved	NO
Number of terms in the objective function	63009
Biggest coefficient in the objective function	2
Number of bits for the biggest coefficient in the objective function	2
Sum of the numbers in the objective function	122425
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	2
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	122425
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	1189.16
Number of variables	63009
Total number of constraints	63516
Number of constraints which are clauses	507
Number of constraints which are cardinality constraints (but not clauses)	63009
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	7753

Trace number 42509

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-06-16 09:32:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25726 boxname=wulflinc3 idbench=1026 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2854384016ebafb26c8bfb47f81aee87  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-fast0507.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-fast0507.opb
IDLAUNCH: 25726
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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.190
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:        698700 kB
Buffers:          8868 kB
Cached:         304676 kB
SwapCached:        820 kB
Active:          43628 kB
Inactive:       272056 kB
HighTotal:      131008 kB
HighFree:          308 kB
LowTotal:       903652 kB
LowFree:        698392 kB
SwapTotal:     2097136 kB
SwapFree:      2095340 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            14600 kB
Committed_AS:    71900 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 09:36:23 (client local time) WITH STATUS 1 IN 248.712 SECONDS
stats: 25726 7 248.712 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: 122425
c big objective detected
c trying from 0 to 511

	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.91 0.94 0.90 2/54 20493
Raw data (stat): 20493 (runsolver) R 20492 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 969698143 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.0015 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 1298 0 0 0 994 4 0 0 25 0 1 0 969698143 5230592 984 4294967295 134512640 135730672 3221224576 3221221748 135159546 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1277 984 301 301 0 976 0
vsize: 5108
[startup+20.0023 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 2424 0 0 0 1991 8 0 0 25 0 1 0 969698143 8634368 1744 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2108 1744 301 301 0 1807 0
vsize: 8432
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 3777 0 0 0 2988 10 0 0 25 0 1 0 969698143 13414400 2384 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3275 2384 301 301 0 2974 0
vsize: 13100
[startup+40.004 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 3923 0 0 0 3988 11 0 0 25 0 1 0 969698143 13549568 2525 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3308 2525 301 301 0 3007 0
vsize: 13232
[startup+50.0048 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 4212 0 0 0 4987 12 0 0 25 0 1 0 969698143 14360576 2809 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3506 2809 301 301 0 3205 0
vsize: 14024
[startup+60.0061 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 4459 0 0 0 5987 12 0 0 25 0 1 0 969698143 14901248 3052 4294967295 134512640 135730672 3221224576 3221221664 134561675 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3638 3052 301 301 0 3337 0
vsize: 14552
[startup+70.0065 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 4681 0 0 0 6986 14 0 0 25 0 1 0 969698143 15577088 3271 4294967295 134512640 135730672 3221224576 3221221520 134539727 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3803 3271 301 301 0 3502 0
vsize: 15212
[startup+80.0074 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 4886 0 0 0 7986 14 0 0 25 0 1 0 969698143 16117760 3472 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3935 3472 301 301 0 3634 0
vsize: 15740
[startup+90.0082 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 5076 0 0 0 8985 15 0 0 25 0 1 0 969698143 16523264 3659 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4034 3659 301 301 0 3733 0
vsize: 16136
[startup+100.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 5255 0 0 0 9985 16 0 0 25 0 1 0 969698143 17063936 3835 4294967295 134512640 135730672 3221224576 3221221664 134561656 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4166 3835 301 301 0 3865 0
vsize: 16664
[startup+110.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 5865 0 0 0 10983 18 0 0 25 0 1 0 969698143 19361792 4443 4294967295 134512640 135730672 3221224576 3221221584 134851006 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4727 4443 301 301 0 4426 0
vsize: 18908
[startup+120.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 6108 0 0 0 11981 20 0 0 25 0 1 0 969698143 20582400 4686 4294967295 134512640 135730672 3221224576 3221221552 134540018 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5025 4686 301 301 0 4724 0
vsize: 20100
[startup+130.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 6261 0 0 0 12980 21 0 0 25 0 1 0 969698143 21643264 4839 4294967295 134512640 135730672 3221224576 3221221552 134539974 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5284 4839 301 301 0 4983 0
vsize: 21136
[startup+140.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 25408 0 0 0 13936 64 0 0 25 0 1 0 969698143 90009600 18620 4294967295 134512640 135730672 3221224576 3210352876 135291222 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 21975 18620 301 301 0 21674 0
vsize: 87900
[startup+150.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 52778 0 0 0 14872 128 0 0 25 0 1 0 969698143 164368384 36556 4294967295 134512640 135730672 3221224576 3195657336 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 40129 36556 301 301 0 39828 0
vsize: 160516
[startup+160.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 87938 0 0 0 15800 202 0 0 25 0 1 0 969698143 282853376 55674 4294967295 134512640 135730672 3221224576 3204349360 134770873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 69056 55674 301 301 0 68755 0
vsize: 276224
[startup+170.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 114023 0 0 0 16738 264 0 0 25 0 1 0 969698143 375119872 69260 4294967295 134512640 135730672 3221224576 3197541652 135281249 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 91582 69260 301 301 0 91281 0
vsize: 366328
[startup+180.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 134059 0 0 0 17693 309 0 0 25 0 1 0 969698143 402964480 89064 4294967295 134512640 135730672 3221224576 3199045000 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 98380 89064 301 301 0 98079 0
vsize: 393520
[startup+190.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 172503 0 0 0 18619 383 0 0 25 0 1 0 969698143 522919936 107923 4294967295 134512640 135730672 3221224576 3196899792 134786302 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 127666 107923 301 301 0 127365 0
vsize: 510664
[startup+200.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 207063 0 0 0 19543 460 0 0 25 0 1 0 969698143 657137664 117731 4294967295 134512640 135730672 3221224576 3201422448 134770772 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 160434 117731 301 301 0 160133 0
vsize: 641736
[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 225184 0 0 0 20500 502 0 0 25 0 1 0 969698143 678223872 135628 4294967295 134512640 135730672 3221224576 3211803608 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 165582 135628 301 301 0 165281 0
vsize: 662328
[startup+220.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 244699 0 0 0 21462 541 0 0 25 0 1 0 969698143 706609152 154916 4294967295 134512640 135730672 3221224576 3209986200 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 172512 154916 301 301 0 172211 0
vsize: 690048
[startup+230.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 260541 0 0 0 22426 576 0 0 25 0 1 0 969698143 779513856 170574 4294967295 134512640 135730672 3221224576 3209587160 135284590 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 190311 170574 301 301 0 190010 0
vsize: 761244
[startup+240.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 272746 0 0 0 23395 605 0 0 25 0 1 0 969698143 796676096 182391 4294967295 134512640 135730672 3221224576 3221222704 135282770 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 194501 182391 301 301 0 194200 0
vsize: 778004
[startup+248.73 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 20493
Raw data (stat): 20493 (pb2sat-v2) R 20492 20224 20223 0 -1 0 272746 0 0 0 23395 605 0 0 25 0 1 0 969698143 796676096 182391 4294967295 134512640 135730672 3221224576 3221222704 135282770 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 194501 182391 301 301 0 194200 0
vsize: 0

Child status: 1
Real time (s): 248.729
CPU time (s): 248.712
CPU user time (s): 242.286
CPU system time (s): 6.42602
CPU usage (%): 99.9931
Max. virtual memory (Kb): 778004
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####