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-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-scsd8.opb
MD5SUM	63dde7c8c3b02bd89e3e065c5bd58b69
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	82500
Biggest coefficient in the objective function	221357547985043456
Number of bits for the biggest coefficient in the objective function	58
Sum of the numbers in the objective function	595796164546237562880
Number of bits of the sum of numbers in the objective function	70
Biggest number in a constraint	221357547985043456
Number of bits of the biggest number in a constraint	58
Biggest sum of numbers in a constraint	595796164546237562880
Number of bits of the biggest sum of numbers	70
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.744886
Number of variables	82500
Total number of constraints	397
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	397
Minimum length of a constraint	300
Maximum length of a constraint	720

Trace number 35113

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-28 12:12:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24398 boxname=wulflinc10 idbench=870 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  63dde7c8c3b02bd89e3e065c5bd58b69  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-scsd8.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-scsd8.opb
IDLAUNCH: 24398
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        814016 kB
Buffers:         34732 kB
Cached:         164016 kB
SwapCached:         84 kB
Active:          84436 kB
Inactive:       116944 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        813764 kB
SwapTotal:     2097136 kB
SwapFree:      2096728 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5880 kB
Slab:            13644 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 12:17:37 (client local time) WITH STATUS 1 IN 295.02 SECONDS
stats: 24398 7 295.02 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.98 0.94 0.91 1/54 22596
Raw data (stat): 22596 (runsolver) R 22595 15547 15546 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806501950 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.002 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 2167 0 0 0 995 4 0 0 25 0 1 0 806501950 7954432 1491 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1942 1491 300 300 0 1642 0
vsize: 7768
[startup+20.0032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 2690 0 0 0 1993 6 0 0 25 0 1 0 806501950 9306112 2006 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2272 2006 300 300 0 1972 0
vsize: 9088
[startup+30.0023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 3859 0 0 0 2990 9 0 0 25 0 1 0 806501950 13410304 2463 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2463 300 300 0 2974 0
vsize: 13096
[startup+40.0029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 4100 0 0 0 3989 10 0 0 25 0 1 0 806501950 13950976 2699 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3406 2699 300 300 0 3106 0
vsize: 13624
[startup+50.0028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 4361 0 0 0 4988 11 0 0 25 0 1 0 806501950 14626816 2956 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3571 2956 300 300 0 3271 0
vsize: 14284
[startup+60.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 4592 0 0 0 5988 11 0 0 25 0 1 0 806501950 15302656 3183 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3736 3183 300 300 0 3436 0
vsize: 14944
[startup+70.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 4803 0 0 0 6987 12 0 0 25 0 1 0 806501950 15843328 3391 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3868 3391 300 300 0 3568 0
vsize: 15472
[startup+80.0034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 4997 0 0 0 7987 13 0 0 25 0 1 0 806501950 16384000 3582 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4000 3582 300 300 0 3700 0
vsize: 16000
[startup+90.0041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 5179 0 0 0 8986 14 0 0 25 0 1 0 806501950 16789504 3761 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4099 3761 300 300 0 3799 0
vsize: 16396
[startup+100.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 5352 0 0 0 9985 14 0 0 25 0 1 0 806501950 17330176 3931 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4231 3931 300 300 0 3931 0
vsize: 16924
[startup+110.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 5517 0 0 0 10985 15 0 0 25 0 1 0 806501950 17735680 4093 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4330 4093 300 300 0 4030 0
vsize: 17320
[startup+120.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 7501 0 0 0 11980 20 0 0 25 0 1 0 806501950 25403392 4665 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4665 300 300 0 5902 0
vsize: 24808
[startup+130.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 7554 0 0 0 12980 20 0 0 25 0 1 0 806501950 25403392 4715 4294967295 134512640 135726644 3221224576 3221221664 134556168 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4715 300 300 0 5902 0
vsize: 24808
[startup+140.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 7607 0 0 0 13980 20 0 0 25 0 1 0 806501950 25403392 4766 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4766 300 300 0 5902 0
vsize: 24808
[startup+150.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 7679 0 0 0 14981 20 0 0 25 0 1 0 806501950 25538560 4836 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6235 4836 300 300 0 5935 0
vsize: 24940
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 7729 0 0 0 15980 21 0 0 25 0 1 0 806501950 25538560 4883 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6235 4883 300 300 0 5935 0
vsize: 24940
[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 7855 0 0 0 16979 22 0 0 25 0 1 0 806501950 25808896 5007 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6301 5007 300 300 0 6001 0
vsize: 25204
[startup+180.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 7986 0 0 0 17979 22 0 0 25 0 1 0 806501950 26079232 5136 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6367 5136 300 300 0 6067 0
vsize: 25468
[startup+190.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 32297 0 0 0 18922 79 0 0 25 0 1 0 806501950 107466752 23966 4294967295 134512640 135726644 3221224576 3188686552 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 26237 23966 300 300 0 25937 0
vsize: 104948
[startup+200.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 59184 0 0 0 19864 137 0 0 25 0 1 0 806501950 228306944 42951 4294967295 134512640 135726644 3221224576 3188473392 134784885 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 55739 42955 300 300 0 55439 0
vsize: 222956
[startup+210.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 89273 0 0 0 20798 203 0 0 25 0 1 0 806501950 284561408 56982 4294967295 134512640 135726644 3221224576 3188247896 134603585 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 69473 56983 300 300 0 69173 0
vsize: 277892
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 117794 0 0 0 21735 267 0 0 25 0 1 0 806501950 388857856 72999 4294967295 134512640 135726644 3221224576 3188850000 134780435 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 94936 72999 300 300 0 94636 0
vsize: 379744
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 157556 0 0 0 22658 344 0 0 25 0 1 0 806501950 589860864 111687 4294967295 134512640 135726644 3221224576 3188479160 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 144009 111690 300 300 0 143709 0
vsize: 576036
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 172245 0 0 0 23625 377 0 0 25 0 1 0 806501950 527749120 107623 4294967295 134512640 135726644 3221224576 3189053728 134554698 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 128845 107623 300 300 0 128545 0
vsize: 515380
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 209076 0 0 0 24542 460 0 0 25 0 1 0 806501950 633819136 119676 4294967295 134512640 135726644 3221224576 3188218464 134767123 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 154741 119676 300 300 0 154441 0
vsize: 618964
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 225625 0 0 0 25508 495 0 0 25 0 1 0 806501950 691298304 136035 4294967295 134512640 135726644 3221224576 3188344800 135284860 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 168774 136035 300 300 0 168474 0
vsize: 675096
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 245877 0 0 0 26464 538 0 0 25 0 1 0 806501950 722116608 156037 4294967295 134512640 135726644 3221224576 3188617280 134783265 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 176298 156038 300 300 0 175998 0
vsize: 705192
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 261844 0 0 0 27428 575 0 0 25 0 1 0 806501950 747225088 171810 4294967295 134512640 135726644 3221224576 3190539856 135133201 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 182428 171810 300 300 0 182128 0
vsize: 729712
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 261846 0 0 0 28415 588 0 0 25 0 1 0 806501950 434733056 105696 4294967295 134512640 135726644 3221224576 3221222764 135277480 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 106136 105696 300 300 0 105836 0
vsize: 424544
[startup+295 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 22596
Raw data (stat): 22596 (pb2sat) R 22595 15547 15546 0 -1 0 261846 0 0 0 28415 588 0 0 25 0 1 0 806501950 434733056 105696 4294967295 134512640 135726644 3221224576 3221222764 135277480 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 106136 105696 300 300 0 105836 0
vsize: 0

Child status: 1
Real time (s): 294.999
CPU time (s): 295.02
CPU user time (s): 288.917
CPU system time (s): 6.10307
CPU usage (%): 100.007
Max. virtual memory (Kb): 729712
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####