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 26681

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-24 16:56:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11482 boxname=wulflinc7 idbench=884 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  4eeca712f5c43ba16697ebe3806a3a23  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-sierra.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-sierra.opb
IDLAUNCH: 11482
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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.050
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:        866384 kB
Buffers:         34704 kB
Cached:         112008 kB
SwapCached:        100 kB
Active:          66808 kB
Inactive:        82668 kB
HighTotal:      131008 kB
HighFree:        14784 kB
LowTotal:       903652 kB
LowFree:        851600 kB
SwapTotal:     2097136 kB
SwapFree:      2096820 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6740 kB
Slab:            13008 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-24 17:02:07 (client local time) WITH STATUS 20 IN 316.894 SECONDS
stats: 11482 7 316.894 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Initial problem consists of 38715 variables and 3781 constraints.
s UNSATISFIABLE
c Exit Code: 20
c Total time: 316.821 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.80 0.92 0.92 2/54 26541
Raw data (stat): 26541 (runsolver) R 26540 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 773636671 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 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.0004 s]
Raw data (loadavg): 0.83 0.93 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 947 0 0 0 996 2 0 0 25 0 1 0 773636671 16785408 925 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 4098 925 1111 63 0 4035 0
vsize: 16392
[startup+20.0006 s]
Raw data (loadavg): 0.86 0.93 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 1399 0 0 0 1996 2 0 0 25 0 1 0 773636671 18665472 1377 4294967295 134512640 134714540 3221224592 3221222820 1077414401 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 4557 1377 1111 63 0 4494 0
vsize: 18228
[startup+30.0003 s]
Raw data (loadavg): 0.88 0.93 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 1854 0 0 0 2995 3 0 0 25 0 1 0 773636671 20537344 1832 4294967295 134512640 134714540 3221224592 3221222820 1077414408 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5014 1832 1111 63 0 4951 0
vsize: 20056
[startup+40.0013 s]
Raw data (loadavg): 0.90 0.93 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 2311 0 0 0 3995 4 0 0 25 0 1 0 773636671 22401024 2289 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5469 2289 1111 63 0 5406 0
vsize: 21876
[startup+50.0019 s]
Raw data (loadavg): 0.91 0.93 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 2748 0 0 0 4994 5 0 0 25 0 1 0 773636671 24137728 2726 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5893 2726 1111 63 0 5830 0
vsize: 23572
[startup+60.0026 s]
Raw data (loadavg): 0.93 0.94 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 3331 0 0 0 5993 6 0 0 25 0 1 0 773636671 26546176 3309 4294967295 134512640 134714540 3221224592 3221222840 1077360322 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 6481 3309 1111 63 0 6418 0
vsize: 25924
[startup+70.0022 s]
Raw data (loadavg): 0.94 0.94 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 3896 0 0 0 6992 7 0 0 25 0 1 0 773636671 28934144 3874 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7064 3874 1111 63 0 7001 0
vsize: 28256
[startup+80.0028 s]
Raw data (loadavg): 0.95 0.94 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 4437 0 0 0 7992 8 0 0 25 0 1 0 773636671 31059968 4415 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7583 4415 1111 63 0 7520 0
vsize: 30332
[startup+90.0024 s]
Raw data (loadavg): 0.95 0.94 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 5077 0 0 0 8991 9 0 0 25 0 1 0 773636671 33705984 5055 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8229 5055 1111 63 0 8166 0
vsize: 32916
[startup+100.002 s]
Raw data (loadavg): 0.96 0.94 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 5644 0 0 0 9990 10 0 0 25 0 1 0 773636671 35966976 5622 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8781 5622 1111 63 0 8718 0
vsize: 35124
[startup+110.003 s]
Raw data (loadavg): 0.97 0.94 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 6291 0 0 0 10988 12 0 0 25 0 1 0 773636671 38776832 6269 4294967295 134512640 134714540 3221224592 3221222820 1077414432 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9467 6269 1111 63 0 9404 0
vsize: 37868
[startup+120.003 s]
Raw data (loadavg): 0.97 0.94 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 6881 0 0 0 11987 13 0 0 25 0 1 0 773636671 41193472 6859 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10057 6859 1111 63 0 9994 0
vsize: 40228
[startup+130.004 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 7623 0 0 0 12987 14 0 0 25 0 1 0 773636671 44113920 7601 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10770 7601 1111 63 0 10707 0
vsize: 43080
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 8268 0 0 0 13985 16 0 0 25 0 1 0 773636671 46833664 8246 4294967295 134512640 134714540 3221224592 3221222820 1077414370 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11434 8246 1111 63 0 11371 0
vsize: 45736
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 8983 0 0 0 14984 18 0 0 25 0 1 0 773636671 49672192 8961 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12127 8961 1111 63 0 12064 0
vsize: 48508
[startup+160.004 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 9927 0 0 0 15982 19 0 0 25 0 1 0 773636671 53555200 9905 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 13075 9905 1111 63 0 13012 0
vsize: 52300
[startup+170.004 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 10858 0 0 0 16981 21 0 0 25 0 1 0 773636671 57327616 10836 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 13996 10836 1111 63 0 13933 0
vsize: 55984
[startup+180.004 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 11952 0 0 0 17979 23 0 0 25 0 1 0 773636671 62009344 11930 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15139 11930 1111 63 0 15076 0
vsize: 60556
[startup+190.005 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 26541
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 13057 0 0 0 18977 25 0 0 25 0 1 0 773636671 66551808 13035 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 16248 13035 1111 63 0 16185 0
vsize: 64992
[startup+200.004 s]
Raw data (loadavg): 1.07 0.97 0.93 2/54 26594
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 14184 0 0 0 19962 40 0 0 25 0 1 0 773636671 71098368 14162 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17358 14162 1111 63 0 17295 0
vsize: 69432
[startup+210.005 s]
Raw data (loadavg): 1.06 0.97 0.93 2/54 26594
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 15268 0 0 0 20960 42 0 0 25 0 1 0 773636671 75554816 15246 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18446 15246 1111 63 0 18383 0
vsize: 73784
[startup+220.006 s]
Raw data (loadavg): 1.05 0.97 0.93 2/54 26594
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 16329 0 0 0 21959 43 0 0 25 0 1 0 773636671 79917056 16307 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19511 16307 1111 63 0 19448 0
vsize: 78044
[startup+230.006 s]
Raw data (loadavg): 1.04 0.97 0.93 2/54 26594
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 17410 0 0 0 22957 45 0 0 25 0 1 0 773636671 84275200 17388 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20575 17388 1111 63 0 20512 0
vsize: 82300
[startup+240.007 s]
Raw data (loadavg): 1.03 0.97 0.93 2/54 26594
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 18541 0 0 0 23955 47 0 0 25 0 1 0 773636671 88924160 18519 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21710 18519 1111 63 0 21647 0
vsize: 86840
[startup+250.006 s]
Raw data (loadavg): 1.03 0.97 0.93 2/54 26594
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 19732 0 0 0 24953 49 0 0 25 0 1 0 773636671 93708288 19710 4294967295 134512640 134714540 3221224592 3221222820 1077414345 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 22878 19710 1111 63 0 22815 0
vsize: 91512
[startup+260.007 s]
Raw data (loadavg): 1.02 0.97 0.93 2/54 26594
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 20932 0 0 0 25952 51 0 0 25 0 1 0 773636671 98631680 20910 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 24080 20910 1111 63 0 24017 0
vsize: 96320
[startup+270.007 s]
Raw data (loadavg): 1.02 0.97 0.93 2/54 26594
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 22315 0 0 0 26949 54 0 0 25 0 1 0 773636671 104341504 22293 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 25474 22293 1111 63 0 25411 0
vsize: 101896
[startup+280.007 s]
Raw data (loadavg): 1.02 0.97 0.93 2/54 26596
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 23716 0 0 0 27948 56 0 0 25 0 1 0 773636671 110329856 23694 4294967295 134512640 134714540 3221224592 3221223248 134527928 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 26936 23694 1111 63 0 26873 0
vsize: 107744
[startup+290.008 s]
Raw data (loadavg): 1.01 0.97 0.93 2/54 26596
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 25064 0 0 0 28946 58 0 0 25 0 1 0 773636671 115798016 25042 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 28271 25042 1111 63 0 28208 0
vsize: 113084
[startup+300.008 s]
Raw data (loadavg): 1.01 0.97 0.93 2/54 26596
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 26675 0 0 0 29943 60 0 0 25 0 1 0 773636671 122413056 26653 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 29886 26653 1111 63 0 29823 0
vsize: 119544
[startup+310.008 s]
Raw data (loadavg): 1.01 0.97 0.93 2/54 26596
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 31061 0 0 0 30933 71 0 0 25 0 1 0 773636671 139698176 30891 4294967295 134512640 134714540 3221224592 3221222640 1077314133 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 34106 30891 1111 63 0 34043 0
vsize: 136424
[startup+316.86 s]
Raw data (loadavg): 1.01 0.97 0.93 1/53 26596
Raw data (stat): 26541 (bsolo_mis) R 26540 24300 24299 0 -1 0 31061 0 0 0 30933 71 0 0 25 0 1 0 773636671 139698176 30891 4294967295 134512640 134714540 3221224592 3221222640 1077314133 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 34106 30891 1111 63 0 34043 0
vsize: 0

Child status: 20
Real time (s): 316.86
CPU time (s): 316.894
CPU user time (s): 315.992
CPU system time (s): 0.901862
CPU usage (%): 100.011
Max. virtual memory (Kb): 136424
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####