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-sierra.opb
MD5SUM	4eeca712f5c43ba16697ebe3806a3a23
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	36989
Biggest coefficient in the objective function	40063152947200
Number of bits for the biggest coefficient in the objective function	46
Sum of the numbers in the objective function	712861332680300
Number of bits of the sum of numbers in the objective function	50
Biggest number in a constraint	40063152947200
Number of bits of the biggest number in a constraint	46
Biggest sum of numbers in a constraint	712861332680300
Number of bits of the biggest sum of numbers	50
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.344947
Number of variables	38715
Total number of constraints	3263
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	3263
Minimum length of a constraint	10
Maximum length of a constraint	498

Trace number 28735

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-25 04:00:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11481 boxname=wulflinc24 idbench=884 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  4eeca712f5c43ba16697ebe3806a3a23  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-sierra.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-sierra.opb
IDLAUNCH: 11481
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        810812 kB
Buffers:          7044 kB
Cached:         194120 kB
SwapCached:        524 kB
Active:         120500 kB
Inactive:        83044 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        810560 kB
SwapTotal:     2097892 kB
SwapFree:      2096776 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5656 kB
Slab:            14620 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 04:06:00 (client local time) WITH STATUS 20 IN 325.042 SECONDS
stats: 11481 7 325.042 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c Initial problem consists of 38715 variables and 3781 constraints.
s UNSATISFIABLE
c Exit Code: 20
c Total time: 324.967 s
#### 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
Raw data (loadavg): 0.58 0.74 0.83 2/54 16005
Raw data (stat): 16005 (runsolver) R 16004 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 835830631 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.65 0.75 0.83 2/54 16005
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 1117 0 0 0 993 4 0 0 25 0 1 0 835830631 16936960 1041 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4135 1041 1111 63 0 4072 0
vsize: 16540
[startup+20.0016 s]
Raw data (loadavg): 0.70 0.76 0.83 2/54 16005
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 1596 0 0 0 1993 5 0 0 25 0 1 0 835830631 18960384 1520 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4629 1520 1111 63 0 4566 0
vsize: 18516
[startup+30.0019 s]
Raw data (loadavg): 0.75 0.77 0.83 2/54 16005
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 2066 0 0 0 2991 7 0 0 25 0 1 0 835830631 20832256 1990 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5086 1990 1111 63 0 5023 0
vsize: 20344
[startup+40.002 s]
Raw data (loadavg): 0.78 0.77 0.84 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 2545 0 0 0 3990 8 0 0 25 0 1 0 835830631 22847488 2469 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5578 2469 1111 63 0 5515 0
vsize: 22312
[startup+50.0027 s]
Raw data (loadavg): 0.89 0.80 0.84 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 3005 0 0 0 4989 9 0 0 25 0 1 0 835830631 24727552 2929 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6037 2929 1111 63 0 5974 0
vsize: 24148
[startup+60.0039 s]
Raw data (loadavg): 0.91 0.80 0.84 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 3663 0 0 0 5988 10 0 0 25 0 1 0 835830631 27381760 3587 4294967295 134512640 134714508 3221224576 3221222804 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6685 3587 1111 63 0 6622 0
vsize: 26740
[startup+70.0041 s]
Raw data (loadavg): 0.92 0.81 0.84 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 4204 0 0 0 6987 12 0 0 25 0 1 0 835830631 29650944 4128 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7239 4128 1111 63 0 7176 0
vsize: 28956
[startup+80.0037 s]
Raw data (loadavg): 0.93 0.82 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 4792 0 0 0 7986 13 0 0 25 0 1 0 835830631 32055296 4716 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7826 4716 1111 63 0 7763 0
vsize: 31304
[startup+90.0041 s]
Raw data (loadavg): 0.94 0.82 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 5486 0 0 0 8984 15 0 0 25 0 1 0 835830631 34832384 5410 4294967295 134512640 134714508 3221224576 3221222804 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8504 5410 1111 63 0 8441 0
vsize: 34016
[startup+100.004 s]
Raw data (loadavg): 0.95 0.83 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 6116 0 0 0 9983 16 0 0 25 0 1 0 835830631 37519360 6040 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9160 6040 1111 63 0 9097 0
vsize: 36640
[startup+110.005 s]
Raw data (loadavg): 0.96 0.83 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 6720 0 0 0 10982 18 0 0 25 0 1 0 835830631 39931904 6644 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9749 6644 1111 63 0 9686 0
vsize: 38996
[startup+120.006 s]
Raw data (loadavg): 0.96 0.84 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 7368 0 0 0 11980 20 0 0 25 0 1 0 835830631 42606592 7292 4294967295 134512640 134714508 3221224576 3221222804 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10402 7292 1111 63 0 10339 0
vsize: 41608
[startup+130.005 s]
Raw data (loadavg): 0.97 0.84 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 8062 0 0 0 12978 21 0 0 25 0 1 0 835830631 45416448 7986 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11088 7986 1111 63 0 11025 0
vsize: 44352
[startup+140.005 s]
Raw data (loadavg): 0.97 0.85 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 8679 0 0 0 13978 22 0 0 25 0 1 0 835830631 47992832 8603 4294967295 134512640 134714508 3221224576 3221222804 1077414382 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11717 8603 1111 63 0 11654 0
vsize: 46868
[startup+150.006 s]
Raw data (loadavg): 0.98 0.85 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 9396 0 0 0 14977 23 0 0 25 0 1 0 835830631 50810880 9320 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12405 9320 1111 63 0 12342 0
vsize: 49620
[startup+160.006 s]
Raw data (loadavg): 0.98 0.86 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 10275 0 0 0 15974 26 0 0 25 0 1 0 835830631 54390784 10199 4294967295 134512640 134714508 3221224576 3221222804 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13279 10199 1111 63 0 13216 0
vsize: 53116
[startup+170.006 s]
Raw data (loadavg): 0.98 0.86 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 11100 0 0 0 16972 28 0 0 25 0 1 0 835830631 57884672 11024 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14132 11024 1111 63 0 14069 0
vsize: 56528
[startup+180.006 s]
Raw data (loadavg): 0.98 0.86 0.85 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 12066 0 0 0 17971 30 0 0 25 0 1 0 835830631 61853696 11990 4294967295 134512640 134714508 3221224576 3221222804 1077414432 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15101 11990 1111 63 0 15038 0
vsize: 60404
[startup+190.006 s]
Raw data (loadavg): 0.99 0.87 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 13057 0 0 0 18969 31 0 0 25 0 1 0 835830631 65986560 12981 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16110 12981 1111 63 0 16047 0
vsize: 64440
[startup+200.006 s]
Raw data (loadavg): 0.99 0.87 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 14083 0 0 0 19967 34 0 0 25 0 1 0 835830631 70119424 14007 4294967295 134512640 134714508 3221224576 3221222804 1077414433 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17119 14007 1111 63 0 17056 0
vsize: 68476
[startup+210.006 s]
Raw data (loadavg): 0.99 0.87 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 15119 0 0 0 20964 37 0 0 25 0 1 0 835830631 74403840 15043 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 18165 15043 1111 63 0 18102 0
vsize: 72660
[startup+220.007 s]
Raw data (loadavg): 0.99 0.88 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 16081 0 0 0 21962 39 0 0 25 0 1 0 835830631 78340096 16005 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 19126 16005 1111 63 0 19063 0
vsize: 76504
[startup+230.006 s]
Raw data (loadavg): 0.99 0.88 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 17037 0 0 0 22960 41 0 0 25 0 1 0 835830631 82161664 16961 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 20059 16961 1111 63 0 19996 0
vsize: 80236
[startup+240.007 s]
Raw data (loadavg): 0.99 0.89 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 18084 0 0 0 23958 43 0 0 25 0 1 0 835830631 86519808 18008 4294967295 134512640 134714508 3221224576 3221222804 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21123 18008 1111 63 0 21060 0
vsize: 84492
[startup+250.008 s]
Raw data (loadavg): 0.99 0.89 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 19187 0 0 0 24956 46 0 0 25 0 1 0 835830631 91021312 19111 4294967295 134512640 134714508 3221224576 3221223232 134527928 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 22222 19111 1111 63 0 22159 0
vsize: 88888
[startup+260.007 s]
Raw data (loadavg): 0.99 0.89 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 20345 0 0 0 25953 49 0 0 25 0 1 0 835830631 95666176 20269 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 23356 20269 1111 63 0 23293 0
vsize: 93424
[startup+271.401 s]
Raw data (loadavg): 0.99 0.89 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 21700 0 0 0 27089 51 0 0 25 0 1 0 835830631 101285888 21624 4294967295 134512640 134714508 3221224576 3221222804 1077414433 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 24728 21624 1111 63 0 24665 0
vsize: 98912
[startup+281.4 s]
Raw data (loadavg): 0.99 0.90 0.86 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 23184 0 0 0 28087 54 0 0 25 0 1 0 835830631 107384832 23108 4294967295 134512640 134714508 3221224576 3221223232 134527930 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 26217 23108 1111 63 0 26154 0
vsize: 104868
[startup+291.401 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 24476 0 0 0 29085 57 0 0 25 0 1 0 835830631 112832512 24400 4294967295 134512640 134714508 3221224576 3221222804 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 27547 24400 1111 63 0 27484 0
vsize: 110188
[startup+301.401 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 16007
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 25846 0 0 0 30082 59 0 0 25 0 1 0 835830631 118407168 25770 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 28908 25770 1111 63 0 28845 0
vsize: 115632
[startup+311.401 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 16009
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 27390 0 0 0 31079 62 0 0 25 0 1 0 835830631 124743680 27314 4294967295 134512640 134714508 3221224576 3221221188 1077358243 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30455 27314 1111 63 0 30392 0
vsize: 121820
[startup+321.401 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 16009
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 32428 0 0 0 32064 77 0 0 25 0 1 0 835830631 144740352 32204 4294967295 134512640 134714508 3221224576 3221222860 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 35337 32204 1111 63 0 35274 0
vsize: 141348
[startup+325.022 s]
Raw data (loadavg): 0.99 0.91 0.87 1/53 16009
Raw data (stat): 16005 (bsolo_lpr_cuts) R 16004 4613 4612 0 -1 0 32428 0 0 0 32064 77 0 0 25 0 1 0 835830631 144740352 32204 4294967295 134512640 134714508 3221224576 3221222860 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 35337 32204 1111 63 0 35274 0
vsize: 0

Child status: 20
Real time (s): 325.021
CPU time (s): 325.042
CPU user time (s): 324.091
CPU system time (s): 0.950855
CPU usage (%): 100.006
Max. virtual memory (Kb): 141348
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####