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-scsd8.opb
MD5SUM	489cca8508801e1a27a21414584e0af6
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	55000
Biggest coefficient in the objective function	216169480454144
Number of bits for the biggest coefficient in the objective function	48
Sum of the numbers in the objective function	581831637603140100
Number of bits of the sum of numbers in the objective function	60
Biggest number in a constraint	216169480454144
Number of bits of the biggest number in a constraint	48
Biggest sum of numbers in a constraint	581831637603140100
Number of bits of the biggest sum of numbers	60
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.481926
Number of variables	55000
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	200
Maximum length of a constraint	480

Trace number 35492

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-05-28 13:17:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24782 boxname=wulflinc2 idbench=1254 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  489cca8508801e1a27a21414584e0af6  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-scsd8.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-scsd8.opb
IDLAUNCH: 24782
/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:        692476 kB
Buffers:         37436 kB
Cached:         281480 kB
SwapCached:        820 kB
Active:          25112 kB
Inactive:       296016 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        692224 kB
SwapTotal:     2097136 kB
SwapFree:      2095480 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5340 kB
Slab:            15272 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:20:35 (client local time) WITH STATUS 1 IN 182.548 SECONDS
stats: 24782 7 182.548 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.90 2/54 11965
Raw data (stat): 11965 (runsolver) R 11964 31399 31398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806880530 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.0005 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 2184 0 0 0 993 6 0 0 25 0 1 0 806880530 7954432 1509 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1942 1509 300 300 0 1642 0
vsize: 7768
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 2709 0 0 0 1992 7 0 0 25 0 1 0 806880530 9441280 2026 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2305 2026 300 300 0 2005 0
vsize: 9220
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 3868 0 0 0 2991 8 0 0 25 0 1 0 806880530 13410304 2473 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3274 2473 300 300 0 2974 0
vsize: 13096
[startup+40.0026 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 4103 0 0 0 3990 9 0 0 25 0 1 0 806880530 13950976 2703 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3406 2703 300 300 0 3106 0
vsize: 13624
[startup+50.0029 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 4358 0 0 0 4988 10 0 0 25 0 1 0 806880530 14626816 2954 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3571 2954 300 300 0 3271 0
vsize: 14284
[startup+60.0029 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 4588 0 0 0 5988 11 0 0 25 0 1 0 806880530 15302656 3180 4294967295 134512640 135726644 3221224592 3221221792 134576102 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3736 3180 300 300 0 3436 0
vsize: 14944
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 4797 0 0 0 6987 12 0 0 25 0 1 0 806880530 15843328 3386 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3868 3386 300 300 0 3568 0
vsize: 15472
[startup+80.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 26001 0 0 0 7939 59 0 0 25 0 1 0 806880530 86564864 17978 4294967295 134512640 135726644 3221224592 3200539472 134560326 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 21134 17979 300 300 0 20834 0
vsize: 84536
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 55515 0 0 0 8875 124 0 0 25 0 1 0 806880530 207163392 39335 4294967295 134512640 135726644 3221224592 3199439408 134784885 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 50577 39339 300 300 0 50277 0
vsize: 202308
[startup+100.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 85345 0 0 0 9815 185 0 0 25 0 1 0 806880530 270987264 53103 4294967295 134512640 135726644 3221224592 3199620464 135284693 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 66159 53104 300 300 0 65859 0
vsize: 264636
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 112258 0 0 0 10758 242 0 0 25 0 1 0 806880530 368525312 67508 4294967295 134512640 135726644 3221224592 3199363372 135287576 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 89972 67508 300 300 0 89672 0
vsize: 359888
[startup+120.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 142294 0 0 0 11697 303 0 0 25 0 1 0 806880530 556957696 96912 4294967295 134512640 135726644 3221224592 3199333176 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 135976 96915 300 300 0 135676 0
vsize: 543904
[startup+130.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 168798 0 0 0 12641 358 0 0 25 0 1 0 806880530 513093632 104197 4294967295 134512640 135726644 3221224592 3199371796 134608834 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 125267 104197 300 300 0 124967 0
vsize: 501068
[startup+140.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 205351 0 0 0 13563 436 0 0 25 0 1 0 806880530 616730624 115956 4294967295 134512640 135726644 3221224592 3199296108 134604415 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 150569 115956 300 300 0 150269 0
vsize: 602276
[startup+150.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 222287 0 0 0 14529 471 0 0 25 0 1 0 806880530 675020800 132693 4294967295 134512640 135726644 3221224592 3199385744 134554681 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 164800 132693 300 300 0 164500 0
vsize: 659200
[startup+160.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 242540 0 0 0 15483 516 0 0 25 0 1 0 806880530 705703936 152694 4294967295 134512640 135726644 3221224592 3199760608 134784525 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 172291 152695 300 300 0 171991 0
vsize: 689164
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 258815 0 0 0 16452 548 0 0 25 0 1 0 806880530 733380608 168782 4294967295 134512640 135726644 3221224592 3203213328 135139496 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 179048 168782 300 300 0 178748 0
vsize: 716192
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 258817 0 0 0 17439 561 0 0 25 0 1 0 806880530 421937152 102593 4294967295 134512640 135726644 3221224592 3221222780 135277480 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 103012 102593 300 300 0 102712 0
vsize: 412048
[startup+182.544 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 11965
Raw data (stat): 11965 (pb2sat) R 11964 31399 31398 0 -1 0 258817 0 0 0 17439 561 0 0 25 0 1 0 806880530 421937152 102593 4294967295 134512640 135726644 3221224592 3221222780 135277480 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 103012 102593 300 300 0 102712 0
vsize: 0

Child status: 1
Real time (s): 182.544
CPU time (s): 182.548
CPU user time (s): 176.723
CPU system time (s): 5.82511
CPU usage (%): 100.002
Max. virtual memory (Kb): 716192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####