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/MIPLIB/miplib2003/normalized-mps-v2-20-10-stp3d.opb
MD5SUM	bd41ba4f2ddbc80664ba643e2dc93b96
Bench Category	optimization, medium integers (OPTMEDINT)
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	75648
Biggest coefficient in the objective function	100303
Number of bits for the biggest coefficient in the objective function	17
Sum of the numbers in the objective function	7576279200
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	100303
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	7576279200
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	2.74658
Number of variables	204880
Total number of constraints	364368
Number of constraints which are clauses	129232
Number of constraints which are cardinality constraints (but not clauses)	210685
Number of constraints which are nor clauses,nor cardinality constraints	24451
Minimum length of a constraint	1
Maximum length of a constraint	120

Trace number 35236

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-05-28 12:29:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24532 boxname=wulflinc8 idbench=1004 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bd41ba4f2ddbc80664ba643e2dc93b96  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-stp3d.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-stp3d.opb
IDLAUNCH: 24532
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        657320 kB
Buffers:         37480 kB
Cached:         316652 kB
SwapCached:        896 kB
Active:          50564 kB
Inactive:       305824 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        657068 kB
SwapTotal:     2097136 kB
SwapFree:      2095540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5196 kB
Slab:            15140 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 12:33:30 (client local time) WITH STATUS 1 IN 267.027 SECONDS
stats: 24532 7 267.027 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.91 1/54 16114
Raw data (stat): 16114 (runsolver) D 16113 3132 3131 0 -1 64 8 0 0 0 0 0 0 0 18 0 1 0 793020238 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 134 0 0 0 993 3 0 0 25 0 1 0 793020238 1540096 124 4294967295 134512640 135726644 3221224592 3221221792 134574455 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 376 124 300 300 0 76 0
vsize: 1504
[startup+20 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 134 0 0 0 1991 4 0 0 25 0 1 0 793020238 1540096 124 4294967295 134512640 135726644 3221224592 3221221792 134576113 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 376 124 300 300 0 76 0
vsize: 1504
[startup+29.9999 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 2156 0 0 0 2985 10 0 0 25 0 1 0 793020238 7954432 1480 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1942 1480 300 300 0 1642 0
vsize: 7768
[startup+40.0049 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 2684 0 0 0 3983 12 0 0 25 0 1 0 793020238 9306112 2000 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2272 2000 300 300 0 1972 0
vsize: 9088
[startup+50.0082 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 3867 0 0 0 4981 14 0 0 25 0 1 0 793020238 13410304 2471 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3274 2471 300 300 0 2974 0
vsize: 13096
[startup+60.0086 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 4110 0 0 0 5979 15 0 0 25 0 1 0 793020238 14086144 2709 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3439 2709 300 300 0 3139 0
vsize: 13756
[startup+70.0079 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 4366 0 0 0 6978 16 0 0 25 0 1 0 793020238 14761984 2961 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3604 2961 300 300 0 3304 0
vsize: 14416
[startup+80.0086 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 4591 0 0 0 7978 17 0 0 25 0 1 0 793020238 15302656 3182 4294967295 134512640 135726644 3221224592 3221221680 134556179 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3736 3182 300 300 0 3436 0
vsize: 14944
[startup+90.0084 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 4799 0 0 0 8977 18 0 0 25 0 1 0 793020238 15843328 3387 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3868 3387 300 300 0 3568 0
vsize: 15472
[startup+100.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 4995 0 0 0 9976 18 0 0 25 0 1 0 793020238 16384000 3580 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4000 3580 300 300 0 3700 0
vsize: 16000
[startup+110.019 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 5179 0 0 0 10977 19 0 0 25 0 1 0 793020238 16789504 3761 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4099 3761 300 300 0 3799 0
vsize: 16396
[startup+120.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 5353 0 0 0 11977 19 0 0 25 0 1 0 793020238 17330176 3932 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4231 3932 300 300 0 3931 0
vsize: 16924
[startup+130.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 5519 0 0 0 12976 20 0 0 25 0 1 0 793020238 17735680 4095 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4330 4095 300 300 0 4030 0
vsize: 17320
[startup+140.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 7498 0 0 0 13973 23 0 0 25 0 1 0 793020238 25403392 4662 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4662 300 300 0 5902 0
vsize: 24808
[startup+150.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 7553 0 0 0 14973 24 0 0 25 0 1 0 793020238 25403392 4714 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4714 300 300 0 5902 0
vsize: 24808
[startup+160.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 7604 0 0 0 15972 24 0 0 25 0 1 0 793020238 25403392 4763 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4763 300 300 0 5902 0
vsize: 24808
[startup+170.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 7682 0 0 0 16972 24 0 0 25 0 1 0 793020238 25403392 4839 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4839 300 300 0 5902 0
vsize: 24808
[startup+180.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 40896 0 0 0 17897 99 0 0 25 0 1 0 793020238 154558464 32279 4294967295 134512640 135726644 3221224592 3207163632 135279084 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 37734 32279 300 300 0 37434 0
vsize: 150936
[startup+190.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 75745 0 0 0 18819 178 0 0 25 0 1 0 793020238 289660928 52977 4294967295 134512640 135726644 3221224592 3192908776 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 70718 52979 300 300 0 70418 0
vsize: 282872
[startup+200.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 95079 0 0 0 19775 222 0 0 25 0 1 0 793020238 288153600 62680 4294967295 134512640 135726644 3221224592 3217339848 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 70350 62680 300 300 0 70050 0
vsize: 281400
[startup+210.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 126230 0 0 0 20705 292 0 0 25 0 1 0 793020238 402857984 81291 4294967295 134512640 135726644 3221224592 3207180968 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 98354 81292 300 300 0 98054 0
vsize: 393416
[startup+220.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 163713 0 0 0 21630 368 0 0 25 0 1 0 793020238 521744384 99148 4294967295 134512640 135726644 3221224592 3197751272 135280732 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 127379 99148 300 300 0 127079 0
vsize: 509516
[startup+230.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 179166 0 0 0 22595 402 0 0 25 0 1 0 793020238 529043456 114308 4294967295 134512640 135726644 3221224592 3194745852 134604466 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 129161 114308 300 300 0 128861 0
vsize: 516644
[startup+240.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 222306 0 0 0 23493 505 0 0 25 0 1 0 793020238 657281024 132641 4294967295 134512640 135726644 3221224592 3216537080 135280675 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 160469 132643 300 300 0 160169 0
vsize: 641876
[startup+250.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 240558 0 0 0 24448 550 0 0 25 0 1 0 793020238 720842752 150646 4294967295 134512640 135726644 3221224592 3201379768 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 175987 150647 300 300 0 175687 0
vsize: 703948
[startup+260.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 251868 0 0 0 25419 579 0 0 25 0 1 0 793020238 741281792 161538 4294967295 134512640 135726644 3221224592 3221223056 134732747 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 180977 161538 300 300 0 180677 0
vsize: 723908
[startup+267.062 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 16114
Raw data (stat): 16114 (pb2sat) R 16113 3132 3131 0 -1 0 251868 0 0 0 25419 579 0 0 25 0 1 0 793020238 741281792 161538 4294967295 134512640 135726644 3221224592 3221223056 134732747 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 180977 161538 300 300 0 180677 0
vsize: 0

Child status: 1
Real time (s): 267.061
CPU time (s): 267.027
CPU user time (s): 260.906
CPU system time (s): 6.12107
CPU usage (%): 99.9873
Max. virtual memory (Kb): 723908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####