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-misc04.opb
MD5SUM7b42190d864979953c47e5a92736f365
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 43188899594881916928
Number of bits of the biggest number in a constraint 66
Biggest sum of numbers in a constraint 133861748414790074368
Number of bits of the biggest sum of numbers67
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark4.12137
Number of variables146276
Total number of constraints1755
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)45
Number of constraints which are nor clauses,nor cardinality constraints1710
Minimum length of a constraint1
Maximum length of a constraint5071

Trace number 35149 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-28 12:19:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24450 boxname=wulflinc15 idbench=922 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7b42190d864979953c47e5a92736f365  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-misc04.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-misc04.opb
IDLAUNCH: 24450
/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:        908572 kB
Buffers:         33200 kB
Cached:          69896 kB
SwapCached:        604 kB
Active:          55428 kB
Inactive:        49768 kB
HighTotal:      131008 kB
HighFree:        58912 kB
LowTotal:       903652 kB
LowFree:        849660 kB
SwapTotal:     2097136 kB
SwapFree:      2095616 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            15196 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 12:21:03 (client local time) WITH STATUS 1 IN 100.725 SECONDS
stats: 24450 7 100.725 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.85 0.94 0.90 1/54 1946
Raw data (stat): 1946 (runsolver) R 1945 23514 23513 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806521811 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.0011 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 28263 0 0 0 937 62 0 0 25 0 1 0 806521811 83087360 17127 4294967295 134512640 135726644 3221224576 3221007072 134554691 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 20285 17127 300 300 0 19985 0
vsize: 81140
[startup+20.0024 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 55655 0 0 0 1879 120 0 0 25 0 1 0 806521811 161882112 33293 4294967295 134512640 135726644 3221224576 3220949496 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 39522 33294 300 300 0 39222 0
vsize: 158088
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 92965 0 0 0 2803 196 0 0 25 0 1 0 806521811 304054272 48409 4294967295 134512640 135726644 3221224576 3221033008 134767123 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 74232 48409 300 300 0 73932 0
vsize: 296928
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 107974 0 0 0 3773 225 0 0 25 0 1 0 806521811 307568640 63160 4294967295 134512640 135726644 3221224576 3220997496 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 75090 63161 300 300 0 74790 0
vsize: 300360
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 149416 0 0 0 4690 308 0 0 25 0 1 0 806521811 436994048 86009 4294967295 134512640 135726644 3221224576 3220987492 135277617 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 106688 86009 300 300 0 106388 0
vsize: 426752
[startup+60.0034 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 183866 0 0 0 5615 384 0 0 25 0 1 0 806521811 571211776 95703 4294967295 134512640 135726644 3221224576 3220980144 134780450 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 139456 95703 300 300 0 139156 0
vsize: 557824
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 198742 0 0 0 6582 417 0 0 25 0 1 0 806521811 571211776 110310 4294967295 134512640 135726644 3221224576 3221002092 135287445 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 139456 110311 300 300 0 139156 0
vsize: 557824
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 214248 0 0 0 7548 450 0 0 25 0 1 0 806521811 576348160 125557 4294967295 134512640 135726644 3221224576 3220966224 134782642 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 140710 125557 300 300 0 140410 0
vsize: 562840
[startup+90.0048 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 229698 0 0 0 8517 482 0 0 25 0 1 0 806521811 641548288 140792 4294967295 134512640 135726644 3221224576 3220977036 134604449 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 156628 140792 300 300 0 156328 0
vsize: 626512
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 243410 0 0 0 9467 532 0 0 25 0 1 0 806521811 153358336 37282 4294967295 134512640 135726644 3221224576 3221223020 135277617 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 37441 37282 300 300 0 37141 0
vsize: 149764
[startup+100.736 s]
Raw data (loadavg): 0.97 0.95 0.91 1/53 1946
Raw data (stat): 1946 (pb2sat) R 1945 23514 23513 0 -1 0 243410 0 0 0 9467 532 0 0 25 0 1 0 806521811 153358336 37282 4294967295 134512640 135726644 3221224576 3221223020 135277617 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 37441 37282 300 300 0 37141 0
vsize: 0

Child status: 1
Real time (s): 100.735
CPU time (s): 100.725
CPU user time (s): 95.3175
CPU system time (s): 5.40718
CPU usage (%): 99.9896
Max. virtual memory (Kb): 626512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####