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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-bnl2.opb
MD5SUM	25ba81ffd6b61270ad99e5bd6f700914
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	33700
Biggest coefficient in the objective function	314887372800
Number of bits for the biggest coefficient in the objective function	39
Sum of the numbers in the objective function	11048951166825
Number of bits of the sum of numbers in the objective function	44
Biggest number in a constraint	314887372800
Number of bits of the biggest number in a constraint	39
Biggest sum of numbers in a constraint	11048951166825
Number of bits of the biggest sum of numbers	44
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.632903
Number of variables	69780
Total number of constraints	2280
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	2280
Minimum length of a constraint	20
Maximum length of a constraint	1640

Trace number 26082

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-24 02:19:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15549 boxname=wulflinc31 idbench=1197 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  25ba81ffd6b61270ad99e5bd6f700914  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-bnl2.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-bnl2.opb
IDLAUNCH: 15549
/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:        607016 kB
Buffers:         26740 kB
Cached:         379976 kB
SwapCached:       1352 kB
Active:         291780 kB
Inactive:       117428 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        606764 kB
SwapTotal:     2097892 kB
SwapFree:      2095532 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            12880 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-24 02:23:43 (client local time) WITH STATUS 0 IN 228.371 SECONDS
stats: 15549 7 228.371 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c ERROR Parsing file!!!
c ERROR parsing line: -3053*X1001001_bit_7 -6106*X1001001_bit_6 -12212*X1001001_bit_5 -24424*X1001001_bit_4 -48848*X1001001_bit_3 -97696*X1001001_bit_2 -195392*X1001001_bit_1 -390784*X1001001_bit0 -781568*X1001001_bit1 -1563136*X1001001_bit2 -3126272*X1001001_bit3 -6252544*X1001001_bit4 -12505088*X1001001_bit5 -25010176*X1001001_bit6 -50020352*X1001001_bit7 -100040704*X1001001_bit8 -200081408*X1001001_bit9 -400162816*X1001001_bit10 -800325632*X1001001_bit11 -1600651264*X1001001_bit12 -4884*X1001002_bit_7 -9768*X1001002_bit_6 -19536*X1001002_bit_5 -39072*X1001002_bit_4 -78144*X1001002_bit_3 -156288*X1001002_bit_2 -312576*X1001002_bit_1 -625152*X1001002_bit0 -1250304*X1001002_bit1 -2500608*X1001002_bit2 -5001216*X1001002_bit3 -10002432*X1001002_bit4 -20004864*X1001002_bit5 -40009728*X1001002_bit6 -80019456*X1001002_bit7 -160038912*X1001002_bit8 -320077824*X1001002_bit9 -640155648*X1001002_bit10 -1280311296*X1001002_bit11 -2560622592*X1001002_bit12 -24420*X1001003_bit_7 -48840*X1001003_bit_6 -97680*X1001003_bit_5 -195360*X1001003_bit_4 -390720*X1001003_bit_3 -781440*X1001003_bit_2 -1562880*X1001003_bit_1 -3125760*X1001003_bit0 -6251520*X1001003_bit1 -12503040*X1001003_bit2 -25006080*X1001003_bit3 -50012160*X1001003_bit4 -100024320*X1001003_bit5 -200048640*X1001003_bit6 -400097280*X1001003_bit7 -800194560*X1001003_bit8 -1600389120*X1001003_bit9 -3200778240*X1001003_bit10 -6401556480*X1001003_bit11 -12803112960*X1001003_bit12 -3256*X1001009_bit_7 -6512*X1001009_bit_6 -13024*X1001009_bit_5 -26048*X1001009_bit_4 -52096*X1001009_bit_3 -104192*X1001009_bit_2 -208384*X1001009_bit_1 -416768*X1001009_bit0 -833536*X1001009_bit1 -1667072*X1001009_bit2 -3334144*X1001009_bit3 -6668288*X1001009_bit4 -13336576*X1001009_bit5 -26673152*X1001009_bit6 -53346304*X1001009_bit7 -106692608*X1001009_bit8 -213385216*X1001009_bit9 -426770432*X1001009_bit10 -853540864*X1001009_bit11 -1707081728*X1001009_bit12 -5814*X1001013_bit_7 -11628*X1001013_bit_6 -23256*X1001013_bit_5 -46512*X1001013_bit_4 -93024*X1001013_bit_3 -186048*X1001013_bit_2 -372096*X1001013_bit_1 -744192*X1001013_bit0 -1488384*X1001013_bit1 -2976768*X1001013_bit2 -5953536*X1001013_bit3 -11907072*X1001013_bit4 -23814144*X1001013_bit5 -47628288*X1001013_bit6 -95256576*X1001013_bit7 -190513152*X1001013_bit8 -381026304*X1001013_bit9 -762052608*X1001013_bit10 -1524105216*X1001013_bit11 -3048210432*X1001013_bit12 -5814*X1001014_bit_7 -11628*X1001014_bit_6 -23256*X1001014_bit_5 -46512*X1001014_bit_4 -93024*X1001014_bit_3 -186048*X1001014_bit_2 -372096*X1001014_bit_1 -744192*X1001014_bit0 -1488384*X1001014_bit1 -2976768*X1001014_bit2 -5953536*X1001014_bit3 -11907072*X1001014_bit4 -23814144*X1001014_bit5 -47628288*X1001014_bit6 -95256576*X1001014_bit7 -190513152*X1001014_bit8 -381026304*X1001014_bit9 -762052608*X1001014_bit10 -1524105216*X1001014_bit11 -3048210432*X1001014_bit12 -3053*X1001015_bit_7 -6106*X1001015_bit_6 -12212*X1001015_bit_5 -24424*X1001015_bit_4 -48848*X1001015_bit_3 -97696*X1001015_bit_2 -195392*X1001015_bit_1 -390784*X1001015_bit0 -781568*X1001015_bit1 -1563136*X1001015_bit2 -3126272*X1001015_bit3 -6252544*X1001015_bit4 -12505088*X1001015_bit5 -25010176*X1001015_bit6 -50020352*X1001015_bit7 -100040704*X1001015_bit8 -200081408*X1001015_bit9 -400162816*X1001015_bit10 -800325632*X1001015_bit11 -1600651264*X1001015_bit12 -3053*X1001018_bit_7 -6106*X1001018_bit_6 -12212*X1001018_bit_5 -24424*X1001018_bit_4 -48848*X1001018_bit_3 -97696*X1001018_bit_2 -195392*X1001018_bit_1 -390784*X1001018_bit0 -781568*X1001018_bit1 -1563136*X1001018_bit2 -3126272*X1001018_bit3 -6252544*X1001018_bit4 -12505088*X1001018_bit5 -25010176*X1001018_bit6 -50020352*X1001018_bit7 -100040704*X1001018_bit8 -200081408*X1001018_bit9 -400162816*X1001018_bit10 -800325632*X1001018_bit11 -1600651264*X1001018_bit12 -4884*X1001021_bit_7 -9768*X1001021_bit_6 -19536*X1001021_bit_5 -39072*X1001021_bit_4 -78144*X1001021_bit_3 -156288*X1001021_bit_2 -312576*X1001021_bit_1 -625152*X1001021_bit0 -1250304*X1001021_bit1 -2500608*X1001021_bit2 -5001216*X1001021_bit3 -10002432*X1001021_bit4 -20004864*X1001021_bit5 -40009728*X1001021_bit6 -80019456*X1001021_bit7 -160038912*X1001021_bit8 -320077824*X1001021_bit9 -640155648*X1001021_bit10 -1280311296*X1001021_bit11 -2560622592*X1001021_bit12 >= -7040000;
c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-bnl2.opb
s UNKNOWN
c Exit Code: 0
c Total time: 228.302 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.98 0.92 0.89 2/55 22283
Raw data (stat): 22283 (runsolver) R 22282 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 826568228 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0014 s]
Raw data (loadavg): 0.98 0.92 0.89 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 1226 0 0 0 990 5 0 0 25 0 1 0 826568228 17477632 1149 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 4267 1149 1111 63 0 4204 0
vsize: 17068
[startup+20.0022 s]
Raw data (loadavg): 0.99 0.92 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 1822 0 0 0 1989 6 0 0 25 0 1 0 826568228 19890176 1745 4294967295 134512640 134714508 3221221792 3221220020 1077414370 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 4856 1745 1111 63 0 4793 0
vsize: 19424
[startup+30.0021 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 2426 0 0 0 2988 7 0 0 25 0 1 0 826568228 22425600 2349 4294967295 134512640 134714508 3221221792 3221220020 1077414345 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 5475 2349 1111 63 0 5412 0
vsize: 21900
[startup+40.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 3041 0 0 0 3987 8 0 0 25 0 1 0 826568228 24825856 2964 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 6061 2964 1111 63 0 5998 0
vsize: 24244
[startup+50.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 3668 0 0 0 4987 9 0 0 25 0 1 0 826568228 27529216 3591 4294967295 134512640 134714508 3221221792 3221220020 1077414435 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 6721 3591 1111 63 0 6658 0
vsize: 26884
[startup+60.0029 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 4311 0 0 0 5986 10 0 0 25 0 1 0 826568228 30068736 4234 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 7341 4234 1111 63 0 7278 0
vsize: 29364
[startup+70.0039 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 5001 0 0 0 6985 11 0 0 25 0 1 0 826568228 32890880 4924 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8030 4924 1111 63 0 7967 0
vsize: 32120
[startup+80.0039 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 5735 0 0 0 7984 13 0 0 25 0 1 0 826568228 35856384 5658 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8754 5658 1111 63 0 8691 0
vsize: 35016
[startup+90.0047 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 6505 0 0 0 8982 15 0 0 25 0 1 0 826568228 39112704 6428 4294967295 134512640 134714508 3221221792 3221220020 1077414360 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 9549 6428 1111 63 0 9486 0
vsize: 38196
[startup+100.005 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 7320 0 0 0 9981 16 0 0 25 0 1 0 826568228 42504192 7243 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 10377 7243 1111 63 0 10314 0
vsize: 41508
[startup+110.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 8143 0 0 0 10980 17 0 0 25 0 1 0 826568228 45752320 8066 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 11170 8066 1111 63 0 11107 0
vsize: 44680
[startup+120.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 8994 0 0 0 11978 19 0 0 25 0 1 0 826568228 49283072 8917 4294967295 134512640 134714508 3221221792 3221220020 1077414370 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 12032 8917 1111 63 0 11969 0
vsize: 48128
[startup+130.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 9850 0 0 0 12976 21 0 0 25 0 1 0 826568228 52813824 9773 4294967295 134512640 134714508 3221221792 3221220020 1077414410 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 12894 9773 1111 63 0 12831 0
vsize: 51576
[startup+140.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 10776 0 0 0 13974 24 0 0 25 0 1 0 826568228 56627200 10699 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13825 10699 1111 63 0 13762 0
vsize: 55300
[startup+150.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 11831 0 0 0 14973 25 0 0 25 0 1 0 826568228 60940288 11754 4294967295 134512640 134714508 3221221792 3221220020 1077414357 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14878 11754 1111 63 0 14815 0
vsize: 59512
[startup+160.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 12977 0 0 0 15971 27 0 0 25 0 1 0 826568228 65736704 12900 4294967295 134512640 134714508 3221221792 3221220020 1077414420 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16049 12900 1111 63 0 15986 0
vsize: 64196
[startup+170.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 14209 0 0 0 16969 29 0 0 25 0 1 0 826568228 70680576 14132 4294967295 134512640 134714508 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17256 14132 1111 63 0 17193 0
vsize: 69024
[startup+180.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 15536 0 0 0 17967 32 0 0 25 0 1 0 826568228 76189696 15459 4294967295 134512640 134714508 3221221792 3221220020 1077414360 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18601 15459 1111 63 0 18538 0
vsize: 74404
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 16953 0 0 0 18963 35 0 0 25 0 1 0 826568228 81981440 16876 4294967295 134512640 134714508 3221221792 3221219660 1077244511 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 20015 16876 1111 63 0 19952 0
vsize: 80060
[startup+200.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 18549 0 0 0 19960 38 0 0 25 0 1 0 826568228 88473600 18472 4294967295 134512640 134714508 3221221792 3221220020 1077414351 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 21600 18472 1111 63 0 21537 0
vsize: 86400
[startup+210.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 20361 0 0 0 20957 42 0 0 25 0 1 0 826568228 95817728 20284 4294967295 134512640 134714508 3221221792 3221220448 134527930 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 23393 20284 1111 63 0 23330 0
vsize: 93572
[startup+220.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 22303 0 0 0 21954 46 0 0 25 0 1 0 826568228 103727104 22226 4294967295 134512640 134714508 3221221792 3221218476 1077359266 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 25324 22226 1111 63 0 25261 0
vsize: 101296
[startup+228.382 s]
Raw data (loadavg): 0.99 0.95 0.91 1/54 22283
Raw data (stat): 22283 (bsolo_lpr) R 22282 7876 7672 0 -1 0 22303 0 0 0 21954 46 0 0 25 0 1 0 826568228 103727104 22226 4294967295 134512640 134714508 3221221792 3221218476 1077359266 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 25324 22226 1111 63 0 25261 0
vsize: 0

Child status: 0
Real time (s): 228.382
CPU time (s): 228.371
CPU user time (s): 227.802
CPU system time (s): 0.568913
CPU usage (%): 99.9955
Max. virtual memory (Kb): 101296
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####