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/miplib2003/normalized-mps-v2-20-10-atlanta-ip.opb
MD5SUM	0a1ff370c051d88127ca8cdb722ca490
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	31296
Biggest coefficient in the objective function	1700000000000
Number of bits for the biggest coefficient in the objective function	41
Sum of the numbers in the objective function	81421012358779
Number of bits of the sum of numbers in the objective function	47
Biggest number in a constraint	1700000000000
Number of bits of the biggest number in a constraint	41
Biggest sum of numbers in a constraint	81421012358779
Number of bits of the biggest sum of numbers	47
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.893863
Number of variables	77286
Total number of constraints	70354
Number of constraints which are clauses	2311
Number of constraints which are cardinality constraints (but not clauses)	47534
Number of constraints which are nor clauses,nor cardinality constraints	20509
Minimum length of a constraint	1
Maximum length of a constraint	2790

Trace number 41107

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-06-09 06:14:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=29176 boxname=wulflinc4 idbench=960 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  0a1ff370c051d88127ca8cdb722ca490  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-atlanta-ip.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-atlanta-ip.opb
IDLAUNCH: 29176
/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:        713224 kB
Buffers:         32812 kB
Cached:         266352 kB
SwapCached:       1192 kB
Active:          48908 kB
Inactive:       252632 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        712972 kB
SwapTotal:     2097136 kB
SwapFree:      2094880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4912 kB
Slab:            14192 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-09 06:18:17 (client local time) WITH STATUS 0 IN 246.447 SECONDS
stats: 29176 7 246.447 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
#### 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.89 0.97 0.92 1/54 10145
Raw data (stat): 10145 (runsolver) R 10144 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 908021011 884736 94 4294967295 134512640 135332820 3221224448 3221219628 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.0004 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 6708 0 0 0 984 13 0 0 25 0 1 0 908021011 40017920 6628 4294967295 134512640 134716908 3221224560 3221222680 1077378037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9770 6628 1111 63 0 9707 0
vsize: 39080
[startup+20.0014 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 14034 0 0 0 1972 26 0 0 25 0 1 0 908021011 69992448 13954 4294967295 134512640 134716908 3221224560 3221222788 1077414408 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17088 13954 1111 63 0 17025 0
vsize: 68352
[startup+30.002 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 21367 0 0 0 2960 38 0 0 25 0 1 0 908021011 100151296 21287 4294967295 134512640 134716908 3221224560 3221222788 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 24451 21287 1111 63 0 24388 0
vsize: 97804
[startup+40.0018 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 28859 0 0 0 3947 51 0 0 25 0 1 0 908021011 130727936 28779 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 31916 28779 1111 63 0 31853 0
vsize: 127664
[startup+50.003 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 36224 0 0 0 4933 65 0 0 25 0 1 0 908021011 160886784 36144 4294967295 134512640 134716908 3221224560 3221222788 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 39279 36144 1111 63 0 39216 0
vsize: 157116
[startup+60.0025 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 44397 0 0 0 5920 79 0 0 25 0 1 0 908021011 194482176 44317 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 47481 44317 1111 63 0 47418 0
vsize: 189924
[startup+70.0034 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 52440 0 0 0 6906 93 0 0 25 0 1 0 908021011 227475456 52360 4294967295 134512640 134716908 3221224560 3221222788 1077414357 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 55536 52365 1111 63 0 55473 0
vsize: 222144
[startup+80.0046 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 60503 0 0 0 7895 104 0 0 25 0 1 0 908021011 260468736 60423 4294967295 134512640 134716908 3221224560 3221222788 1077414382 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 63591 60423 1111 63 0 63528 0
vsize: 254364
[startup+90.0041 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 69019 0 0 0 8880 119 0 0 25 0 1 0 908021011 295260160 68939 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 72085 68939 1111 63 0 72022 0
vsize: 288340
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 77684 0 0 0 9866 133 0 0 25 0 1 0 908021011 330792960 77604 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 80760 77604 1111 63 0 80697 0
vsize: 323040
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 86533 0 0 0 10850 149 0 0 25 0 1 0 908021011 367075328 86453 4294967295 134512640 134716908 3221224560 3221222788 1077414435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 89618 86453 1111 63 0 89555 0
vsize: 358472
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 95890 0 0 0 11835 165 0 0 25 0 1 0 908021011 405299200 95810 4294967295 134512640 134716908 3221224560 3221222788 1077414407 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 98950 95810 1111 63 0 98887 0
vsize: 395800
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 105284 0 0 0 12820 180 0 0 25 0 1 0 908021011 443887616 105204 4294967295 134512640 134716908 3221224560 3221222788 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 108371 105204 1111 63 0 108308 0
vsize: 433484
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 114411 0 0 0 13805 195 0 0 25 0 1 0 908021011 481357824 114331 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 117519 114331 1111 63 0 117456 0
vsize: 470076
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 123721 0 0 0 14790 210 0 0 25 0 1 0 908021011 519430144 123641 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 126814 123641 1111 63 0 126751 0
vsize: 507256
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 133209 0 0 0 15775 225 0 0 25 0 1 0 908021011 558256128 133129 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 136293 133129 1111 63 0 136230 0
vsize: 545172
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 142980 0 0 0 16759 242 0 0 25 0 1 0 908021011 598265856 142900 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 146061 142900 1111 63 0 145998 0
vsize: 584244
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 152771 0 0 0 17743 258 0 0 25 0 1 0 908021011 638427136 152691 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 155866 152691 1111 63 0 155803 0
vsize: 623464
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 162348 0 0 0 18728 274 0 0 25 0 1 0 908021011 677548032 162268 4294967295 134512640 134716908 3221224560 3221222788 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 165417 162268 1111 63 0 165354 0
vsize: 661668
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 171757 0 0 0 19710 291 0 0 25 0 1 0 908021011 716066816 171677 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 174821 171677 1111 63 0 174758 0
vsize: 699284
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 181460 0 0 0 20691 311 0 0 25 0 1 0 908021011 755781632 181380 4294967295 134512640 134716908 3221224560 3221223216 134527944 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 184517 181380 1111 63 0 184454 0
vsize: 738068
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 193233 0 0 0 21666 335 0 0 25 0 1 0 908021011 804339712 193154 4294967295 134512640 134716908 3221224560 3221222600 1077378037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 196372 193154 1111 63 0 196309 0
vsize: 785488
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 219357 0 30 0 22567 390 0 0 24 0 1 0 908021011 911060992 217145 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222427 217145 1111 63 0 222364 0
vsize: 889708
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 225854 0 40 0 23541 406 0 0 25 0 1 0 908021011 937574400 222604 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 228900 222604 1111 63 0 228837 0
vsize: 915600
[startup+247.128 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 10145
Raw data (stat): 10145 (bsolo_lpr_cuts-) R 10144 21152 21151 0 -1 0 225854 0 40 0 23541 406 0 0 25 0 1 0 908021011 937574400 222604 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 228900 222604 1111 63 0 228837 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 247.127
CPU time (s): 246.447
CPU user time (s): 241.921
CPU system time (s): 4.52531
CPU usage (%): 99.7246
Max. virtual memory (Kb): 915600
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####