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-neos5.opb
MD5SUM	4f5f6e30a602f3968daa9ca41c7da043
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2058
Optimality of the best value was proved	NO
Number of terms in the objective function	133
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	9334
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1024
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	9334
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05284
Number of variables	133
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	81

Trace number 25248

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-17 23:36:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19711 boxname=wulflinc31 idbench=1517 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  4f5f6e30a602f3968daa9ca41c7da043  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-neos5.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-neos5.opb
IDLAUNCH: 19711
/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:        790104 kB
Buffers:         33640 kB
Cached:         186496 kB
SwapCached:       2836 kB
Active:         121372 kB
Inactive:       103884 kB
HighTotal:      131008 kB
HighFree:          980 kB
LowTotal:       903652 kB
LowFree:        789124 kB
SwapTotal:     2097892 kB
SwapFree:      2094220 kB
Dirty:             124 kB
Writeback:           0 kB
Mapped:           5380 kB
Slab:            13604 kB
Committed_AS:    63840 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-17 23:37:49 (client local time) WITH STATUS 0 IN 101.064 SECONDS
stats: 19711 7 101.064 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Initial problem consists of 133 variables and 73 constraints.
c After prepocess the problem consists of 133 variables and 73 constraints.
c preprocess terminated 0.266 s
c Initial Lower Bound: 896
c Lower Bound Elapsed time: 0
c Use computed LB before first solution.
c NEW SOLUTION FOUND: 2694 @ 0.35
c NEW SOLUTION FOUND: 2678 @ 0.352
#### 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.86 0.97 0.96 2/55 31918
Raw data (stat): 31918 (runsolver) R 31917 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 773739472 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.0003 s]
Raw data (loadavg): 0.88 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 22110 0 0 0 941 55 0 0 25 0 1 0 773739472 95965184 21829 4294967295 134512640 134714540 3221221776 3221220400 134542936 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 23429 21829 1111 63 0 23366 0
vsize: 93716
[startup+20.0019 s]
Raw data (loadavg): 0.90 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 42242 0 0 0 1895 101 0 0 25 0 1 0 773739472 180326400 41576 4294967295 134512640 134714540 3221221776 3221220496 134592116 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 44025 41576 1111 63 0 43962 0
vsize: 176100
[startup+30.0041 s]
Raw data (loadavg): 0.91 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 67787 0 0 0 2839 158 0 0 25 0 1 0 773739472 283389952 64176 4294967295 134512640 134714540 3221221776 3221220200 1077377768 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 69187 64176 1111 63 0 69124 0
vsize: 276748
[startup+40.004 s]
Raw data (loadavg): 0.93 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 87789 0 0 0 3791 205 0 0 25 0 1 0 773739472 361918464 83900 4294967295 134512640 134714540 3221221776 3221220200 1077377725 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 88359 83900 1111 63 0 88296 0
vsize: 353436
[startup+50.0047 s]
Raw data (loadavg): 0.94 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 109981 0 0 0 4742 255 0 0 25 0 1 0 773739472 451280896 105895 4294967295 134512640 134714540 3221221776 3221220340 134543025 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 110176 105895 1111 63 0 110113 0
vsize: 440704
[startup+60.0049 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 146569 0 0 0 5661 336 0 0 25 0 1 0 773739472 592121856 134352 4294967295 134512640 134714540 3221221776 3221220440 134591891 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 144561 134352 1111 63 0 144498 0
vsize: 578244
[startup+70.0048 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 160445 0 0 0 6623 374 0 0 25 0 1 0 773739472 646426624 147957 4294967295 134512640 134714540 3221221776 3221220200 1077377401 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 157819 147957 1111 63 0 157756 0
vsize: 631276
[startup+80.0056 s]
Raw data (loadavg): 0.96 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 182590 0 0 0 7567 430 0 0 25 0 1 0 773739472 732815360 169694 4294967295 134512640 134714540 3221221776 3221220072 1077378037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 178910 169695 1111 63 0 178847 0
vsize: 715640
[startup+90.0055 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 211593 0 0 0 8490 506 0 0 25 0 1 0 773739472 845291520 197713 4294967295 134512640 134714540 3221221776 3221220648 134543606 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 206370 197713 1111 63 0 206307 0
vsize: 825480
[startup+100.006 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 236092 0 0 0 9415 579 0 0 25 0 1 0 773739472 936476672 218166 4294967295 134512640 134714540 3221221776 3221220316 134543615 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 228632 218166 1111 63 0 228569 0
vsize: 914528
[startup+101.372 s]
Raw data (loadavg): 0.97 0.97 0.96 1/54 31918
Raw data (stat): 31918 (bsolo_mis) R 31917 7876 7672 0 -1 0 236092 0 0 0 9415 579 0 0 25 0 1 0 773739472 936476672 218166 4294967295 134512640 134714540 3221221776 3221220316 134543615 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 228632 218166 1111 63 0 228569 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 101.371
CPU time (s): 101.064
CPU user time (s): 94.7866
CPU system time (s): 6.27704
CPU usage (%): 99.6968
Max. virtual memory (Kb): 914528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####