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/submitted/manquinho/primes-dimacs-cnf/normalized-ssa2670-141.opb
MD5SUM	423b72910a463b7aa4b9bdae86b878a8
Bench Category	optimization, small integers (OPTSMALLINT)
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	1972
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1972
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1972
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.158974
Number of variables	1972
Total number of constraints	3301
Number of constraints which are clauses	3301
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	5

Trace number 34855

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-28 11:01:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24151 boxname=wulflinc24 idbench=225 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  423b72910a463b7aa4b9bdae86b878a8  /oldhome/oroussel/tmp/wulflinc24/normalized-ssa2670-141.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc24/normalized-ssa2670-141.opb
IDLAUNCH: 24151
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        713976 kB
Buffers:         36524 kB
Cached:         262380 kB
SwapCached:        636 kB
Active:          20276 kB
Inactive:       280688 kB
HighTotal:      131008 kB
HighFree:        29092 kB
LowTotal:       903652 kB
LowFree:        684884 kB
SwapTotal:     2097892 kB
SwapFree:      2096360 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5148 kB
Slab:            14060 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 11:06:22 (client local time) WITH STATUS 20 IN 298.8 SECONDS
stats: 24151 7 298.8 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...
c [startup+204.797 s]  setting bit 10 to 0
c CONFLICT during preprocess 
c [startup+213.448 s]  setting bit 9 to 0
c CONFLICT during preprocess 
c [startup+221.95 s]  setting bit 8 to 0
c CONFLICT during preprocess 
c [startup+230.44 s]  setting bit 7 to 0
c CONFLICT during preprocess 
c [startup+238.923 s]  setting bit 6 to 0
c CONFLICT during preprocess 
c [startup+247.398 s]  setting bit 5 to 0
c CONFLICT during preprocess 
c [startup+255.873 s]  setting bit 4 to 0
c CONFLICT during preprocess 
c [startup+264.348 s]  setting bit 3 to 0
c CONFLICT during preprocess 
c [startup+272.823 s]  setting bit 2 to 0
c CONFLICT during preprocess 
c [startup+281.294 s]  setting bit 1 to 0
c CONFLICT during preprocess 
c [startup+289.768 s]  setting bit 0 to 0
s UNSATISFIABLE
#### 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.95 0.91 2/54 18838
Raw data (stat): 18838 (runsolver) R 18837 4613 4612 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 864279461 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.94 0.95 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 28906 0 0 0 934 64 0 0 25 0 1 0 864279461 88547328 17975 4294967295 134512640 135726644 3221224592 3220936232 135280405 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 21618 17975 300 300 0 21318 0
vsize: 86472
[startup+20.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 56926 0 0 0 1871 128 0 0 25 0 1 0 864279461 173862912 35043 4294967295 134512640 135726644 3221224592 3220746908 134604451 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 42447 35043 300 300 0 42147 0
vsize: 169788
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 97184 0 0 0 2784 215 0 0 25 0 1 0 864279461 298639360 53630 4294967295 134512640 135726644 3221224592 3221130508 134604449 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 72910 53630 300 300 0 72610 0
vsize: 291640
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 112092 0 0 0 3749 250 0 0 25 0 1 0 864279461 343142400 68319 4294967295 134512640 135726644 3221224592 3220915732 134554779 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 83775 68319 300 300 0 83475 0
vsize: 335100
[startup+50.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 131516 0 0 0 4707 292 0 0 25 0 1 0 864279461 371122176 87518 4294967295 134512640 135726644 3221224592 3221169504 135278582 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 90606 87518 300 300 0 90306 0
vsize: 362424
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 192544 0 0 0 5583 416 0 0 25 0 1 0 864279461 594993152 105440 4294967295 134512640 135726644 3221224592 3220726400 135287555 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 145262 105440 300 300 0 144962 0
vsize: 581048
[startup+70.0045 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 203742 0 0 0 6555 445 0 0 25 0 1 0 864279461 628547584 116438 4294967295 134512640 135726644 3221224592 3220915376 134606359 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 153454 116438 300 300 0 153154 0
vsize: 613816
[startup+80.0052 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 220260 0 0 0 7515 485 0 0 25 0 1 0 864279461 644902912 132733 4294967295 134512640 135726644 3221224592 3221048388 135287520 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 157447 132733 300 300 0 157147 0
vsize: 629788
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 239324 0 0 0 8474 526 0 0 25 0 1 0 864279461 672206848 151576 4294967295 134512640 135726644 3221224592 3221098116 135279151 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 164113 151576 300 300 0 163813 0
vsize: 656452
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 260113 0 0 0 9426 573 0 0 25 0 1 0 864279461 772657152 172212 4294967295 134512640 135726644 3221224592 3221222904 134761847 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 188637 172212 300 300 0 188337 0
vsize: 754548
[startup+110.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 265944 0 0 0 10413 587 0 0 25 0 1 0 864279461 777404416 172685 4294967295 134512640 135726644 3221224592 3221223196 135280476 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 189796 172685 300 300 0 189496 0
vsize: 759184
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 269177 0 0 0 11407 593 0 0 25 0 1 0 864279461 788086784 174874 4294967295 134512640 135726644 3221224592 3221223088 134743980 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 192404 174874 300 300 0 192104 0
vsize: 769616
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 270890 0 0 0 12404 596 0 0 25 0 1 0 864279461 793403392 175874 4294967295 134512640 135726644 3221224592 3221223088 134744153 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 193702 175874 300 300 0 193402 0
vsize: 774808
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 271983 0 0 0 13401 599 0 0 25 0 1 0 864279461 796647424 176303 4294967295 134512640 135726644 3221224592 3221223216 134744612 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 194494 176303 300 300 0 194194 0
vsize: 777976
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 272198 0 0 0 14400 600 0 0 25 0 1 0 864279461 797171712 176389 4294967295 134512640 135726644 3221224592 3221223088 134743901 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 194622 176389 300 300 0 194322 0
vsize: 778488
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 272663 0 0 0 15398 602 0 0 25 0 1 0 864279461 798617600 176532 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 194975 176532 300 300 0 194675 0
vsize: 779900
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 273708 0 0 0 16396 605 0 0 25 0 1 0 864279461 801517568 176934 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 195683 176934 300 300 0 195383 0
vsize: 782732
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 274558 0 0 0 17394 607 0 0 25 0 1 0 864279461 803749888 177269 4294967295 134512640 135726644 3221224592 3221223264 134745056 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196228 177269 300 300 0 195928 0
vsize: 784912
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 274870 0 0 0 18393 607 0 0 25 0 1 0 864279461 803749888 177581 4294967295 134512640 135726644 3221224592 3221223088 134744156 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196228 177581 300 300 0 195928 0
vsize: 784912
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 274995 0 0 0 19393 608 0 0 25 0 1 0 864279461 803889152 177706 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196262 177706 300 300 0 195962 0
vsize: 785048
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 279163 0 0 0 20382 619 0 0 25 0 1 0 864279461 803889152 178066 4294967295 134512640 135726644 3221224592 3221223168 134738146 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196262 178066 300 300 0 195962 0
vsize: 785048
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 282971 0 0 0 21371 629 0 0 25 0 1 0 864279461 803889152 178066 4294967295 134512640 135726644 3221224592 3221223312 134736184 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196262 178066 300 300 0 195962 0
vsize: 785048
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 286779 0 0 0 22361 640 0 0 25 0 1 0 864279461 803889152 178066 4294967295 134512640 135726644 3221224592 3221223312 134736260 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196262 178066 300 300 0 195962 0
vsize: 785048
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 294395 0 0 0 23340 661 0 0 25 0 1 0 864279461 819486720 181874 4294967295 134512640 135726644 3221224592 3221222928 134765241 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 200070 181874 300 300 0 199770 0
vsize: 800280
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 298203 0 0 0 24330 671 0 0 25 0 1 0 864279461 819486720 181874 4294967295 134512640 135726644 3221224592 3221222928 134765226 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 200070 181874 300 300 0 199770 0
vsize: 800280
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 302011 0 0 0 25320 681 0 0 25 0 1 0 864279461 819486720 181874 4294967295 134512640 135726644 3221224592 3221222912 134765177 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 200070 181874 300 300 0 199770 0
vsize: 800280
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 305819 0 0 0 26310 691 0 0 25 0 1 0 864279461 803889152 178066 4294967295 134512640 135726644 3221224592 3221223136 134746281 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196262 178066 300 300 0 195962 0
vsize: 785048
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 309627 0 0 0 27301 700 0 0 25 0 1 0 864279461 803889152 178066 4294967295 134512640 135726644 3221224592 3221223312 134736256 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196262 178066 300 300 0 195962 0
vsize: 785048
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18838
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 313435 0 0 0 28292 710 0 0 25 0 1 0 864279461 803889152 178066 4294967295 134512640 135726644 3221224592 3221222608 135280446 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196262 178066 300 300 0 195962 0
vsize: 785048
[startup+298.787 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 18840
Raw data (stat): 18838 (pb2sat) R 18837 4613 4612 0 -1 0 313435 0 0 0 28292 710 0 0 25 0 1 0 864279461 803889152 178066 4294967295 134512640 135726644 3221224592 3221222608 135280446 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 196262 178066 300 300 0 195962 0
vsize: 0

Child status: 20
Real time (s): 298.786
CPU time (s): 298.8
CPU user time (s): 291.32
CPU system time (s): 7.47986
CPU usage (%): 100.004
Max. virtual memory (Kb): 800280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####