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/miplib3/normalized-mps-v2-20-10-nw04.opb
MD5SUM	a5c401bba5afccf02c7b40cb1c595b15
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	87482
Biggest coefficient in the objective function	5220
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	120189580
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	5220
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	120189580
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.13683
Number of variables	87482
Total number of constraints	87518
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	87518
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	42032

Trace number 35289

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-05-28 12:38:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24581 boxname=wulflinc17 idbench=1053 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 24581
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 3
cpu MHz		: 451.072
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:        759240 kB
Buffers:         34788 kB
Cached:         209520 kB
SwapCached:        628 kB
Active:          33688 kB
Inactive:       212728 kB
HighTotal:      131008 kB
HighFree:        22400 kB
LowTotal:       903652 kB
LowFree:        736840 kB
SwapTotal:     2097892 kB
SwapFree:      2096376 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5144 kB
Slab:            23040 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 12:43:21 (client local time) WITH STATUS 1 IN 309.957 SECONDS
stats: 24581 7 309.957 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 21116
Raw data (stat): 21116 (runsolver) R 21115 7475 7474 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 864874982 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.0011 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 967 0 0 0 995 4 0 0 25 0 1 0 864874982 4419584 692 4294967295 134512640 135726644 3221224576 3221221340 135297998 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1079 692 300 300 0 779 0
vsize: 4316
[startup+20.002 s]
Raw data (loadavg): 1.08 0.97 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 2367 0 0 0 1992 7 0 0 25 0 1 0 864874982 8495104 1688 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2074 1688 300 300 0 1774 0
vsize: 8296
[startup+30.0012 s]
Raw data (loadavg): 1.06 0.97 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 3772 0 0 0 2989 9 0 0 25 0 1 0 864874982 13410304 2380 4294967295 134512640 135726644 3221224576 3221221664 134556168 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3274 2380 300 300 0 2974 0
vsize: 13096
[startup+40.0017 s]
Raw data (loadavg): 1.05 0.97 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 3904 0 0 0 3989 10 0 0 25 0 1 0 864874982 13410304 2506 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3274 2506 300 300 0 2974 0
vsize: 13096
[startup+50.0017 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 4192 0 0 0 4988 11 0 0 25 0 1 0 864874982 14221312 2790 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3472 2790 300 300 0 3172 0
vsize: 13888
[startup+60.0023 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 4444 0 0 0 5987 11 0 0 25 0 1 0 864874982 14897152 3037 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3637 3037 300 300 0 3337 0
vsize: 14548
[startup+70.0025 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 4666 0 0 0 6986 12 0 0 25 0 1 0 864874982 15437824 3256 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3769 3256 300 300 0 3469 0
vsize: 15076
[startup+80.0024 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 4866 0 0 0 7986 13 0 0 25 0 1 0 864874982 15978496 3453 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3901 3453 300 300 0 3601 0
vsize: 15604
[startup+90.0027 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 5053 0 0 0 8985 14 0 0 25 0 1 0 864874982 16519168 3637 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4033 3637 300 300 0 3733 0
vsize: 16132
[startup+100.002 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 5234 0 0 0 9984 14 0 0 25 0 1 0 864874982 16924672 3815 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4132 3815 300 300 0 3832 0
vsize: 16528
[startup+110.003 s]
Raw data (loadavg): 1.16 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 5405 0 0 0 10983 15 0 0 25 0 1 0 864874982 17465344 3983 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4264 3983 300 300 0 3964 0
vsize: 17056
[startup+120.004 s]
Raw data (loadavg): 1.13 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 7460 0 0 0 11979 19 0 0 25 0 1 0 864874982 25403392 4625 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4625 300 300 0 5902 0
vsize: 24808
[startup+130.003 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 7516 0 0 0 12979 19 0 0 25 0 1 0 864874982 25403392 4679 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4679 300 300 0 5902 0
vsize: 24808
[startup+140.003 s]
Raw data (loadavg): 1.09 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 7570 0 0 0 13979 19 0 0 25 0 1 0 864874982 25403392 4730 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4730 300 300 0 5902 0
vsize: 24808
[startup+150.003 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 7624 0 0 0 14980 20 0 0 25 0 1 0 864874982 25403392 4782 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4782 300 300 0 5902 0
vsize: 24808
[startup+160.004 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 7700 0 0 0 15979 20 0 0 25 0 1 0 864874982 25403392 4856 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4856 300 300 0 5902 0
vsize: 24808
[startup+170.004 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 7777 0 0 0 16979 20 0 0 25 0 1 0 864874982 25538560 4930 4294967295 134512640 135726644 3221224576 3221221664 134556168 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6235 4930 300 300 0 5935 0
vsize: 24940
[startup+180.003 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 7911 0 0 0 17979 20 0 0 25 0 1 0 864874982 25944064 5062 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6334 5062 300 300 0 6034 0
vsize: 25336
[startup+190.004 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 8041 0 0 0 18979 20 0 0 25 0 1 0 864874982 26214400 5190 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6400 5190 300 300 0 6100 0
vsize: 25600
[startup+200.004 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 8168 0 0 0 19979 21 0 0 25 0 1 0 864874982 26619904 5315 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6499 5315 300 300 0 6199 0
vsize: 25996
[startup+210.004 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 8291 0 0 0 20979 21 0 0 25 0 1 0 864874982 26890240 5436 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6565 5436 300 300 0 6265 0
vsize: 26260
[startup+220.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 34668 0 0 0 21919 81 0 0 25 0 1 0 864874982 117391360 26308 4294967295 134512640 135726644 3221224576 3186241528 135280584 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 28660 26310 300 300 0 28360 0
vsize: 114640
[startup+230.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 65687 0 0 0 22852 148 0 0 25 0 1 0 864874982 234983424 49418 4294967295 134512640 135726644 3221224576 3186728592 134784885 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 57369 49422 300 300 0 57069 0
vsize: 229476
[startup+240.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 91714 0 0 0 23796 205 0 0 25 0 1 0 864874982 287453184 59352 4294967295 134512640 135726644 3221224576 3190761680 134782642 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 70179 59353 300 300 0 69879 0
vsize: 280716
[startup+250.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 123217 0 0 0 24723 278 0 0 25 0 1 0 864874982 401887232 78330 4294967295 134512640 135726644 3221224576 3205179764 135277617 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 98117 78330 300 300 0 97817 0
vsize: 392468
[startup+260.006 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 161254 0 0 0 25649 352 0 0 25 0 1 0 864874982 522801152 96756 4294967295 134512640 135726644 3221224576 3211817752 134784091 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 127637 96756 300 300 0 127337 0
vsize: 510548
[startup+270.006 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 176160 0 0 0 26608 393 0 0 25 0 1 0 864874982 526180352 111356 4294967295 134512640 135726644 3221224576 3205220232 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 128462 111357 300 300 0 128162 0
vsize: 513848
[startup+280.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 219452 0 0 0 27514 488 0 0 25 0 1 0 864874982 656986112 129841 4294967295 134512640 135726644 3221224576 3217286880 134783024 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 160397 129842 300 300 0 160097 0
vsize: 641588
[startup+290.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 237451 0 0 0 28472 531 0 0 25 0 1 0 864874982 719060992 147606 4294967295 134512640 135726644 3221224576 3217255000 135280487 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 175552 147606 300 300 0 175252 0
vsize: 702208
[startup+300.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 251055 0 0 0 29440 562 0 0 25 0 1 0 864874982 742141952 161021 4294967295 134512640 135726644 3221224576 3217570528 135139381 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 181187 161021 300 300 0 180887 0
vsize: 724748
[startup+309.938 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 21116
Raw data (stat): 21116 (pb2sat) R 21115 7475 7474 0 -1 0 251055 0 0 0 29440 562 0 0 25 0 1 0 864874982 742141952 161021 4294967295 134512640 135726644 3221224576 3217570528 135139381 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 181187 161021 300 300 0 180887 0
vsize: 0

Child status: 1
Real time (s): 309.937
CPU time (s): 309.957
CPU user time (s): 304.007
CPU system time (s): 5.9501
CPU usage (%): 100.006
Max. virtual memory (Kb): 724748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####