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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-bell3a.opb
MD5SUM20897ed4b3cd94cc1a84b64d339b40e4
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2147483647
Optimality of the best value was proved NO
Number of terms in the objective function 1716
Biggest coefficient in the objective function 5134096531456000
Number of bits for the biggest coefficient in the objective function 53
Sum of the numbers in the objective function 216401520151185266
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 5134096531456000
Number of bits of the biggest number in a constraint 53
Biggest sum of numbers in a constraint 216401520151185266
Number of bits of the biggest sum of numbers58
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1252.45
Number of variables2219
Total number of constraints194
Number of constraints which are clauses22
Number of constraints which are cardinality constraints (but not clauses)39
Number of constraints which are nor clauses,nor cardinality constraints133
Minimum length of a constraint1
Maximum length of a constraint191

Trace number 42381 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-06-16 06:15:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25600 boxname=wulflinc2 idbench=900 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  20897ed4b3cd94cc1a84b64d339b40e4  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-bell3a.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-bell3a.opb
IDLAUNCH: 25600
/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:        709708 kB
Buffers:         34816 kB
Cached:         264832 kB
SwapCached:       4448 kB
Active:          61348 kB
Inactive:       243424 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        709456 kB
SwapTotal:     2097136 kB
SwapFree:      2091696 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5056 kB
Slab:            14580 kB
Committed_AS:    71904 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 06:18:12 (client local time) WITH STATUS 1 IN 151.494 SECONDS
stats: 25600 7 151.494 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...
c got solution with objective value: 2831141305875703
c big objective detected
c trying from 0 to 511
c CONFLICT during preprocess 
c trying from 512 to 1023

	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.95 0.90 2/54 6158
Raw data (stat): 6158 (runsolver) R 6157 31399 31398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 968531733 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.0007 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 25973 0 0 0 941 58 0 0 25 0 1 0 968531733 77750272 15059 4294967295 134512640 135730672 3221224576 3221199520 134770772 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 18982 15059 301 301 0 18681 0
vsize: 75928
[startup+20.0005 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 50950 0 0 0 1890 108 0 0 25 0 1 0 968531733 151875584 28814 4294967295 134512640 135730672 3221224576 3221197628 134608033 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 37079 28814 301 301 0 36778 0
vsize: 148316
[startup+30.0013 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 87147 0 0 0 2820 179 0 0 25 0 1 0 968531733 261783552 43327 4294967295 134512640 135730672 3221224576 3221200332 135301649 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 63912 43327 301 301 0 63611 0
vsize: 255648
[startup+40.0031 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 100071 0 0 0 3791 208 0 0 25 0 1 0 968531733 298852352 56008 4294967295 134512640 135730672 3221224576 3221195344 134546483 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 72962 56008 301 301 0 72661 0
vsize: 291848
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 139756 0 0 0 4718 281 0 0 25 0 1 0 968531733 493772800 94498 4294967295 134512640 135730672 3221224576 3221202336 135282197 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 120550 94498 301 301 0 120249 0
vsize: 482200
[startup+60.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 149457 0 0 0 5693 306 0 0 25 0 1 0 968531733 431710208 84429 4294967295 134512640 135730672 3221224576 3221223264 134748449 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 105398 84429 301 301 0 105097 0
vsize: 421592
[startup+70.0054 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 149465 0 0 0 6692 308 0 0 25 0 1 0 968531733 431710208 84437 4294967295 134512640 135730672 3221224576 3221223072 134747878 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 105398 84437 301 301 0 105097 0
vsize: 421592
[startup+80.0059 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 149630 0 0 0 7691 309 0 0 25 0 1 0 968531733 432447488 84602 4294967295 134512640 135730672 3221224576 3221222896 134732518 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 105578 84602 301 301 0 105277 0
vsize: 422312
[startup+90.0056 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 179688 0 0 0 8622 377 0 0 25 0 1 0 968531733 534306816 89969 4294967295 134512640 135730672 3221224576 3220588064 134607963 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 130446 89969 301 301 0 130145 0
vsize: 521784
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 194793 0 0 0 9587 413 0 0 25 0 1 0 968531733 587096064 104847 4294967295 134512640 135730672 3221224576 3221138608 134784086 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 143334 104847 301 301 0 143033 0
vsize: 573336
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 212767 0 0 0 10546 453 0 0 25 0 1 0 968531733 615890944 122583 4294967295 134512640 135730672 3221224576 3220971232 134770715 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 150364 122584 301 301 0 150063 0
vsize: 601456
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 231259 0 0 0 11504 496 0 0 25 0 1 0 968531733 645234688 140828 4294967295 134512640 135730672 3221224576 3220988016 134608819 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 157528 140828 301 301 0 157227 0
vsize: 630112
[startup+130.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 243871 0 0 0 12477 523 0 0 25 0 1 0 968531733 667344896 147078 4294967295 134512640 135730672 3221224576 3221223024 134739768 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 162926 147078 301 301 0 162625 0
vsize: 651704
[startup+140.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 257558 0 0 0 13442 558 0 0 25 0 1 0 968531733 723439616 160765 4294967295 134512640 135730672 3221224576 3221223024 134739827 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 176621 160765 301 301 0 176320 0
vsize: 706484
[startup+150.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 260393 0 0 0 14423 577 0 0 25 0 1 0 968531733 403472384 97939 4294967295 134512640 135730672 3221224576 3221222948 135104789 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 98504 97939 301 301 0 98203 0
vsize: 394016
[startup+151.493 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 6158
Raw data (stat): 6158 (pb2sat-v2) R 6157 31399 31398 0 -1 0 260393 0 0 0 14423 577 0 0 25 0 1 0 968531733 403472384 97939 4294967295 134512640 135730672 3221224576 3221222948 135104789 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 98504 97939 301 301 0 98203 0
vsize: 0

Child status: 1
Real time (s): 151.493
CPU time (s): 151.494
CPU user time (s): 145.513
CPU system time (s): 5.98109
CPU usage (%): 100.001
Max. virtual memory (Kb): 706484
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####