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/unibo/normalized-mps-v2-13-7-rail507.opb
MD5SUM	323cdddd9985e43f8e7199c63ad6de47
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	63209
Biggest coefficient in the objective function	52428800000000000
Number of bits for the biggest coefficient in the objective function	56
Sum of the numbers in the objective function	226433975012582900
Number of bits of the sum of numbers in the objective function	58
Biggest number in a constraint	52428800000000000
Number of bits of the biggest number in a constraint	56
Biggest sum of numbers in a constraint	226433975012582900
Number of bits of the biggest sum of numbers	58
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	295.054
Number of variables	63009
Total number of constraints	63518
Number of constraints which are clauses	507
Number of constraints which are cardinality constraints (but not clauses)	63011
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	59416

Trace number 43033

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-06-16 21:31:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=26253 boxname=wulflinc2 idbench=1553 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  323cdddd9985e43f8e7199c63ad6de47  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-rail507.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-rail507.opb
IDLAUNCH: 26253
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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	: 2
cpu MHz		: 451.191
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:        687952 kB
Buffers:         23292 kB
Cached:         300328 kB
SwapCached:       1420 kB
Active:          37132 kB
Inactive:       288504 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        687700 kB
SwapTotal:     2097136 kB
SwapFree:      2094720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5056 kB
Slab:            15340 kB
Committed_AS:    71900 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 21:37:09 (client local time) WITH STATUS 1 IN 335.633 SECONDS
stats: 26253 7 335.633 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified

	Unexpected exception :
	St9bad_alloc
#### 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.91 0.94 0.90 1/54 16195
Raw data (stat): 16195 (runsolver) R 16194 31399 31398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 974027729 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0006 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 1315 0 0 0 995 4 0 0 25 0 1 0 974027729 5230592 1002 4294967295 134512640 135730672 3221224576 3221221728 134610549 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1277 1002 301 301 0 976 0
vsize: 5108
[startup+20.0009 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 2444 0 0 0 1992 6 0 0 25 0 1 0 974027729 8634368 1765 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2108 1765 301 301 0 1807 0
vsize: 8432
[startup+30.0009 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 3785 0 0 0 2990 8 0 0 25 0 1 0 974027729 13414400 2393 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3275 2393 301 301 0 2974 0
vsize: 13100
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 3934 0 0 0 3989 9 0 0 25 0 1 0 974027729 13549568 2537 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3308 2537 301 301 0 3007 0
vsize: 13232
[startup+50.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 4213 0 0 0 4988 9 0 0 25 0 1 0 974027729 14360576 2811 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3506 2811 301 301 0 3205 0
vsize: 14024
[startup+60.0021 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 4459 0 0 0 5987 10 0 0 25 0 1 0 974027729 14901248 3053 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3638 3053 301 301 0 3337 0
vsize: 14552
[startup+70.0017 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 4676 0 0 0 6986 11 0 0 25 0 1 0 974027729 15577088 3267 4294967295 134512640 135730672 3221224576 3221221888 134568517 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3803 3267 301 301 0 3502 0
vsize: 15212
[startup+80.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 4878 0 0 0 7986 11 0 0 25 0 1 0 974027729 16117760 3465 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3935 3465 301 301 0 3634 0
vsize: 15740
[startup+90.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 5067 0 0 0 8986 11 0 0 25 0 1 0 974027729 16523264 3651 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4034 3651 301 301 0 3733 0
vsize: 16136
[startup+100.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 5247 0 0 0 9985 12 0 0 25 0 1 0 974027729 17063936 3828 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4166 3828 301 301 0 3865 0
vsize: 16664
[startup+110.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 5879 0 0 0 10985 13 0 0 25 0 1 0 974027729 19361792 4458 4294967295 134512640 135730672 3221224576 3221221804 135291220 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4727 4458 301 301 0 4426 0
vsize: 18908
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6099 0 0 0 11982 16 0 0 25 0 1 0 974027729 20705280 4678 4294967295 134512640 135730672 3221224576 3221221664 134561675 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5055 4678 301 301 0 4754 0
vsize: 20220
[startup+130.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6252 0 0 0 12980 17 0 0 25 0 1 0 974027729 21766144 4831 4294967295 134512640 135730672 3221224576 3221221552 134539980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5314 4831 301 301 0 5013 0
vsize: 21256
[startup+140.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6524 0 0 0 13979 19 0 0 25 0 1 0 974027729 22429696 5038 4294967295 134512640 135730672 3221224576 3221221520 134539765 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5476 5038 301 301 0 5175 0
vsize: 21904
[startup+150.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6570 0 0 0 14978 20 0 0 25 0 1 0 974027729 22429696 5084 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5476 5084 301 301 0 5175 0
vsize: 21904
[startup+160.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6852 0 0 0 15977 21 0 0 25 0 1 0 974027729 23494656 5237 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 5736 5237 301 301 0 5435 0
vsize: 22944
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6872 0 0 0 16976 21 0 0 25 0 1 0 974027729 23494656 5257 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5736 5257 301 301 0 5435 0
vsize: 22944
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6889 0 0 0 17976 21 0 0 25 0 1 0 974027729 23494656 5274 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5736 5274 301 301 0 5435 0
vsize: 22944
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6905 0 0 0 18976 21 0 0 25 0 1 0 974027729 23494656 5290 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5736 5290 301 301 0 5435 0
vsize: 22944
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6919 0 0 0 19976 21 0 0 25 0 1 0 974027729 23494656 5304 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5736 5304 301 301 0 5435 0
vsize: 22944
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6932 0 0 0 20976 22 0 0 25 0 1 0 974027729 23494656 5317 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 5736 5317 301 301 0 5435 0
vsize: 22944
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 6945 0 0 0 21976 22 0 0 25 0 1 0 974027729 23494656 5330 4294967295 134512640 135730672 3221224576 3221220908 134637875 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 5736 5330 301 301 0 5435 0
vsize: 22944
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 46891 0 0 0 22886 111 0 0 25 0 1 0 974027729 161357824 30830 4294967295 134512640 135730672 3221224576 3195713236 135282783 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 39394 30832 301 301 0 39093 0
vsize: 157576
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 69784 0 0 0 23832 165 0 0 25 0 1 0 974027729 218845184 47357 4294967295 134512640 135730672 3221224576 3204941376 134786302 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 53429 47358 301 301 0 53128 0
vsize: 213716
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 107171 0 0 0 24753 245 0 0 25 0 1 0 974027729 329220096 62554 4294967295 134512640 135730672 3221224576 3199659104 135284078 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 80376 62554 301 301 0 80075 0
vsize: 321504
[startup+260.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 125431 0 0 0 25705 292 0 0 25 0 1 0 974027729 388456448 80609 4294967295 134512640 135730672 3221224576 3212294520 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 94838 80610 301 301 0 94537 0
vsize: 379352
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 169472 0 0 0 26613 385 0 0 25 0 1 0 974027729 598921216 123457 4294967295 134512640 135730672 3221224576 3201962032 135282752 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 146221 123457 301 301 0 145920 0
vsize: 584884
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 202955 0 0 0 27531 468 0 0 25 0 1 0 974027729 628277248 114790 4294967295 134512640 135730672 3221224576 3194418928 134607963 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 153388 114790 301 301 0 153087 0
vsize: 613552
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 215222 0 0 0 28498 500 0 0 25 0 1 0 974027729 664129536 126861 4294967295 134512640 135730672 3221224576 3212147512 135284564 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 162141 126861 301 301 0 161840 0
vsize: 648564
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 234163 0 0 0 29449 550 0 0 25 0 1 0 974027729 691163136 145574 4294967295 134512640 135730672 3221224576 3201752280 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 168741 145574 301 301 0 168440 0
vsize: 674964
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 252454 0 0 0 30409 590 0 0 25 0 1 0 974027729 768258048 163652 4294967295 134512640 135730672 3221224576 3197384592 134783984 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 187563 163652 301 301 0 187262 0
vsize: 750252
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 268136 0 0 0 31369 627 0 0 25 0 1 0 974027729 790290432 179151 4294967295 134512640 135730672 3221224576 3200047580 134607999 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 192942 179152 301 301 0 192641 0
vsize: 771768
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 271724 0 0 0 32359 635 0 0 25 0 1 0 974027729 793829376 182218 4294967295 134512640 135730672 3221224576 3221222828 135281170 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 193806 182218 301 301 0 193505 0
vsize: 775224
[startup+335.697 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 16195
Raw data (stat): 16195 (pb2sat-v2) R 16194 31399 31398 0 -1 0 271724 0 0 0 32359 635 0 0 25 0 1 0 974027729 793829376 182218 4294967295 134512640 135730672 3221224576 3221222828 135281170 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 193806 182218 301 301 0 193505 0
vsize: 0

Child status: 1
Real time (s): 335.697
CPU time (s): 335.633
CPU user time (s): 328.912
CPU system time (s): 6.72098
CPU usage (%): 99.981
Max. virtual memory (Kb): 775224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####