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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-cracpb1.opb
MD5SUM098fe473d82d5f7d4121673eb775be76
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 22199
Optimality of the best value was proved NO
Number of terms in the objective function 572
Biggest coefficient in the objective function 5000
Number of bits for the biggest coefficient in the objective function 13
Sum of the numbers in the objective function 547769
Number of bits of the sum of numbers in the objective function 20
Biggest number in a constraint 5000
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 547769
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark30.8603
Number of variables572
Total number of constraints716
Number of constraints which are clauses3
Number of constraints which are cardinality constraints (but not clauses)644
Number of constraints which are nor clauses,nor cardinality constraints69
Minimum length of a constraint1
Maximum length of a constraint518

Trace number 25907

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-23 09:35:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16745 boxname=wulflinc31 idbench=1289 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  098fe473d82d5f7d4121673eb775be76  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-cracpb1.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-cracpb1.opb
IDLAUNCH: 16745
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        911384 kB
Buffers:         28444 kB
Cached:          72244 kB
SwapCached:        972 kB
Active:          71992 kB
Inactive:        30872 kB
HighTotal:      131008 kB
HighFree:        70000 kB
LowTotal:       903652 kB
LowFree:        841384 kB
SwapTotal:     2097892 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14832 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-23 09:36:20 (client local time) WITH STATUS 30 IN 30.8973 SECONDS
stats: 16745 0 30.8973 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c Initial problem consists of 572 variables and 215 constraints.
c After prepocess the problem consists of 566 variables and 519 constraints.
c preprocess terminated 2.871 s
c Initial Lower Bound: 22199
c Lower Bound Elapsed time: 0.444333
c Use computed LB before first solution.
c NEW SOLUTION FOUND: 22199 @ 20.893
s OPTIMUM FOUND
v -GPT00001_bit0 -GPT00002_bit0 -GPT00003_bit0 -GPT00004_bit0 -GPT00005_bit0 GPT00006_bit0 -GPT00007_bit0 -GPT00008_bit0 -GPT00009_bit0 -GPT00010_bit0 GPT00011_bit0 -GPT00012_bit0 -GPT00013_bit0 -GPT00014_bit0 -GPT00015_bit0 GPT00016_bit0 -GPT00017_bit0 -GPT00018_bit0 GPT00019_bit0 -GPT00020_bit0 -GPT00021_bit0 -GPT00022_bit0 -GPT00023_bit0 GPT00024_bit0 -GPT00025_bit0 -GPT00026_bit0 -GPT00027_bit0 -GPT00028_bit0 -GPT00029_bit0 -GPT00030_bit0 -GPT00031_bit0 -GPT00032_bit0 GPT00033_bit0 -GPT00034_bit0 -GPT00035_bit0 GPT00036_bit0 -GPT00037_bit0 -GPT00038_bit0 -GPT00039_bit0 -GPT00040_bit0 -GPT00041_bit0 -GPT00042_bit0 -GPT00043_bit0 -GPT00044_bit0 -GPT00045_bit0 -GPT00046_bit0 -GPT00047_bit0 -GPT00048_bit0 -GPT00049_bit0 -GPT00050_bit0 GPT00051_bit0 -GPT00052_bit0 -GPT00053_bit0 -GPT00054_bit0 -GPT00055_bit0 GPT00056_bit0 -GPT00057_bit0 -GPT00058_bit0 GPT00059_bit0 -GPT00060_bit0 -GPT00061_bit0 GPT00062_bit0 -GPT00063_bit0 -GPT00064_bit0 -GPT00065_bit0 -GPT00066_bit0 -GPT00067_bit0 -GPT00068_bit0 -GPT00069_bit0 GPT00070_bit0 GPT00071_bit0 -GPT00072_bit0 -GPT00073_bit0 -GPT00074_bit0 -GPT00075_bit0 -GPT00076_bit0 -GPT00077_bit0 -GPT00078_bit0 -GPT00079_bit0 -GPT00080_bit0 -GPT00081_bit0 -GPT00082_bit0 -GPT00083_bit0 -GPT00084_bit0 -GPT00085_bit0 -GPT00086_bit0 -GPT00087_bit0 -GPT00088_bit0 -GPT00089_bit0 -GPT00090_bit0 -GPT00091_bit0 -GPT00092_bit0 -GPT00093_bit0 -GPT00094_bit0 -GPT00095_bit0 -GPT00096_bit0 -GPT00097_bit0 -GPT00098_bit0 -GPT00099_bit0 -GPT00100_bit0 -GPT00101_bit0 -GPT00102_bit0 -GPT00103_bit0 -GPT00104_bit0 -GPT00105_bit0 -GPT00106_bit0 -GPT00107_bit0 GPT00108_bit0 -GPT00109_bit0 -GPT00110_bit0 -GPT00111_bit0 -GPT00112_bit0 GPT00113_bit0 -GPT00114_bit0 -GPT00115_bit0 -GPT00116_bit0 GPT00117_bit0 -GPT00118_bit0 GPT00119_bit0 -GPT00120_bit0 -GPT00121_bit0 -GPT00122_bit0 -GPT00123_bit0 -GPT00124_bit0 -GPT00125_bit0 -GPT00126_bit0 -GPT00127_bit0 -GPT00128_bit0 -GPT00129_bit0 GPT00130_bit0 -GPT00131_bit0 -GPT00132_bit0 -GPT00133_bit0 -GPT00134_bit0 -GPT00135_bit0 -GPT00136_bit0 -GPT00137_bit0 -GPT00138_bit0 GPT00139_bit0 -GPT00140_bit0 -GPT00141_bit0 -GPT00142_bit0 -GPT00143_bit0 -GPT00144_bit0 -GPT00145_bit0 -GPT00146_bit0 -GPT00147_bit0 -GPT00148_bit0 -GPT00149_bit0 -GPT00150_bit0 -GPT00151_bit0 -GPT00152_bit0 -GPT00153_bit0 -GPT00154_bit0 -GPT00155_bit0 -GPT00156_bit0 GPT00157_bit0 -GPT00158_bit0 -GPT00159_bit0 -GPT00160_bit0 -GPT00161_bit0 -GPT00162_bit0 GPT00163_bit0 -GPT00164_bit0 -GPT00165_bit0 -GPT00166_bit0 -GPT00167_bit0 -GPT00168_bit0 -GPT00169_bit0 GPT00170_bit0 -GPT00171_bit0 -GPT00172_bit0 -GPT00173_bit0 -GPT00174_bit0 -GPT00175_bit0 -GPT00176_bit0 GPT00177_bit0 -GPT00178_bit0 -GPT00179_bit0 -GPT00180_bit0 -GPT00181_bit0 -GPT00182_bit0 -GPT00183_bit0 -GPT00184_bit0 GPT00185_bit0 -GPT00186_bit0 -GPT00187_bit0 -GPT00188_bit0 -GPT00189_bit0 -GPT00190_bit0 -GPT00191_bit0 GPT00192_bit0 -GPT00193_bit0 -GPT00194_bit0 -GPT00195_bit0 -GPT00196_bit0 -GPT00197_bit0 GPT00198_bit0 -GPT00199_bit0 -GPT00200_bit0 GPT00201_bit0 -GPT00202_bit0 GPT00203_bit0 -GPT00204_bit0 GPT00205_bit0 -GPT00206_bit0 -GPT00207_bit0 -GPT00208_bit0 -GPT00209_bit0 -GPT00210_bit0 -GPT00211_bit0 -GPT00212_bit0 -GPT00213_bit0 -GPT00214_bit0 GPT00215_bit0 -GPT00216_bit0 -GPT00217_bit0 -GPT00218_bit0 -GPT00219_bit0 -GPT00220_bit0 -GPT00221_bit0 -GPT00222_bit0 -GPT00223_bit0 -GPT00224_bit0 -GPT00225_bit0 -GPT00226_bit0 -GPT00227_bit0 -GPT00228_bit0 -GPT00229_bit0 -GPT00230_bit0 -GPT00231_bit0 GPT00232_bit0 -GPT00233_bit0 GPT00234_bit0 -GPT00235_bit0 -GPT00236_bit0 -GPT00237_bit0 -GPT00238_bit0 -GPT00239_bit0 GPT00240_bit0 -GPT00241_bit0 GPT00242_bit0 -GPT00243_bit0 -GPT00244_bit0 -GPT00245_bit0 -GPT00246_bit0 -GPT00247_bit0 -GPT00248_bit0 -GPT00249_bit0 -GPT00250_bit0 -GPT00251_bit0 -GPT00252_bit0 GPT00253_bit0 -GPT00254_bit0 -GPT00255_bit0 GPT00256_bit0 -GPT00257_bit0 -GPT00258_bit0 -GPT00259_bit0 -GPT00260_bit0 -GPT00261_bit0 -GPT00262_bit0 -GPT00263_bit0 -GPT00264_bit0 -GPT00265_bit0 GPT00266_bit0 -GPT00267_bit0 -GPT00268_bit0 -GPT00269_bit0 GPT00270_bit0 -GPT00271_bit0 -GPT00272_bit0 -GPT00273_bit0 -GPT00274_bit0 -GPT00275_bit0 -GPT00276_bit0 -GPT00277_bit0 GPT00278_bit0 -GPT00279_bit0 -GPT00280_bit0 -GPT00281_bit0 -GPT00282_bit0 -GPT00283_bit0 -GPT00284_bit0 -GPT00285_bit0 -GPT00286_bit0 -GPT00287_bit0 -GPT00288_bit0 -GPT00289_bit0 -GPT00290_bit0 -GPT00291_bit0 -GPT00292_bit0 -GPT00293_bit0 -GPT00294_bit0 -GPT00295_bit0 -GPT00296_bit0 -GPT00297_bit0 -GPT00298_bit0 -GPT00299_bit0 -GPT00300_bit0 -GPT00301_bit0 -GPT00302_bit0 GPT00303_bit0 -GPT00304_bit0 -GPT00305_bit0 -GPT00306_bit0 -GPT00307_bit0 -GPT00308_bit0 -GPT00309_bit0 -GPT00310_bit0 -GPT00311_bit0 -GPT00312_bit0 -GPT00313_bit0 -GPT00314_bit0 -GPT00315_bit0 -GPT00316_bit0 -GPT00317_bit0 GPT00318_bit0 -GPT00319_bit0 -GPT00320_bit0 -GPT00321_bit0 GPT00322_bit0 -GPT00323_bit0 GPT00324_bit0 -GPT00325_bit0 -GPT00326_bit0 -GPT00327_bit0 -GPT00328_bit0 -GPT00329_bit0 -GPT00330_bit0 -GPT00331_bit0 -GPT00332_bit0 -GPT00333_bit0 -GPT00334_bit0 -GPT00335_bit0 -GPT00336_bit0 -GPT00337_bit0 -GPT00338_bit0 -GPT00339_bit0 -GPT00340_bit0 -GPT00341_bit0 -GPT00342_bit0 -GPT00343_bit0 -GPT00344_bit0 -GPT00345_bit0 -GPT00346_bit0 -GPT00347_bit0 -GPT00348_bit0 -GPT00349_bit0 -GPT00350_bit0 -GPT00351_bit0 -GPT00352_bit0 -GPT00353_bit0 -GPT00354_bit0 -GPT00355_bit0 -GPT00356_bit0 -GPT00357_bit0 -GPT00358_bit0 -GPT00359_bit0 -GPT00360_bit0 -GPT00361_bit0 -GPT00362_bit0 -GPT00363_bit0 -GPT00364_bit0 -GPT00365_bit0 -GPT00366_bit0 -GPT00367_bit0 -GPT00368_bit0 -GPT00369_bit0 -GPT00370_bit0 -GPT00371_bit0 -GPT00372_bit0 -GPT00373_bit0 -GPT00374_bit0 -GPT00375_bit0 GPT00376_bit0 -GPT00377_bit0 -GPT00378_bit0 -GPT00379_bit0 -GPT00380_bit0 -GPT00381_bit0 -GPT00382_bit0 -GPT00383_bit0 GPT00384_bit0 GPT00385_bit0 -GPT00386_bit0 -GPT00387_bit0 GPT00388_bit0 GPT00389_bit0 -GPT00390_bit0 -GPT00391_bit0 -GPT00392_bit0 -GPT00393_bit0 -GPT00394_bit0 -GPT00395_bit0 GPT00396_bit0 -GPT00397_bit0 -GPT00398_bit0 -GPT00399_bit0 -GPT00400_bit0 -GPT00401_bit0 -GPT00402_bit0 -GPT00403_bit0 -GPT00404_bit0 -GPT00405_bit0 -GPT00406_bit0 -GPT00407_bit0 -GPT00408_bit0 -GPT00409_bit0 -GPT00410_bit0 -GPT00411_bit0 -GPT00412_bit0 -GPT00413_bit0 -GPT00414_bit0 -GPT00415_bit0 -GPT00416_bit0 -GPT00417_bit0 -GPT00418_bit0 -GPT00419_bit0 -GPT00420_bit0 GPT00421_bit0 -GPT00422_bit0 -GPT00423_bit0 -GPT00424_bit0 -GPT00425_bit0 -GPT00426_bit0 -GPT00427_bit0 -GPT00428_bit0 -GPT00429_bit0 -GPT00430_bit0 -GPT00431_bit0 -GPT00432_bit0 -GPT00433_bit0 -GPT00434_bit0 -GPT00435_bit0 -GPT00436_bit0 -GPT00437_bit0 -GPT00438_bit0 -GPT00439_bit0 -GPT00440_bit0 -GPT00441_bit0 -GPT00442_bit0 -GPT00443_bit0 -GPT00444_bit0 -GPT00445_bit0 -GPT00446_bit0 -GPT00447_bit0 -GPT00448_bit0 -GPT00449_bit0 -GPT00450_bit0 -GPT00451_bit0 -GPT00452_bit0 -GPT00453_bit0 -GPT00454_bit0 -GPT00455_bit0 -GPT00456_bit0 -GPT00457_bit0 -GPT00458_bit0 -GPT00459_bit0 -GPT00460_bit0 -GPT00461_bit0 -GPT00462_bit0 -GPT00463_bit0 -GPT00464_bit0 -GPT00465_bit0 -GPT00466_bit0 -GPT00467_bit0 -GPT00468_bit0 -GPT00469_bit0 -GPT00470_bit0 -GPT00471_bit0 GPT00472_bit0 -GPT00473_bit0 -GPT00474_bit0 -GPT00475_bit0 -GPT00476_bit0 GPT00477_bit0 -GPT00478_bit0 -GPT00479_bit0 -GPT00480_bit0 -GPT00481_bit0 GPT00482_bit0 -GPT00483_bit0 -GPT00484_bit0 -GPT00485_bit0 -GPT00486_bit0 -GPT00487_bit0 -GPT00488_bit0 -GPT00489_bit0 -GPT00490_bit0 -GPT00491_bit0 -GPT00492_bit0 -GPT00493_bit0 -GPT00494_bit0 -GPT00495_bit0 -GPT00496_bit0 -GPT00497_bit0 -GPT00498_bit0 -GPT00499_bit0 -GPT00500_bit0 -GPT00501_bit0 -GPT00502_bit0 -GPT00503_bit0 -GPT00504_bit0 -GPT00505_bit0 -GPT00506_bit0 -GPT00507_bit0 -GPT00508_bit0 -GPT00509_bit0 -GPT00510_bit0 -GPT00511_bit0 -GPT00512_bit0 -GPT00513_bit0 -GPT00514_bit0 -GPT00515_bit0 -GPT00516_bit0 -GPT00517_bit0 -GPT00518_bit0 -ECAR0001_bit0 -ECAR0002_bit0 -ECAR0003_bit0 -ECAR0004_bit0 -ECAR0005_bit0 -ECAR0006_bit0 -ECAR0007_bit0 -ECAR0008_bit0 -ECAR0009_bit0 -ECAR0010_bit0 -ECAR0011_bit0 -ECAR0012_bit0 -ECAR0013_bit0 -ECAR0014_bit0 -ECAR0015_bit0 -ECAR0016_bit0 -ECAR0017_bit0 -ECAR0018_bit0 -ECAR0019_bit0 -ECAR0020_bit0 -ECAR0021_bit0 -ECAR0022_bit0 -ECAR0023_bit0 -ECAR0024_bit0 -ECAR0025_bit0 -ECAR0026_bit0 -ECAR0027_bit0 -ECAR0028_bit0 -ECAR0029_bit0 -ECAR0030_bit0 -ECAR0031_bit0 -ECAR0032_bit0 -ECAR0033_bit0 -ECAR0034_bit0 -ECAR0035_bit0 -ECAR0036_bit0 -ECAR0037_bit0 -ECAR0038_bit0 -ECAR0039_bit0 -ECAR0040_bit0 -ECAR0041_bit0 -ECAR0042_bit0 -ECAR0043_bit0 -ECAR0044_bit0 -ECAR0045_bit0 -ECAR0046_bit0 -ECAR0047_bit0 -ECAR0048_bit0 -ECAR0049_bit0 -ECAR0050_bit0 -ECAR0051_bit0 -ECAR0052_bit0 -ECAR0053_bit0 -ECAR0054_bit0 
c Exit Code: 30
c Total time: 30.873 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.92 0.95 0.93 2/55 4767
Raw data (stat): 4767 (runsolver) R 4766 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 820542947 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.96 0.93 2/55 4767
Raw data (stat): 4767 (bsolo_lpr) R 4766 7876 7672 0 -1 0 8255 0 0 0 972 22 0 0 25 0 1 0 820542947 22589440 4775 4294967295 134512640 134714508 3221221776 3221217788 1074788950 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 5515 4775 1111 63 0 5452 0
vsize: 22060
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.93 2/55 4767
Raw data (stat): 4767 (bsolo_lpr) R 4766 7876 7672 0 -1 0 13304 0 0 0 1958 36 0 0 25 0 1 0 820542947 21770240 4631 4294967295 134512640 134714508 3221221776 3221220064 1074153800 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5315 4631 1111 63 0 5252 0
vsize: 21260
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.93 2/55 4767
Raw data (stat): 4767 (bsolo_lpr) R 4766 7876 7672 0 -1 0 17452 0 0 0 2947 46 0 0 25 0 1 0 820542947 22511616 4756 4294967295 134512640 134714508 3221221776 3221217952 1074882530 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 5496 4756 1111 63 0 5433 0
vsize: 21984
[startup+30.9538 s]
Raw data (loadavg): 0.95 0.96 0.93 1/54 4767
Raw data (stat): 4767 (bsolo_lpr) R 4766 7876 7672 0 -1 0 17452 0 0 0 2947 46 0 0 25 0 1 0 820542947 22511616 4756 4294967295 134512640 134714508 3221221776 3221217952 1074882530 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 5496 4756 1111 63 0 5433 0
vsize: 0

Child status: 30
Real time (s): 30.9532
CPU time (s): 30.8973
CPU user time (s): 30.4094
CPU system time (s): 0.487925
CPU usage (%): 99.8195
Max. virtual memory (Kb): 22060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	22199
#### END VERIFIER DATA ####