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-momentum3.opb
MD5SUM	fd20bcfe4a71405dc1e0ef3cb894b630
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	87370
Biggest coefficient in the objective function	1310720000
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	13573186735
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	10240000000000000927712935936
Number of bits of the biggest number in a constraint	94
Biggest sum of numbers in a constraint	29801266744107043904416645120
Number of bits of the biggest sum of numbers	95
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.893863
Number of variables	93400
Total number of constraints	70153
Number of constraints which are clauses	6081
Number of constraints which are cardinality constraints (but not clauses)	7185
Number of constraints which are nor clauses,nor cardinality constraints	56887
Minimum length of a constraint	1
Maximum length of a constraint	1018

Trace number 42468

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-06-16 08:18:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25683 boxname=wulflinc2 idbench=983 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fd20bcfe4a71405dc1e0ef3cb894b630  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-momentum3.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-momentum3.opb
IDLAUNCH: 25683
/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:        120892 kB
Buffers:         33444 kB
Cached:         856156 kB
SwapCached:       2016 kB
Active:         327560 kB
Inactive:       564688 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        120640 kB
SwapTotal:     2097136 kB
SwapFree:      2094128 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5056 kB
Slab:            15772 kB
Committed_AS:    71900 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 08:23:45 (client local time) WITH STATUS 1 IN 318.886 SECONDS
stats: 25683 7 318.886 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): 1.09 1.00 0.92 1/54 7848
Raw data (stat): 7848 (runsolver) R 7847 31399 31398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 969268398 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.0013 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 2185 0 0 0 995 4 0 0 25 0 1 0 969268398 7958528 1509 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1943 1509 301 301 0 1642 0
vsize: 7772
[startup+20.0015 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 2711 0 0 0 1993 6 0 0 25 0 1 0 969268398 9445376 2026 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2306 2026 301 301 0 2005 0
vsize: 9224
[startup+30.0022 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 3865 0 0 0 2992 8 0 0 25 0 1 0 969268398 13414400 2469 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3275 2469 301 301 0 2974 0
vsize: 13100
[startup+40.0034 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 4103 0 0 0 3991 9 0 0 25 0 1 0 969268398 13955072 2702 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3407 2702 301 301 0 3106 0
vsize: 13628
[startup+50.0046 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 4361 0 0 0 4990 9 0 0 25 0 1 0 969268398 14630912 2956 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3572 2956 301 301 0 3271 0
vsize: 14288
[startup+60.0043 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 4595 0 0 0 5989 11 0 0 25 0 1 0 969268398 15306752 3186 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3737 3186 301 301 0 3436 0
vsize: 14948
[startup+70.0044 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 4807 0 0 0 6989 12 0 0 25 0 1 0 969268398 15847424 3395 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3869 3395 301 301 0 3568 0
vsize: 15476
[startup+80.0047 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 5004 0 0 0 7988 12 0 0 25 0 1 0 969268398 16388096 3588 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4001 3588 301 301 0 3700 0
vsize: 16004
[startup+90.0044 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 5189 0 0 0 8987 13 0 0 25 0 1 0 969268398 16928768 3770 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4133 3770 301 301 0 3832 0
vsize: 16532
[startup+100.006 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 5363 0 0 0 9987 14 0 0 25 0 1 0 969268398 17334272 3942 4294967295 134512640 135730672 3221224576 3221221664 134561664 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4232 3942 301 301 0 3931 0
vsize: 16928
[startup+110.006 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 7446 0 0 0 10983 18 0 0 25 0 1 0 969268398 25407488 4612 4294967295 134512640 135730672 3221224576 3221221664 134561688 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6203 4612 301 301 0 5902 0
vsize: 24812
[startup+120.006 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 7503 0 0 0 11983 18 0 0 25 0 1 0 969268398 25407488 4666 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6203 4666 301 301 0 5902 0
vsize: 24812
[startup+130.006 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 7557 0 0 0 12982 19 0 0 25 0 1 0 969268398 25407488 4718 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6203 4718 301 301 0 5902 0
vsize: 24812
[startup+140.006 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 7611 0 0 0 13982 19 0 0 25 0 1 0 969268398 25407488 4769 4294967295 134512640 135730672 3221224576 3221221664 134561675 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6203 4769 301 301 0 5902 0
vsize: 24812
[startup+150.007 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 7688 0 0 0 14982 19 0 0 25 0 1 0 969268398 25407488 4844 4294967295 134512640 135730672 3221224576 3221221664 134561656 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6203 4844 301 301 0 5902 0
vsize: 24812
[startup+160.008 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 7746 0 0 0 15982 20 0 0 25 0 1 0 969268398 25542656 4900 4294967295 134512640 135730672 3221224576 3221221664 134561688 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6236 4900 301 301 0 5935 0
vsize: 24944
[startup+170.007 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 7881 0 0 0 16981 20 0 0 25 0 1 0 969268398 25812992 5033 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6302 5033 301 301 0 6001 0
vsize: 25208
[startup+180.007 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 8011 0 0 0 17981 21 0 0 25 0 1 0 969268398 26218496 5161 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6401 5161 301 301 0 6100 0
vsize: 25604
[startup+190.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 8139 0 0 0 18981 21 0 0 25 0 1 0 969268398 26488832 5287 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6467 5287 301 301 0 6166 0
vsize: 25868
[startup+200.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 8264 0 0 0 19981 22 0 0 25 0 1 0 969268398 26894336 5410 4294967295 134512640 135730672 3221224576 3221221664 134561664 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6566 5410 301 301 0 6265 0
vsize: 26264
[startup+210.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 16793 0 0 0 20963 39 0 0 25 0 1 0 969268398 54681600 10091 4294967295 134512640 135730672 3221224576 3221218080 134770673 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 13350 10091 301 301 0 13049 0
vsize: 53400
[startup+220.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 28486 0 0 0 21934 69 0 0 25 0 1 0 969268398 85008384 17054 4294967295 134512640 135730672 3221224576 3220828408 135284889 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 20754 17054 301 301 0 20453 0
vsize: 83016
[startup+230.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 57178 0 0 0 22871 130 0 0 25 0 1 0 969268398 178950144 34529 4294967295 134512640 135730672 3221224576 3220904508 134608033 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 43689 34529 301 301 0 43388 0
vsize: 174756
[startup+240.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 93795 0 0 0 23786 205 0 0 25 0 1 0 969268398 340742144 61235 4294967295 134512640 135730672 3221224576 3220788080 134788517 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 83189 61235 301 301 0 82888 0
vsize: 332756
[startup+250.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 114373 0 0 0 24735 253 0 0 25 0 1 0 969268398 350318592 69298 4294967295 134512640 135730672 3221224576 3220883520 134546591 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 85527 69298 301 301 0 85226 0
vsize: 342108
[startup+260.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 157359 0 0 0 25647 337 0 0 25 0 1 0 969268398 557944832 111103 4294967295 134512640 135730672 3221224576 3220854400 134776110 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 136217 111103 301 301 0 135916 0
vsize: 544868
[startup+270.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 192925 0 0 0 26564 420 0 0 25 0 1 0 969268398 595693568 104506 4294967295 134512640 135730672 3221224576 3220875184 134770727 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 145433 104506 301 301 0 145132 0
vsize: 581732
[startup+280.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 204595 0 0 0 27543 442 0 0 25 0 1 0 969268398 629248000 115969 4294967295 134512640 135730672 3221224576 3220810688 134770721 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 153625 115969 301 301 0 153324 0
vsize: 614500
[startup+290.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 224132 0 0 0 28501 484 0 0 25 0 1 0 969268398 655200256 135271 4294967295 134512640 135730672 3221224576 3220815420 134608058 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 159961 135273 301 301 0 159660 0
vsize: 639844
[startup+300.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 244173 0 0 0 29459 526 0 0 25 0 1 0 969268398 683991040 155081 4294967295 134512640 135730672 3221224576 3220827908 134612202 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 166990 155081 301 301 0 166689 0
vsize: 667960
[startup+310.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 259230 0 0 0 30426 559 0 0 25 0 1 0 969268398 754626560 169622 4294967295 134512640 135730672 3221224576 3221222656 135282225 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 184235 169622 301 301 0 183934 0
vsize: 736940
[startup+319.049 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 7848
Raw data (stat): 7848 (pb2sat-v2) R 7847 31399 31398 0 -1 0 259230 0 0 0 30426 559 0 0 25 0 1 0 969268398 754626560 169622 4294967295 134512640 135730672 3221224576 3221222656 135282225 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 184235 169622 301 301 0 183934 0
vsize: 0

Child status: 1
Real time (s): 319.048
CPU time (s): 318.886
CPU user time (s): 312.936
CPU system time (s): 5.9491
CPU usage (%): 99.949
Max. virtual memory (Kb): 736940
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####