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/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos16.opb
MD5SUM	44281820d2b00a47b643433ffa4e2d73
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	117
Optimality of the best value was proved	NO
Number of terms in the objective function	8
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	255
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	138
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	535
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	5.96709
Number of variables	464
Total number of constraints	1395
Number of constraints which are clauses	336
Number of constraints which are cardinality constraints (but not clauses)	336
Number of constraints which are nor clauses,nor cardinality constraints	723
Minimum length of a constraint	1
Maximum length of a constraint	128

Trace number 13448

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-20 21:10:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14592 boxname=wulflinc20 idbench=1123 idsolver=6 numberseed=0
MD5SUM SOLVER: 2225cba0d9b2c30e235f6cafc823d7ac  /oldhome/oroussel/solvers/PBS4
MD5SUM BENCH:  44281820d2b00a47b643433ffa4e2d73  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-neos16.opb
REAL COMMAND:  PBS4 /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-neos16.opb
IDLAUNCH: 14592
/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:        783044 kB
Buffers:         33632 kB
Cached:         192280 kB
SwapCached:        528 kB
Active:         110804 kB
Inactive:       117052 kB
HighTotal:      131008 kB
HighFree:        13104 kB
LowTotal:       903652 kB
LowFree:        769940 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            17920 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 21:10:24 (client local time) WITH STATUS 30 IN 5.96709 SECONDS
stats: 14592 0 5.96709 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c PBS v4 by Bashar Al-Rawi & Fadi Aloul
c Solving /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-neos16.opb ......
c The optimum solution is:129
s OPTIMUM FOUND
v C0001_bit0 -C0002_bit0 C0003_bit0 C0004_bit0 C0005_bit0 C0006_bit0 -C0007_bit0 C0008_bit0 C0009_bit0 C0010_bit0 -C0011_bit0 C0012_bit0 C0013_bit0 C0014_bit0 C0015_bit0 -C0016_bit0 -C0017_bit0 -C0018_bit0 -C0019_bit0 -C0020_bit0 -C0021_bit0 C0022_bit0 C0023_bit0 C0024_bit0 C0025_bit0 C0026_bit0 C0027_bit0 C0028_bit0 C0029_bit0 -C0030_bit0 C0031_bit0 C0032_bit0 -C0033_bit0 -C0034_bit0 C0035_bit0 -C0036_bit0 -C0037_bit0 C0038_bit0 C0039_bit0 C0040_bit0 C0041_bit0 -C0042_bit0 C0043_bit0 -C0044_bit0 C0045_bit0 -C0046_bit0 C0047_bit0 C0048_bit0 -C0049_bit0 C0050_bit0 -C0051_bit0 -C0052_bit0 C0053_bit0 C0054_bit0 -C0055_bit0 C0056_bit0 C0057_bit0 -C0058_bit0 -C0059_bit0 -C0060_bit0 C0061_bit0 C0062_bit0 C0063_bit0 C0064_bit0 -C0065_bit0 -C0066_bit0 -C0067_bit0 -C0068_bit0 -C0069_bit0 -C0070_bit0 -C0071_bit0 -C0072_bit0 -C0073_bit0 -C0074_bit0 -C0075_bit0 -C0076_bit0 -C0077_bit0 -C0078_bit0 C0079_bit0 C0080_bit0 C0081_bit0 -C0082_bit0 -C0083_bit0 -C0084_bit0 -C0085_bit0 C0086_bit0 -C0087_bit0 -C0088_bit0 -C0089_bit0 -C0090_bit0 C0091_bit0 -C0092_bit0 -C0093_bit0 -C0094_bit0 C0095_bit0 -C0096_bit0 -C0097_bit0 -C0098_bit0 -C0099_bit0 C0100_bit0 C0101_bit0 C0102_bit0 C0103_bit0 C0104_bit0 C0105_bit0 -C0106_bit0 -C0107_bit0 -C0108_bit0 -C0109_bit0 -C0110_bit0 -C0111_bit0 -C0112_bit0 -C0113_bit0 C0114_bit0 -C0115_bit0 -C0116_bit0 C0117_bit0 C0118_bit0 -C0119_bit0 C0120_bit0 C0121_bit0 -C0122_bit0 -C0123_bit0 -C0124_bit0 -C0125_bit0 C0126_bit0 -C0127_bit0 C0128_bit0 -C0129_bit0 C0130_bit0 -C0131_bit0 -C0132_bit0 C0133_bit0 -C0134_bit0 C0135_bit0 C0136_bit0 -C0137_bit0 -C0138_bit0 C0139_bit0 -C0140_bit0 -C0141_bit0 C0142_bit0 C0143_bit0 C0144_bit0 -C0145_bit0 -C0146_bit0 -C0147_bit0 -C0148_bit0 C0149_bit0 C0150_bit0 C0151_bit0 C0152_bit0 C0153_bit0 C0154_bit0 C0155_bit0 C0156_bit0 C0157_bit0 C0158_bit0 C0159_bit0 C0160_bit0 C0161_bit0 C0162_bit0 -C0163_bit0 -C0164_bit0 -C0165_bit0 C0166_bit0 C0167_bit0 C0168_bit0 C0169_bit0 -C0170_bit0 C0171_bit0 C0172_bit0 C0173_bit0 C0174_bit0 -C0175_bit0 -C0176_bit0 -C0177_bit0 C0178_bit0 C0179_bit0 C0180_bit0 C0181_bit0 C0182_bit0 C0183_bit0 -C0184_bit0 C0185_bit0 C0186_bit0 C0187_bit0 C0188_bit0 -C0189_bit0 C0190_bit0 C0191_bit0 C0192_bit0 C0193_bit0 C0194_bit0 C0195_bit0 C0196_bit0 C0197_bit0 -C0198_bit0 -C0199_bit0 C0200_bit0 C0201_bit0 -C0202_bit0 -C0203_bit0 -C0204_bit0 -C0205_bit0 -C0206_bit0 -C0207_bit0 C0208_bit0 C0209_bit0 C0210_bit0 -C0211_bit0 -C0212_bit0 C0213_bit0 -C0214_bit0 -C0215_bit0 -C0216_bit0 -C0217_bit0 C0218_bit0 -C0219_bit0 -C0220_bit0 -C0221_bit0 C0222_bit0 -C0223_bit0 C0224_bit0 C0225_bit0 -C0226_bit0 -C0227_bit0 -C0228_bit0 C0229_bit0 C0230_bit0 C0231_bit0 C0232_bit0 C0233_bit0 C0234_bit0 C0235_bit0 -C0236_bit0 -C0237_bit0 C0238_bit0 C0239_bit0 C0240_bit0 -C0241_bit0 -C0242_bit0 C0243_bit0 C0244_bit0 -C0245_bit0 -C0246_bit0 -C0247_bit0 -C0248_bit0 -C0249_bit0 -C0250_bit0 -C0251_bit0 C0252_bit0 -C0253_bit0 C0254_bit0 -C0255_bit0 -C0256_bit0 -C0257_bit0 -C0258_bit0 C0259_bit0 C0260_bit0 C0261_bit0 -C0262_bit0 -C0263_bit0 -C0264_bit0 -C0265_bit0 -C0266_bit0 -C0267_bit0 C0268_bit0 -C0269_bit0 -C0270_bit0 -C0271_bit0 -C0272_bit0 C0273_bit0 -C0274_bit0 -C0275_bit0 -C0276_bit0 -C0277_bit0 -C0278_bit0 -C0279_bit0 -C0280_bit0 -C0281_bit0 C0282_bit0 C0283_bit0 -C0284_bit0 -C0285_bit0 C0286_bit0 C0287_bit0 C0288_bit0 C0289_bit0 C0290_bit0 C0291_bit0 -C0292_bit0 -C0293_bit0 -C0294_bit0 C0295_bit0 C0296_bit0 -C0297_bit0 C0298_bit0 C0299_bit0 C0300_bit0 C0301_bit0 -C0302_bit0 C0303_bit0 C0304_bit0 C0305_bit0 -C0306_bit0 C0307_bit0 -C0308_bit0 -C0309_bit0 C0310_bit0 C0311_bit0 C0312_bit0 -C0313_bit0 -C0314_bit0 -C0315_bit0 -C0316_bit0 -C0317_bit0 -C0318_bit0 -C0319_bit0 C0320_bit0 C0321_bit0 -C0322_bit0 -C0323_bit0 -C0324_bit0 C0325_bit0 C0326_bit0 -C0327_bit0 -C0328_bit0 C0329_bit0 C0330_bit0 C0331_bit0 C0332_bit0 C0333_bit0 C0334_bit0 C0335_bit0 -C0336_bit0 C0337_bit0 -C0337_bit1 -C0337_bit2 C0338_bit0 C0338_bit1 -C0338_bit2 -C0339_bit0 -C0339_bit1 -C0339_bit2 -C0340_bit0 C0340_bit1 C0340_bit2 C0341_bit0 -C0341_bit1 C0341_bit2 -C0342_bit0 -C0342_bit1 C0342_bit2 -C0343_bit0 C0343_bit1 -C0343_bit2 -C0344_bit0 -C0344_bit1 C0344_bit2 C0345_bit0 C0345_bit1 -C0345_bit2 -C0346_bit0 -C0346_bit1 C0346_bit2 C0347_bit0 C0347_bit1 -C0347_bit2 -C0348_bit0 -C0348_bit1 -C0348_bit2 -C0349_bit0 C0349_bit1 -C0349_bit2 C0350_bit0 -C0350_bit1 C0350_bit2 C0351_bit0 C0351_bit1 -C0351_bit2 C0352_bit0 -C0352_bit1 -C0352_bit2 -C0353_bit0 C0353_bit1 C0353_bit2 -C0354_bit0 -C0354_bit1 C0354_bit2 C0355_bit0 C0355_bit1 -C0355_bit2 -C0356_bit0 C0356_bit1 C0356_bit2 -C0357_bit0 C0357_bit1 C0357_bit2 -C0358_bit0 C0358_bit1 C0358_bit2 -C0359_bit0 C0359_bit1 -C0359_bit2 -C0360_bit0 -C0360_bit1 C0360_bit2 C0361_bit0 -C0361_bit1 -C0361_bit2 -C0362_bit0 C0362_bit1 C0362_bit2 -C0363_bit0 -C0363_bit1 -C0363_bit2 C0364_bit0 C0364_bit1 -C0364_bit2 C0365_bit0 -C0365_bit1 C0365_bit2 -C0366_bit0 C0366_bit1 C0366_bit2 -C0367_bit0 C0367_bit1 -C0367_bit2 -C0368_bit0 C0368_bit1 -C0368_bit2 -C0369_bit0 -C0369_bit1 -C0369_bit2 C0370_bit0 -C0370_bit1 C0370_bit2 -C0371_bit0 C0371_bit1 C0371_bit2 -C0372_bit0 -C0372_bit1 C0372_bit2 -C0373_bit0 -C0373_bit1 -C0373_bit2 C0374_bit0 C0374_bit1 -C0374_bit2 -C0375_bit0 C0375_bit1 -C0375_bit2 C0376_bit0 -C0376_bit1 -C0376_bit2 C0377_bit0 -C0377_bit1 -C0377_bit2 -C0377_bit3 -C0377_bit4 -C0377_bit5 -C0377_bit6 C0377_bit7 
c Done, CPU Time=5.86411
#### 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.92 0.97 0.90 2/54 22373
Raw data (stat): 22373 (runsolver) R 22372 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539570832 1052672 99 4294967295 134512640 135381576 3221224528 3221219776 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+5.9715 s]
Raw data (loadavg): 0.93 0.97 0.90 1/53 22373
Raw data (stat): 22373 (runsolver) R 22372 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539570832 1052672 99 4294967295 134512640 135381576 3221224528 3221219776 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 0

Child status: 30
Real time (s): 5.9712
CPU time (s): 5.96709
CPU user time (s): 5.9261
CPU system time (s): 0.040993
CPU usage (%): 99.9312
Max. virtual memory (Kb): 1028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	129
#### END VERIFIER DATA ####