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/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-dc1c.opb
MD5SUM	bd6d0785955b31f4cbdede5ce3d2b1e9
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	58150
Biggest coefficient in the objective function	536870912000000000000
Number of bits for the biggest coefficient in the objective function	69
Sum of the numbers in the objective function	6807821537690881359872
Number of bits of the sum of numbers in the objective function	73
Biggest number in a constraint	536870912000000000000
Number of bits of the biggest number in a constraint	69
Biggest sum of numbers in a constraint	6808845537690881359872
Number of bits of the biggest sum of numbers	73
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1305.36
Number of variables	58150
Total number of constraints	10029
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	8381
Number of constraints which are nor clauses,nor cardinality constraints	1648
Minimum length of a constraint	1
Maximum length of a constraint	58150

Trace number 42641

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-06-16 13:15:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25860 boxname=wulflinc6 idbench=1160 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bd6d0785955b31f4cbdede5ce3d2b1e9  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-dc1c.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-dc1c.opb
IDLAUNCH: 25860
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        705968 kB
Buffers:         25748 kB
Cached:         279592 kB
SwapCached:       1000 kB
Active:          32464 kB
Inactive:       275084 kB
HighTotal:      131008 kB
HighFree:        22036 kB
LowTotal:       903652 kB
LowFree:        683932 kB
SwapTotal:     2097136 kB
SwapFree:      2095200 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5092 kB
Slab:            15320 kB
Committed_AS:    63848 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 13:18:43 (client local time) WITH STATUS 1 IN 184.439 SECONDS
stats: 25860 7 184.439 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.92 0.95 0.91 2/54 20139
Raw data (stat): 20139 (runsolver) R 20138 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 971046941 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.0003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 2167 0 0 0 992 7 0 0 25 0 1 0 971046941 7958528 1492 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1943 1492 301 301 0 1642 0
vsize: 7772
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 2679 0 0 0 1990 9 0 0 25 0 1 0 971046941 9310208 1996 4294967295 134512640 135730672 3221224576 3221221664 134561664 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2273 1996 301 301 0 1972 0
vsize: 9092
[startup+30 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 3847 0 0 0 2988 11 0 0 25 0 1 0 971046941 13414400 2452 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3275 2452 301 301 0 2974 0
vsize: 13100
[startup+39.9997 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 4069 0 0 0 3987 13 0 0 25 0 1 0 971046941 13955072 2669 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3407 2669 301 301 0 3106 0
vsize: 13628
[startup+49.9998 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 4320 0 0 0 4986 14 0 0 25 0 1 0 971046941 14630912 2916 4294967295 134512640 135730672 3221224576 3221221664 134561688 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3572 2916 301 301 0 3271 0
vsize: 14288
[startup+59.9994 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 4546 0 0 0 5985 15 0 0 25 0 1 0 971046941 15171584 3139 4294967295 134512640 135730672 3221224576 3221221664 134561656 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3704 3139 301 301 0 3403 0
vsize: 14816
[startup+69.9991 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 4758 0 0 0 6985 15 0 0 25 0 1 0 971046941 15712256 3347 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3836 3347 301 301 0 3535 0
vsize: 15344
[startup+79.9993 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 4958 0 0 0 7984 16 0 0 25 0 1 0 971046941 16252928 3544 4294967295 134512640 135730672 3221224576 3221221664 134561664 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3968 3544 301 301 0 3667 0
vsize: 15872
[startup+89.999 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 12610 0 0 0 8966 35 0 0 25 0 1 0 971046941 37826560 8488 4294967295 134512640 135730672 3221224576 3221201696 134770057 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9235 8488 301 301 0 8934 0
vsize: 36940
[startup+99.9987 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 47379 0 0 0 9882 118 0 0 25 0 1 0 971046941 141869056 25369 4294967295 134512640 135730672 3221224576 3221210988 135301637 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 34636 25369 301 301 0 34335 0
vsize: 138544
[startup+109.999 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 75519 0 0 0 10822 179 0 0 25 0 1 0 971046941 224899072 44086 4294967295 134512640 135730672 3221224576 3221211512 135284293 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 54907 44086 301 301 0 54606 0
vsize: 219628
[startup+119.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 100532 0 0 0 11764 237 0 0 25 0 1 0 971046941 308797440 56581 4294967295 134512640 135730672 3221224576 3221117912 135284287 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 75390 56581 301 301 0 75089 0
vsize: 301560
[startup+129.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 118055 0 0 0 12723 278 0 0 25 0 1 0 971046941 322891776 73853 4294967295 134512640 135730672 3221224576 3221220940 134540202 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 78831 73853 301 301 0 78530 0
vsize: 315324
[startup+139.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 178100 0 0 0 13598 403 0 0 25 0 1 0 971046941 540819456 90783 4294967295 134512640 135730672 3221224576 3221167004 134608033 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 132036 90783 301 301 0 131735 0
vsize: 528144
[startup+149.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 190441 0 0 0 14571 430 0 0 25 0 1 0 971046941 574373888 102903 4294967295 134512640 135730672 3221224576 3221191216 134610086 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 140228 102903 301 301 0 139927 0
vsize: 560912
[startup+159.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 205082 0 0 0 15536 465 0 0 25 0 1 0 971046941 574373888 117282 4294967295 134512640 135730672 3221224576 3221197116 134785989 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 140228 117282 301 301 0 139927 0
vsize: 560912
[startup+169.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 219419 0 0 0 16502 500 0 0 25 0 1 0 971046941 633221120 131399 4294967295 134512640 135730672 3221224576 3221202176 134784086 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 154595 131399 301 301 0 154294 0
vsize: 618380
[startup+179.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 242205 0 0 0 17449 553 0 0 25 0 1 0 971046941 646500352 146555 4294967295 134512640 135730672 3221224576 3221223040 134736337 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 157837 146555 301 301 0 157536 0
vsize: 631348
[startup+184.409 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 20139
Raw data (stat): 20139 (pb2sat-v2) R 20138 25568 25567 0 -1 0 242205 0 0 0 17449 553 0 0 25 0 1 0 971046941 646500352 146555 4294967295 134512640 135730672 3221224576 3221223040 134736337 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 157837 146555 301 301 0 157536 0
vsize: 0

Child status: 1
Real time (s): 184.409
CPU time (s): 184.439
CPU user time (s): 178.609
CPU system time (s): 5.83011
CPU usage (%): 100.016
Max. virtual memory (Kb): 631348
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####