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-ship08l.opb
MD5SUM	0a05016ca1456223450d9ec498a510c4
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	85660
Biggest coefficient in the objective function	425249996800
Number of bits for the biggest coefficient in the objective function	39
Sum of the numbers in the objective function	200022778005600
Number of bits of the sum of numbers in the objective function	48
Biggest number in a constraint	425249996800
Number of bits of the biggest number in a constraint	39
Biggest sum of numbers in a constraint	200022778005600
Number of bits of the biggest sum of numbers	48
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.776881
Number of variables	85660
Total number of constraints	712
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	712
Minimum length of a constraint	20
Maximum length of a constraint	1700

Trace number 35533

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-28 13:18:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24792 boxname=wulflinc7 idbench=1264 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0a05016ca1456223450d9ec498a510c4  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ship08l.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ship08l.opb
IDLAUNCH: 24792
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        672156 kB
Buffers:         34740 kB
Cached:         306180 kB
SwapCached:        644 kB
Active:          28552 kB
Inactive:       314392 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        671904 kB
SwapTotal:     2097136 kB
SwapFree:      2095560 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            13812 kB
Committed_AS:    63568 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:23:47 (client local time) WITH STATUS 1 IN 297.986 SECONDS
stats: 24792 7 297.986 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.99 0.99 0.92 1/54 9499
Raw data (stat): 9499 (runsolver) R 9498 24300 24299 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806893353 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.0007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 2179 0 0 0 994 5 0 0 25 0 1 0 806893353 7954432 1504 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1942 1504 300 300 0 1642 0
vsize: 7768
[startup+20.0013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 2694 0 0 0 1992 7 0 0 25 0 1 0 806893353 9306112 2011 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2272 2011 300 300 0 1972 0
vsize: 9088
[startup+30.0019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 3869 0 0 0 2989 10 0 0 25 0 1 0 806893353 13410304 2474 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2474 300 300 0 2974 0
vsize: 13096
[startup+40.0025 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 4117 0 0 0 3988 11 0 0 25 0 1 0 806893353 14086144 2717 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3439 2717 300 300 0 3139 0
vsize: 13756
[startup+50.0022 s]
Raw data (loadavg): 1.07 1.01 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 4381 0 0 0 4988 12 0 0 25 0 1 0 806893353 14761984 2976 4294967295 134512640 135726644 3221224576 3221221664 134556187 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3604 2976 300 300 0 3304 0
vsize: 14416
[startup+60.0025 s]
Raw data (loadavg): 1.06 1.01 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 4613 0 0 0 5987 13 0 0 25 0 1 0 806893353 15302656 3205 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3736 3205 300 300 0 3436 0
vsize: 14944
[startup+70.0024 s]
Raw data (loadavg): 1.05 1.01 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 4825 0 0 0 6986 14 0 0 25 0 1 0 806893353 15978496 3413 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3901 3413 300 300 0 3601 0
vsize: 15604
[startup+80.0034 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 5019 0 0 0 7985 15 0 0 25 0 1 0 806893353 16384000 3604 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4000 3604 300 300 0 3700 0
vsize: 16000
[startup+90.0037 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 5202 0 0 0 8985 16 0 0 25 0 1 0 806893353 16924672 3784 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4132 3784 300 300 0 3832 0
vsize: 16528
[startup+100.003 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 5374 0 0 0 9984 17 0 0 25 0 1 0 806893353 17330176 3953 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4231 3953 300 300 0 3931 0
vsize: 16924
[startup+110.004 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 7448 0 0 0 10980 21 0 0 25 0 1 0 806893353 25403392 4615 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4615 300 300 0 5902 0
vsize: 24808
[startup+120.005 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 7504 0 0 0 11980 21 0 0 25 0 1 0 806893353 25403392 4668 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4668 300 300 0 5902 0
vsize: 24808
[startup+130.005 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 7558 0 0 0 12980 22 0 0 25 0 1 0 806893353 25403392 4720 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4720 300 300 0 5902 0
vsize: 24808
[startup+140.005 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 7609 0 0 0 13979 22 0 0 25 0 1 0 806893353 25403392 4769 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4769 300 300 0 5902 0
vsize: 24808
[startup+150.006 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 7686 0 0 0 14979 23 0 0 25 0 1 0 806893353 25403392 4843 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4843 300 300 0 5902 0
vsize: 24808
[startup+160.006 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 7737 0 0 0 15969 23 0 0 25 0 1 0 806893353 25538560 4892 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6235 4892 300 300 0 5935 0
vsize: 24940
[startup+170.006 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 7871 0 0 0 16968 24 0 0 25 0 1 0 806893353 25808896 5024 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6301 5024 300 300 0 6001 0
vsize: 25204
[startup+180.006 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 7999 0 0 0 17968 24 0 0 25 0 1 0 806893353 26214400 5150 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6400 5150 300 300 0 6100 0
vsize: 25600
[startup+190.007 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 8126 0 0 0 18967 25 0 0 25 0 1 0 806893353 26484736 5275 4294967295 134512640 135726644 3221224576 3221221664 134556195 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6466 5275 300 300 0 6166 0
vsize: 25864
[startup+200.007 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 19691 0 0 0 19941 51 0 0 25 0 1 0 806893353 78323712 16327 4294967295 134512640 135726644 3221224576 3203072112 135280416 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 19122 16327 300 300 0 18822 0
vsize: 76488
[startup+210.007 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 50906 0 0 0 20872 121 0 0 25 0 1 0 806893353 169254912 34751 4294967295 134512640 135726644 3221224576 3191559352 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 41322 34753 300 300 0 41022 0
vsize: 165288
[startup+220.008 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 84957 0 0 0 21800 193 0 0 25 0 1 0 806893353 284766208 52727 4294967295 134512640 135726644 3221224576 3191992928 134554711 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 69523 52729 300 300 0 69223 0
vsize: 278092
[startup+230.009 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 114518 0 0 0 22737 256 0 0 25 0 1 0 806893353 354291712 69730 4294967295 134512640 135726644 3221224576 3187792348 135287531 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 86497 69731 300 300 0 86197 0
vsize: 345988
[startup+240.009 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 155525 0 0 0 23656 338 0 0 25 0 1 0 806893353 589799424 109569 4294967295 134512640 135726644 3221224576 3187171332 135105744 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 143994 109571 300 300 0 143694 0
vsize: 575976
[startup+250.009 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 168499 0 0 0 24627 367 0 0 25 0 1 0 806893353 524173312 103843 4294967295 134512640 135726644 3221224576 3187053064 135280592 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 127972 103843 300 300 0 127672 0
vsize: 511888
[startup+260.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 208923 0 0 0 25535 459 0 0 25 0 1 0 806893353 641744896 119448 4294967295 134512640 135726644 3221224576 3186956184 134785069 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 156676 119448 300 300 0 156376 0
vsize: 626704
[startup+270.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 227641 0 0 0 26494 500 0 0 25 0 1 0 806893353 704835584 137928 4294967295 134512640 135726644 3221224576 3187110400 134780450 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 172079 137928 300 300 0 171779 0
vsize: 688316
[startup+280.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 248591 0 0 0 27450 544 0 0 25 0 1 0 806893353 737435648 158610 4294967295 134512640 135726644 3221224576 3187105280 134782642 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 180038 158610 300 300 0 179738 0
vsize: 720152
[startup+290.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 253153 0 0 0 28441 553 0 0 25 0 1 0 806893353 742748160 162785 4294967295 134512640 135726644 3221224576 3221222800 135280448 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 181335 162785 300 300 0 181035 0
vsize: 725340
[startup+298.052 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 9499
Raw data (stat): 9499 (pb2sat) R 9498 24300 24299 0 -1 0 253153 0 0 0 28441 553 0 0 25 0 1 0 806893353 742748160 162785 4294967295 134512640 135726644 3221224576 3221222800 135280448 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 181335 162785 300 300 0 181035 0
vsize: 0

Child status: 1
Real time (s): 298.052
CPU time (s): 297.986
CPU user time (s): 292.126
CPU system time (s): 5.86011
CPU usage (%): 99.9777
Max. virtual memory (Kb): 725340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####