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-dc1l.opb
MD5SUM	4d1c8086316d85cb5ef2a3148b52a8a1
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	85408
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	6807849934732110331904
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	6807849934732110331904
Number of bits of the biggest sum of numbers	73
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.91486
Number of variables	85198
Total number of constraints	37291
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	35639
Number of constraints which are nor clauses,nor cardinality constraints	1652
Minimum length of a constraint	1
Maximum length of a constraint	35129

Trace number 35403

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-28 13:03:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24689 boxname=wulflinc15 idbench=1161 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4d1c8086316d85cb5ef2a3148b52a8a1  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-dc1l.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-dc1l.opb
IDLAUNCH: 24689
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        753344 kB
Buffers:         33492 kB
Cached:         224916 kB
SwapCached:        604 kB
Active:          71340 kB
Inactive:       189136 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        753092 kB
SwapTotal:     2097136 kB
SwapFree:      2095616 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5120 kB
Slab:            15296 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:08:24 (client local time) WITH STATUS 1 IN 308.928 SECONDS
stats: 24689 7 308.928 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.93 0.96 0.91 2/54 3489
Raw data (stat): 3489 (runsolver) R 3488 23514 23513 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806785155 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.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 1984 0 0 0 994 5 0 0 25 0 1 0 806785155 7413760 1311 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1810 1311 300 300 0 1510 0
vsize: 7240
[startup+20.0023 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 2586 0 0 0 1992 7 0 0 25 0 1 0 806785155 9035776 1904 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2206 1904 300 300 0 1906 0
vsize: 8824
[startup+30.0013 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 3829 0 0 0 2989 10 0 0 25 0 1 0 806785155 13410304 2434 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2434 300 300 0 2974 0
vsize: 13096
[startup+40.0087 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 4040 0 0 0 3989 11 0 0 25 0 1 0 806785155 13815808 2640 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3373 2640 300 300 0 3073 0
vsize: 13492
[startup+50.0094 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 4302 0 0 0 4988 12 0 0 25 0 1 0 806785155 14491648 2898 4294967295 134512640 135726644 3221224576 3221221888 134565361 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3538 2898 300 300 0 3238 0
vsize: 14152
[startup+60.0098 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 4534 0 0 0 5988 12 0 0 25 0 1 0 806785155 15167488 3126 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3703 3126 300 300 0 3403 0
vsize: 14812
[startup+70.0101 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 4748 0 0 0 6987 13 0 0 25 0 1 0 806785155 15708160 3337 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3835 3337 300 300 0 3535 0
vsize: 15340
[startup+80.0102 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 4946 0 0 0 7987 14 0 0 25 0 1 0 806785155 16248832 3531 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3967 3531 300 300 0 3667 0
vsize: 15868
[startup+90.0103 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 5133 0 0 0 8986 15 0 0 25 0 1 0 806785155 16789504 3715 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4099 3715 300 300 0 3799 0
vsize: 16396
[startup+100.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 5311 0 0 0 9986 15 0 0 25 0 1 0 806785155 17195008 3890 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4198 3890 300 300 0 3898 0
vsize: 16792
[startup+110.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 5479 0 0 0 10985 16 0 0 25 0 1 0 806785155 17600512 4056 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4297 4056 300 300 0 3997 0
vsize: 17188
[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 7486 0 0 0 11981 20 0 0 25 0 1 0 806785155 25403392 4650 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4650 300 300 0 5902 0
vsize: 24808
[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3489
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 7541 0 0 0 12981 20 0 0 25 0 1 0 806785155 25403392 4703 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4703 300 300 0 5902 0
vsize: 24808
[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 7594 0 0 0 13980 21 0 0 25 0 1 0 806785155 25403392 4753 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4753 300 300 0 5902 0
vsize: 24808
[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 7670 0 0 0 14980 22 0 0 25 0 1 0 806785155 25403392 4827 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4827 300 300 0 5902 0
vsize: 24808
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 7721 0 0 0 15979 22 0 0 25 0 1 0 806785155 25403392 4876 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4876 300 300 0 5902 0
vsize: 24808
[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 7834 0 0 0 16979 23 0 0 25 0 1 0 806785155 25673728 4987 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6268 4987 300 300 0 5968 0
vsize: 25072
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 7967 0 0 0 17978 24 0 0 25 0 1 0 806785155 26079232 5117 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6367 5117 300 300 0 6067 0
vsize: 25468
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 8095 0 0 0 18977 24 0 0 25 0 1 0 806785155 26484736 5243 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6466 5243 300 300 0 6166 0
vsize: 25864
[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 10714 0 0 0 19972 30 0 0 25 0 1 0 806785155 36052992 7801 4294967295 134512640 135726644 3221224576 3216715752 134772595 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8803 7803 300 300 0 8503 0
vsize: 35208
[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 48643 0 0 0 20887 116 0 0 25 0 1 0 806785155 166682624 32537 4294967295 134512640 135726644 3221224576 3187197712 134554799 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 40694 32537 300 300 0 40394 0
vsize: 162776
[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 84784 0 0 0 21815 188 0 0 25 0 1 0 806785155 321970176 61828 4294967295 134512640 135726644 3221224576 3187994160 134772474 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 78606 61828 300 300 0 78306 0
vsize: 314424
[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 110484 0 0 0 22758 245 0 0 25 0 1 0 806785155 343609344 65809 4294967295 134512640 135726644 3221224576 3188785984 135280475 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 83889 65811 300 300 0 83589 0
vsize: 335556
[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 129559 0 0 0 23721 282 0 0 25 0 1 0 806785155 404873216 84661 4294967295 134512640 135726644 3221224576 3188136064 134767231 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 98846 84662 300 300 0 98546 0
vsize: 395384
[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 169407 0 0 0 24644 359 0 0 25 0 1 0 806785155 533626880 104914 4294967295 134512640 135726644 3221224576 3187784968 134783921 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 130280 104915 300 300 0 129980 0
vsize: 521120
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 205437 0 0 0 25565 439 0 0 25 0 1 0 806785155 634290176 116156 4294967295 134512640 135726644 3221224576 3187317352 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 154856 116156 300 300 0 154556 0
vsize: 619424
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 220206 0 0 0 26535 468 0 0 25 0 1 0 806785155 681631744 130721 4294967295 134512640 135726644 3221224576 3187990640 134559731 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 166414 130721 300 300 0 166114 0
vsize: 665656
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 240061 0 0 0 27497 507 0 0 25 0 1 0 806785155 710152192 150347 4294967295 134512640 135726644 3221224576 3187934456 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 173377 150348 300 300 0 173077 0
vsize: 693508
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 259985 0 0 0 28453 551 0 0 25 0 1 0 806785155 738537472 170042 4294967295 134512640 135726644 3221224576 3187162928 134554691 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 180307 170042 300 300 0 180007 0
vsize: 721228
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 267786 0 0 0 29435 569 0 0 25 0 1 0 806785155 801271808 177752 4294967295 134512640 135726644 3221224576 3199410336 135298548 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 195623 177752 300 300 0 195323 0
vsize: 782492
[startup+308.904 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 3491
Raw data (stat): 3489 (pb2sat) R 3488 23514 23513 0 -1 0 267786 0 0 0 29435 569 0 0 25 0 1 0 806785155 801271808 177752 4294967295 134512640 135726644 3221224576 3199410336 135298548 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 195623 177752 300 300 0 195323 0
vsize: 0

Child status: 1
Real time (s): 308.903
CPU time (s): 308.928
CPU user time (s): 302.871
CPU system time (s): 6.05708
CPU usage (%): 100.008
Max. virtual memory (Kb): 782492
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####