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/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-dg012142.opb
MD5SUMbc2dcc682f209df3faf1b0ad321ee43d
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 24640
Biggest coefficient in the objective function 5368709120000
Number of bits for the biggest coefficient in the objective function 43
Sum of the numbers in the objective function 1723417105498688
Number of bits of the sum of numbers in the objective function 51
Biggest number in a constraint 5368709120000
Number of bits of the biggest number in a constraint 43
Biggest sum of numbers in a constraint 1723417105498688
Number of bits of the biggest sum of numbers51
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1293.53
Number of variables43840
Total number of constraints6310
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints6270
Minimum length of a constraint1
Maximum length of a constraint371

Trace number 35386 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-05-28 13:03:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24690 boxname=wulflinc21 idbench=1162 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc2dcc682f209df3faf1b0ad321ee43d  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-dg012142.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-dg012142.opb
IDLAUNCH: 24690
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        808512 kB
Buffers:         34684 kB
Cached:         167544 kB
SwapCached:        956 kB
Active:          67492 kB
Inactive:       136892 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        808260 kB
SwapTotal:     2097892 kB
SwapFree:      2096012 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5136 kB
Slab:            16052 kB
Committed_AS:    63916 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 13:05:10 (client local time) WITH STATUS 1 IN 117.952 SECONDS
stats: 24690 7 117.952 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.92 0.95 0.90 2/55 14928
Raw data (stat): 14928 (runsolver) R 14927 32363 32362 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 742277947 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.0002 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 2268 0 0 0 993 5 0 0 25 0 1 0 742277947 8368128 1593 4294967295 134512640 135726644 3221224576 3221221664 134556187 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2043 1593 300 300 0 1743 0
vsize: 8172
[startup+20.001 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 29605 0 0 0 1933 65 0 0 25 0 1 0 742277947 99823616 18486 4294967295 134512640 135726644 3221224576 3211433200 134780362 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 24371 18486 300 300 0 24071 0
vsize: 97484
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 58233 0 0 0 2873 125 0 0 25 0 1 0 742277947 185917440 35900 4294967295 134512640 135726644 3221224576 3211834828 134766457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 45390 35900 300 300 0 45090 0
vsize: 181560
[startup+40.0013 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 99188 0 0 0 3788 211 0 0 25 0 1 0 742277947 311033856 54661 4294967295 134512640 135726644 3221224576 3212576128 134554568 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 75936 54661 300 300 0 75636 0
vsize: 303744
[startup+50.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 115364 0 0 0 4750 249 0 0 25 0 1 0 742277947 357834752 70608 4294967295 134512640 135726644 3221224576 3211777824 134604377 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 87362 70608 300 300 0 87062 0
vsize: 349448
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 143780 0 0 0 5694 305 0 0 25 0 1 0 742277947 542347264 98486 4294967295 134512640 135726644 3221224576 3212540524 135298000 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 132409 98486 300 300 0 132109 0
vsize: 529636
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 197130 0 0 0 6585 415 0 0 25 0 1 0 742277947 609148928 107998 4294967295 134512640 135726644 3221224576 3211899312 135288929 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 148718 107998 300 300 0 148418 0
vsize: 594872
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 209208 0 0 0 7556 443 0 0 25 0 1 0 742277947 642703360 119864 4294967295 134512640 135726644 3221224576 3212088528 134554691 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 156910 119864 300 300 0 156610 0
vsize: 627640
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 228904 0 0 0 8515 485 0 0 25 0 1 0 742277947 666492928 139313 4294967295 134512640 135726644 3221224576 3212390152 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 162718 139313 300 300 0 162418 0
vsize: 650872
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 247999 0 0 0 9475 525 0 0 25 0 1 0 742277947 743993344 158189 4294967295 134512640 135726644 3221224576 3211844400 134780358 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 181639 158189 300 300 0 181339 0
vsize: 726556
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 266457 0 0 0 10438 562 0 0 25 0 1 0 742277947 770215936 176435 4294967295 134512640 135726644 3221224576 3212054928 134554568 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 188041 176437 300 300 0 187741 0
vsize: 752164
[startup+117.951 s]
Raw data (loadavg): 0.99 0.96 0.91 1/54 14928
Raw data (stat): 14928 (pb2sat) R 14927 32363 32362 0 -1 0 266457 0 0 0 10438 562 0 0 25 0 1 0 742277947 770215936 176435 4294967295 134512640 135726644 3221224576 3212054928 134554568 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 188041 176437 300 300 0 187741 0
vsize: 0

Child status: 1
Real time (s): 117.95
CPU time (s): 117.952
CPU user time (s): 111.949
CPU system time (s): 6.00309
CPU usage (%): 100.001
Max. virtual memory (Kb): 752164
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####