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-d2q06c.opb
MD5SUM	8e2638ad794b39b950927d7f3192369b
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	59780
Biggest coefficient in the objective function	35431356301312
Number of bits for the biggest coefficient in the objective function	46
Sum of the numbers in the objective function	17025894421914675
Number of bits of the sum of numbers in the objective function	54
Biggest number in a constraint	1217763488038912
Number of bits of the biggest number in a constraint	51
Biggest sum of numbers in a constraint	17025894421914675
Number of bits of the biggest sum of numbers	54
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.942855
Number of variables	103340
Total number of constraints	2171
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	2171
Minimum length of a constraint	20
Maximum length of a constraint	2180

Trace number 35435

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-05-28 13:10:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24733 boxname=wulflinc2 idbench=1205 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8e2638ad794b39b950927d7f3192369b  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-d2q06c.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-d2q06c.opb
IDLAUNCH: 24733
/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:        694904 kB
Buffers:         37388 kB
Cached:         279012 kB
SwapCached:        820 kB
Active:          33436 kB
Inactive:       285140 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        694624 kB
SwapTotal:     2097136 kB
SwapFree:      2095480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5340 kB
Slab:            15508 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:13:20 (client local time) WITH STATUS 1 IN 199.523 SECONDS
stats: 24733 7 199.523 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.93 0.90 2/54 11686
Raw data (stat): 11686 (runsolver) R 11685 31399 31398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806835341 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0009 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 2254 0 0 0 994 5 0 0 25 0 1 0 806835341 8224768 1576 4294967295 134512640 135726644 3221224592 3221221536 134541148 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2008 1576 300 300 0 1708 0
vsize: 8032
[startup+20.002 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 2753 0 0 0 1993 6 0 0 25 0 1 0 806835341 9441280 2067 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2305 2067 300 300 0 2005 0
vsize: 9220
[startup+30.0028 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 3882 0 0 0 2990 9 0 0 25 0 1 0 806835341 13410304 2484 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2484 300 300 0 2974 0
vsize: 13096
[startup+40.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 4125 0 0 0 3990 10 0 0 25 0 1 0 806835341 14086144 2723 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3439 2723 300 300 0 3139 0
vsize: 13756
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 4377 0 0 0 4989 11 0 0 25 0 1 0 806835341 14761984 2971 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3604 2971 300 300 0 3304 0
vsize: 14416
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 4604 0 0 0 5988 12 0 0 25 0 1 0 806835341 15302656 3194 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3736 3194 300 300 0 3436 0
vsize: 14944
[startup+70.0041 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 4811 0 0 0 6987 12 0 0 25 0 1 0 806835341 15843328 3398 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3868 3398 300 300 0 3568 0
vsize: 15472
[startup+80.0132 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 5006 0 0 0 7987 14 0 0 25 0 1 0 806835341 16384000 3589 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4000 3589 300 300 0 3700 0
vsize: 16000
[startup+90.0137 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 5648 0 0 0 8986 15 0 0 25 0 1 0 806835341 18817024 4229 4294967295 134512640 135726644 3221224592 3221220812 135287512 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4594 4229 300 300 0 4294 0
vsize: 18376
[startup+100.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 44158 0 0 0 9905 96 0 0 25 0 1 0 806835341 152354816 28190 4294967295 134512640 135726644 3221224592 3197294816 134780450 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 37196 28190 300 300 0 36896 0
vsize: 148784
[startup+110.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 72571 0 0 0 10847 154 0 0 25 0 1 0 806835341 294428672 50054 4294967295 134512640 135726644 3221224592 3197296140 135297998 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 71882 50054 300 300 0 71582 0
vsize: 287528
[startup+120.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 105380 0 0 0 11780 221 0 0 25 0 1 0 806835341 326881280 60823 4294967295 134512640 135726644 3221224592 3197300544 134554559 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 79805 60823 300 300 0 79505 0
vsize: 319220
[startup+130.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 124904 0 0 0 12743 259 0 0 25 0 1 0 806835341 390098944 80114 4294967295 134512640 135726644 3221224592 3197308848 134766504 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 95239 80114 300 300 0 94939 0
vsize: 380956
[startup+140.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 164004 0 0 0 13668 333 0 0 25 0 1 0 806835341 518352896 99629 4294967295 134512640 135726644 3221224592 3197310496 134782645 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 126551 99629 300 300 0 126251 0
vsize: 506204
[startup+150.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 199626 0 0 0 14594 408 0 0 25 0 1 0 806835341 619016192 110465 4294967295 134512640 135726644 3221224592 3197308844 135298010 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 151127 110465 300 300 0 150827 0
vsize: 604508
[startup+160.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 214070 0 0 0 15564 438 0 0 25 0 1 0 806835341 666116096 124697 4294967295 134512640 135726644 3221224592 3197316832 134766470 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 162626 124697 300 300 0 162326 0
vsize: 650504
[startup+170.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 234364 0 0 0 16527 475 0 0 25 0 1 0 806835341 696983552 144750 4294967295 134512640 135726644 3221224592 3197330944 134554566 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 170162 144750 300 300 0 169862 0
vsize: 680648
[startup+180.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 254720 0 0 0 17486 516 0 0 25 0 1 0 806835341 727752704 164862 4294967295 134512640 135726644 3221224592 3197308444 135105707 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 177674 164862 300 300 0 177374 0
vsize: 710696
[startup+190.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 261676 0 0 0 18473 529 0 0 25 0 1 0 806835341 738107392 171504 4294967295 134512640 135726644 3221224592 3221222652 134604368 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 180202 171504 300 300 0 179902 0
vsize: 720808
[startup+199.509 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 11686
Raw data (stat): 11686 (pb2sat) R 11685 31399 31398 0 -1 0 261676 0 0 0 18473 529 0 0 25 0 1 0 806835341 738107392 171504 4294967295 134512640 135726644 3221224592 3221222652 134604368 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 180202 171504 300 300 0 179902 0
vsize: 0

Child status: 1
Real time (s): 199.508
CPU time (s): 199.523
CPU user time (s): 193.869
CPU system time (s): 5.65414
CPU usage (%): 100.007
Max. virtual memory (Kb): 720808
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####