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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-dano3_5.opb
MD5SUM	eaead9cf67652e4b2ad71612149d4439
Bench Category	optimization, medium integers (OPTMEDINT)
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	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	131072000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	576307709
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	303.797
Number of variables	269983
Total number of constraints	3778
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	120
Number of constraints which are nor clauses,nor cardinality constraints	3658
Minimum length of a constraint	1
Maximum length of a constraint	10600

Trace number 17505

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 10:35:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19467 boxname=wulflinc20 idbench=1498 idsolver=6 numberseed=0
MD5SUM SOLVER: 2225cba0d9b2c30e235f6cafc823d7ac  /oldhome/oroussel/solvers/PBS4
MD5SUM BENCH:  eaead9cf67652e4b2ad71612149d4439  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-dano3_5.opb
REAL COMMAND:  PBS4 /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-dano3_5.opb
IDLAUNCH: 19467
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        350992 kB
Buffers:         25712 kB
Cached:         633372 kB
SwapCached:        516 kB
Active:         171176 kB
Inactive:       489840 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        350740 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            17028 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 10:41:03 (client local time) WITH STATUS 20 IN 303.797 SECONDS
stats: 19467 7 303.797 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c PBS v4 by Bashar Al-Rawi & Fadi Aloul
c Solving /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-dano3_5.opb ......
s UNSATISFIABLE
c Done, CPU Time=269.549
#### 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.82 0.94 0.92 1/54 6323
Raw data (stat): 6323 (runsolver) D 6322 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 544405609 1052672 99 4294967295 134512640 135381576 3221224528 3221219776 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.84 0.94 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 12276 0 0 0 961 32 0 0 25 0 1 0 544405609 50475008 11788 4294967295 134512640 135450300 3221224624 3221157424 134600237 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12323 11788 231 231 0 12092 0
vsize: 49292
[startup+20.0011 s]
Raw data (loadavg): 0.87 0.94 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 15353 0 0 0 1951 42 0 0 25 0 1 0 544405609 62885888 14865 4294967295 134512640 135450300 3221224624 3221157424 134599748 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15353 14865 231 231 0 15122 0
vsize: 61412
[startup+30.0011 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 19519 0 0 0 2938 54 0 0 25 0 1 0 544405609 79876096 19031 4294967295 134512640 135450300 3221224624 3221157424 134598676 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 19501 19031 231 231 0 19270 0
vsize: 78004
[startup+40.0019 s]
Raw data (loadavg): 0.90 0.94 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29754 0 0 0 3917 76 0 0 25 0 1 0 544405609 119877632 22383 4294967295 134512640 135450300 3221224624 3221223232 134537648 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29267 22383 231 231 0 29036 0
vsize: 117068
[startup+50.0013 s]
Raw data (loadavg): 0.92 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29797 0 0 0 4917 76 0 0 25 0 1 0 544405609 119877632 22426 4294967295 134512640 135450300 3221224624 3221223360 134538032 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29267 22426 231 231 0 29036 0
vsize: 117068
[startup+60.008 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29835 0 0 0 5917 77 0 0 25 0 1 0 544405609 119877632 22464 4294967295 134512640 135450300 3221224624 3221223360 134538010 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29267 22464 231 231 0 29036 0
vsize: 117068
[startup+70.0082 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29879 0 0 0 6916 78 0 0 25 0 1 0 544405609 121991168 22508 4294967295 134512640 135450300 3221224624 3221223360 134537968 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 29783 22508 231 231 0 29552 0
vsize: 119132
[startup+80.0086 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29924 0 0 0 7914 79 0 0 25 0 1 0 544405609 121991168 22553 4294967295 134512640 135450300 3221224624 3221223360 134538010 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 29783 22553 231 231 0 29552 0
vsize: 119132
[startup+90.0085 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29944 0 0 0 8913 79 0 0 25 0 1 0 544405609 121991168 22573 4294967295 134512640 135450300 3221224624 3221222976 134533236 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29783 22573 231 231 0 29552 0
vsize: 119132
[startup+100.008 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29945 0 0 0 9913 80 0 0 25 0 1 0 544405609 121991168 22574 4294967295 134512640 135450300 3221224624 3221223360 134537979 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29783 22574 231 231 0 29552 0
vsize: 119132
[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29956 0 0 0 10913 81 0 0 25 0 1 0 544405609 122126336 22585 4294967295 134512640 135450300 3221224624 3221223232 134537636 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29816 22585 231 231 0 29585 0
vsize: 119264
[startup+120.009 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 29982 0 0 0 11912 81 0 0 25 0 1 0 544405609 122126336 22611 4294967295 134512640 135450300 3221224624 3221223360 134538010 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29816 22611 231 231 0 29585 0
vsize: 119264
[startup+130.009 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30013 0 0 0 12912 82 0 0 25 0 1 0 544405609 122261504 22642 4294967295 134512640 135450300 3221224624 3221223500 135126769 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29849 22642 231 231 0 29618 0
vsize: 119396
[startup+140.009 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30052 0 0 0 13911 82 0 0 25 0 1 0 544405609 122396672 22681 4294967295 134512640 135450300 3221224624 3221222976 134533236 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29882 22681 231 231 0 29651 0
vsize: 119528
[startup+150.009 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30113 0 0 0 14911 83 0 0 25 0 1 0 544405609 122499072 22742 4294967295 134512640 135450300 3221224624 3221223232 134537613 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29907 22742 231 231 0 29676 0
vsize: 119628
[startup+160.01 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30155 0 0 0 15911 83 0 0 25 0 1 0 544405609 122634240 22784 4294967295 134512640 135450300 3221224624 3221223360 134538010 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29940 22784 231 231 0 29709 0
vsize: 119760
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30203 0 0 0 16911 84 0 0 25 0 1 0 544405609 122896384 22832 4294967295 134512640 135450300 3221224624 3221223500 135126769 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30004 22832 231 231 0 29773 0
vsize: 120016
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30251 0 0 0 17911 84 0 0 25 0 1 0 544405609 122896384 22880 4294967295 134512640 135450300 3221224624 3221223360 134538010 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30004 22880 231 231 0 29773 0
vsize: 120016
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30292 0 0 0 18911 84 0 0 25 0 1 0 544405609 123559936 22921 4294967295 134512640 135450300 3221224624 3221223232 134537609 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30166 22921 231 231 0 29935 0
vsize: 120664
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30327 0 0 0 19911 84 0 0 25 0 1 0 544405609 123559936 22956 4294967295 134512640 135450300 3221224624 3221223232 134537659 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30166 22956 231 231 0 29935 0
vsize: 120664
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30357 0 0 0 20911 84 0 0 25 0 1 0 544405609 123559936 22986 4294967295 134512640 135450300 3221224624 3221223360 134538084 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30166 22986 231 231 0 29935 0
vsize: 120664
[startup+220.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30398 0 0 0 21912 84 0 0 25 0 1 0 544405609 123559936 23027 4294967295 134512640 135450300 3221224624 3221223360 134537987 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30166 23027 231 231 0 29935 0
vsize: 120664
[startup+230.018 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30429 0 0 0 22911 85 0 0 25 0 1 0 544405609 124608512 23058 4294967295 134512640 135450300 3221224624 3221223232 134537600 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30422 23058 231 231 0 30191 0
vsize: 121688
[startup+240.018 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 30471 0 0 0 23911 85 0 0 25 0 1 0 544405609 124608512 23100 4294967295 134512640 135450300 3221224624 3221223360 134537946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30422 23100 231 231 0 30191 0
vsize: 121688
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 39887 0 0 0 24895 102 0 0 25 0 1 0 544405609 160940032 31807 4294967295 134512640 135450300 3221224624 3221223232 134537659 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 39292 31807 231 231 0 39061 0
vsize: 157168
[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 43355 0 0 0 25890 107 0 0 25 0 1 0 544405609 175112192 35168 4294967295 134512640 135450300 3221224624 3221223232 134537664 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 42752 35169 231 231 0 42521 0
vsize: 171008
[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 47053 0 0 0 26884 114 0 0 25 0 1 0 544405609 189829120 38737 4294967295 134512640 135450300 3221224624 3221223360 134538018 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 46345 38737 231 231 0 46114 0
vsize: 185380
[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 48766 0 0 0 27882 116 0 0 25 0 1 0 544405609 196583424 40417 4294967295 134512640 135450300 3221224624 3221223360 134537987 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 47994 40417 231 231 0 47763 0
vsize: 191976
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 49413 0 0 0 28881 118 0 0 25 0 1 0 544405609 199016448 41064 4294967295 134512640 135450300 3221224624 3221223360 134538010 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 48588 41064 231 231 0 48357 0
vsize: 194352
[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 49441 0 0 0 29879 120 0 0 25 0 1 0 544405609 150384640 29242 4294967295 134512640 135450300 3221224624 3221223392 134533216 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 36715 29242 231 231 0 36484 0
vsize: 146860
[startup+303.833 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 6323
Raw data (stat): 6323 (PBS4) R 6322 27565 27564 0 -1 0 49441 0 0 0 29879 120 0 0 25 0 1 0 544405609 150384640 29242 4294967295 134512640 135450300 3221224624 3221223392 134533216 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 36715 29242 231 231 0 36484 0
vsize: 0

Child status: 20
Real time (s): 303.832
CPU time (s): 303.797
CPU user time (s): 302.541
CPU system time (s): 1.25581
CPU usage (%): 99.9884
Max. virtual memory (Kb): 194352
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####