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/MIPLIB/miplib2003/normalized-mps-v2-13-7-fast0507.opb
MD5SUM	38504d32a17a57a658eee171614b901e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	324
Optimality of the best value was proved	NO
Number of terms in the objective function	63009
Biggest coefficient in the objective function	2
Number of bits for the biggest coefficient in the objective function	2
Sum of the numbers in the objective function	122425
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	2
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	122425
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.19
Number of variables	63009
Total number of constraints	63516
Number of constraints which are clauses	507
Number of constraints which are cardinality constraints (but not clauses)	63009
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	7753

Trace number 27372

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-24 21:33:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17514 boxname=wulflinc24 idbench=1348 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  38504d32a17a57a658eee171614b901e  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fast0507.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fast0507.opb
IDLAUNCH: 17514
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        775328 kB
Buffers:         36588 kB
Cached:         198748 kB
SwapCached:        624 kB
Active:          72396 kB
Inactive:       165424 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        775076 kB
SwapTotal:     2097892 kB
SwapFree:      2096776 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5652 kB
Slab:            15816 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-24 21:39:20 (client local time) WITH STATUS 0 IN 368.42 SECONDS
stats: 17514 7 368.42 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
#### 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.96 2/54 8266
Raw data (stat): 8266 (runsolver) R 8265 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 833505982 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 5031 0 0 0 988 10 0 0 25 0 1 0 833505982 33427456 5009 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8161 5009 1111 63 0 8098 0
vsize: 32644
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 9638 0 0 0 1979 19 0 0 25 0 1 0 833505982 52224000 9616 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12750 9616 1111 63 0 12687 0
vsize: 51000
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 14293 0 0 0 2971 28 0 0 25 0 1 0 833505982 71335936 14271 4294967295 134512640 134714540 3221224592 3221222820 1077414410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17416 14271 1111 63 0 17353 0
vsize: 69664
[startup+40.0011 s]
Raw data (loadavg): 0.96 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 18983 0 0 0 3962 37 0 0 25 0 1 0 833505982 90595328 18961 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 22118 18961 1111 63 0 22055 0
vsize: 88472
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 23709 0 0 0 4955 45 0 0 25 0 1 0 833505982 109858816 23687 4294967295 134512640 134714540 3221224592 3221222820 1077414408 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 26821 23687 1111 63 0 26758 0
vsize: 107284
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 28499 0 0 0 5946 53 0 0 25 0 1 0 833505982 129564672 28477 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 31632 28477 1111 63 0 31569 0
vsize: 126528
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 33328 0 0 0 6937 63 0 0 25 0 1 0 833505982 149270528 33306 4294967295 134512640 134714540 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 36443 33306 1111 63 0 36380 0
vsize: 145772
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 38221 0 0 0 7929 71 0 0 25 0 1 0 833505982 169426944 38199 4294967295 134512640 134714540 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 41364 38199 1111 63 0 41301 0
vsize: 165456
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 43168 0 0 0 8921 79 0 0 25 0 1 0 833505982 189587456 43146 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 46286 43146 1111 63 0 46223 0
vsize: 185144
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 48180 0 0 0 9911 89 0 0 25 0 1 0 833505982 210190336 48158 4294967295 134512640 134714540 3221224592 3221222820 1077414349 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 51316 48158 1111 63 0 51253 0
vsize: 205264
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 53271 0 0 0 10902 99 0 0 25 0 1 0 833505982 231116800 53249 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 56425 53249 1111 63 0 56362 0
vsize: 225700
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 58479 0 0 0 11893 108 0 0 25 0 1 0 833505982 252317696 58457 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 61601 58457 1111 63 0 61538 0
vsize: 246404
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 63863 0 0 0 12884 116 0 0 25 0 1 0 833505982 274411520 63841 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 66995 63841 1111 63 0 66932 0
vsize: 267980
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 69338 0 0 0 13875 126 0 0 25 0 1 0 833505982 296804352 69316 4294967295 134512640 134714540 3221224592 3221222820 1077414424 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 72462 69316 1111 63 0 72399 0
vsize: 289848
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 74880 0 0 0 14865 136 0 0 25 0 1 0 833505982 319500288 74858 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 78003 74858 1111 63 0 77940 0
vsize: 312012
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 80496 0 0 0 15855 146 0 0 25 0 1 0 833505982 342495232 80474 4294967295 134512640 134714540 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 83617 80474 1111 63 0 83554 0
vsize: 334468
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 86196 0 0 0 16845 156 0 0 25 0 1 0 833505982 365932544 86174 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 89339 86174 1111 63 0 89276 0
vsize: 357356
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 91969 0 0 0 17835 166 0 0 25 0 1 0 833505982 389525504 91947 4294967295 134512640 134714540 3221224592 3221222820 1077414385 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 95099 91947 1111 63 0 95036 0
vsize: 380396
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 97834 0 0 0 18826 176 0 0 25 0 1 0 833505982 413642752 97812 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 100987 97812 1111 63 0 100924 0
vsize: 403948
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 103774 0 0 0 19816 186 0 0 25 0 1 0 833505982 437964800 103752 4294967295 134512640 134714540 3221224592 3221222820 1077414410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 106925 103752 1111 63 0 106862 0
vsize: 427700
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 109779 0 0 0 20805 198 0 0 25 0 1 0 833505982 462602240 109757 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 112940 109757 1111 63 0 112877 0
vsize: 451760
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 115923 0 0 0 21795 208 0 0 25 0 1 0 833505982 487686144 115901 4294967295 134512640 134714540 3221224592 3221222820 1077414410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 119064 115901 1111 63 0 119001 0
vsize: 476256
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 122329 0 0 0 22784 219 0 0 25 0 1 0 833505982 513961984 122307 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 125479 122307 1111 63 0 125416 0
vsize: 501916
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 128849 0 0 0 23773 230 0 0 25 0 1 0 833505982 540684288 128827 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 132003 128827 1111 63 0 131940 0
vsize: 528012
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 135456 0 0 0 24762 241 0 0 25 0 1 0 833505982 567713792 135434 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 138602 135434 1111 63 0 138539 0
vsize: 554408
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 142201 0 0 0 25750 253 0 0 25 0 1 0 833505982 595333120 142179 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 145345 142179 1111 63 0 145282 0
vsize: 581380
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 149111 0 0 0 26738 265 0 0 25 0 1 0 833505982 623550464 149089 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 152234 149089 1111 63 0 152171 0
vsize: 608936
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 156142 0 0 0 27726 277 0 0 25 0 1 0 833505982 652369920 156120 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 159270 156120 1111 63 0 159207 0
vsize: 637080
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 163369 0 0 0 28712 291 0 0 25 0 1 0 833505982 682082304 163347 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 166524 163352 1111 63 0 166461 0
vsize: 666096
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 170844 0 0 0 29699 305 0 0 25 0 1 0 833505982 712536064 170822 4294967295 134512640 134714540 3221224592 3221222820 1077414360 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 173959 170822 1111 63 0 173896 0
vsize: 695836
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 178330 0 0 0 30689 315 0 0 25 0 1 0 833505982 743292928 178308 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 181468 178308 1111 63 0 181405 0
vsize: 725872
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 186152 0 0 0 31675 329 0 0 25 0 1 0 833505982 775245824 186130 4294967295 134512640 134714540 3221224592 3221222712 1077378037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 189269 186136 1111 63 0 189206 0
vsize: 757076
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 194127 0 0 0 32661 342 0 0 25 0 1 0 833505982 807940096 194105 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 197251 194105 1111 63 0 197188 0
vsize: 789004
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 202486 0 0 0 33642 358 0 0 25 0 1 0 833505982 842493952 201824 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 205687 201824 1111 63 0 205624 0
vsize: 822748
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 211116 0 0 0 34624 373 0 0 25 0 1 0 833505982 877735936 209398 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 214291 209398 1111 63 0 214228 0
vsize: 857164
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 219910 0 0 0 35600 395 0 0 25 0 1 0 833505982 913715200 216917 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 223075 216917 1111 63 0 223012 0
vsize: 892300
[startup+368.494 s]
Raw data (loadavg): 0.99 0.97 0.96 1/53 8266
Raw data (stat): 8266 (bsolo_mis) R 8265 4613 4612 0 -1 0 219910 0 0 0 35600 395 0 0 25 0 1 0 833505982 913715200 216917 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 223075 216917 1111 63 0 223012 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 368.494
CPU time (s): 368.42
CPU user time (s): 363.843
CPU system time (s): 4.5773
CPU usage (%): 99.98
Max. virtual memory (Kb): 892300
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####