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 42738

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-06-16 14:14:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25954 boxname=wulflinc5 idbench=1254 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  489cca8508801e1a27a21414584e0af6  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-scsd8.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-scsd8.opb
IDLAUNCH: 25954
/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:        688860 kB
Buffers:         18072 kB
Cached:         304404 kB
SwapCached:        660 kB
Active:          30832 kB
Inactive:       293672 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        688580 kB
SwapTotal:     2097136 kB
SwapFree:      2095536 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5156 kB
Slab:            15644 kB
Committed_AS:    63712 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 14:17:29 (client local time) WITH STATUS 1 IN 179.152 SECONDS
stats: 25954 7 179.152 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.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (runsolver) R 15871 7266 7265 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 971401132 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+9.99992 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 2219 0 0 0 993 6 0 0 25 0 1 0 971401132 8093696 1542 4294967295 134512640 135730672 3221224576 3221221664 134561656 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1976 1542 301 301 0 1675 0
vsize: 7904
[startup+20.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 2714 0 0 0 1991 7 0 0 25 0 1 0 971401132 9445376 2029 4294967295 134512640 135730672 3221224576 3221221664 134561656 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2306 2029 301 301 0 2005 0
vsize: 9224
[startup+30.0004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 3866 0 0 0 2987 12 0 0 25 0 1 0 971401132 13414400 2470 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3275 2470 301 301 0 2974 0
vsize: 13100
[startup+40.0022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 4109 0 0 0 3986 13 0 0 25 0 1 0 971401132 14090240 2708 4294967295 134512640 135730672 3221224576 3221221664 134561675 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3440 2708 301 301 0 3139 0
vsize: 13760
[startup+50.0034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 4371 0 0 0 4984 15 0 0 25 0 1 0 971401132 14766080 2966 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3605 2966 301 301 0 3304 0
vsize: 14420
[startup+60.0027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 4602 0 0 0 5982 17 0 0 25 0 1 0 971401132 15306752 3193 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3737 3193 301 301 0 3436 0
vsize: 14948
[startup+70.0024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 4814 0 0 0 6981 18 0 0 25 0 1 0 971401132 15847424 3401 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3869 3401 301 301 0 3568 0
vsize: 15476
[startup+80.0026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 21829 0 0 0 7945 54 0 0 25 0 1 0 971401132 67690496 13804 4294967295 134512640 135730672 3221224576 3221074624 134786320 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 16526 13804 301 301 0 16225 0
vsize: 66104
[startup+90.0029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 53027 0 0 0 8885 115 0 0 25 0 1 0 971401132 158515200 30957 4294967295 134512640 135730672 3221224576 3221073724 134607984 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 38700 30957 301 301 0 38399 0
vsize: 154800
[startup+100.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 81032 0 0 0 9830 169 0 0 25 0 1 0 971401132 247406592 48861 4294967295 134512640 135730672 3221224576 3221081696 135104805 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 60402 48861 301 301 0 60101 0
vsize: 241608
[startup+110.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 107964 0 0 0 10775 225 0 0 25 0 1 0 971401132 345214976 63290 4294967295 134512640 135730672 3221224576 3221074624 134786278 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 84281 63290 301 301 0 83980 0
vsize: 337124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 135461 0 0 0 11718 282 0 0 25 0 1 0 971401132 529211392 90250 4294967295 134512640 135730672 3221224576 3221074304 134775276 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 129202 90253 301 301 0 128901 0
vsize: 516808
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 163898 0 0 0 12664 336 0 0 25 0 1 0 971401132 488927232 99107 4294967295 134512640 135730672 3221224576 3221076160 134777052 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 119367 99107 301 301 0 119066 0
vsize: 477468
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 199868 0 0 0 13591 410 0 0 25 0 1 0 971401132 591077376 110287 4294967295 134512640 135730672 3221224576 3221078892 135291144 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 144306 110288 301 301 0 144005 0
vsize: 577224
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 216868 0 0 0 14555 446 0 0 25 0 1 0 971401132 649773056 127077 4294967295 134512640 135730672 3221224576 3221073264 135282755 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 158636 127077 301 301 0 158335 0
vsize: 634544
[startup+160.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 236354 0 0 0 15513 488 0 0 25 0 1 0 971401132 678563840 146325 4294967295 134512640 135730672 3221224576 3221078848 134770759 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 165665 146325 301 301 0 165364 0
vsize: 662660
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 253969 0 0 0 16481 520 0 0 25 0 1 0 971401132 707194880 163511 4294967295 134512640 135730672 3221224576 3221222608 135284078 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 172655 163511 301 301 0 172354 0
vsize: 690620
[startup+179.141 s]
Raw data (loadavg): 0.99 0.98 0.92 1/53 15872
Raw data (stat): 15872 (pb2sat-v2) R 15871 7266 7265 0 -1 0 253969 0 0 0 16481 520 0 0 25 0 1 0 971401132 707194880 163511 4294967295 134512640 135730672 3221224576 3221222608 135284078 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 172655 163511 301 301 0 172354 0
vsize: 0

Child status: 1
Real time (s): 179.141
CPU time (s): 179.152
CPU user time (s): 173.611
CPU system time (s): 5.54116
CPU usage (%): 100.006
Max. virtual memory (Kb): 690620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####