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).
    Note that some very long lines in this section may be truncated by your web browser !
  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

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-fast0507.opb
MD5SUM38504d32a17a57a658eee171614b901e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 324
Optimality of the best value was proved NO
Number of terms in the objective function 63009
Biggest coefficient in the objective function 2
Number of bits for the biggest coefficient in the objective function 2
Sum of the numbers in the objective function 122425
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 2
Number of bits of the biggest number in a constraint 2
Biggest sum of numbers in a constraint 122425
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.22
Number of variables63009
Total number of constraints63516
Number of constraints which are clauses507
Number of constraints which are cardinality constraints (but not clauses)63009
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint7753

Trace number 10012

Launcher Data

LAUNCH ON wulflinc20 THE 2005-09-23 16:30:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8768 boxname=wulflinc20 idbench=564 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  38504d32a17a57a658eee171614b901e  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-fast0507.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-fast0507.opb
IDLAUNCH: 8768
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.012
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	: 3
cpu MHz		: 451.012
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        924168 kB
Buffers:         11832 kB
Cached:          81260 kB
SwapCached:          0 kB
Active:          56780 kB
Inactive:        39248 kB
HighTotal:      131008 kB
HighFree:        45276 kB
LowTotal:       903652 kB
LowFree:        878892 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6980 kB
Slab:             8836 kB
Committed_AS:    63660 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-23 16:34:05 (client local time) WITH STATUS 1 IN 232.553 SECONDS
stats: 8768 7 232.553 1

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...
c got solution with objective value: 122425
c big objective detected
c trying from 0 to 511

	Unexpected exception :
	St9bad_alloc

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21639206 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 373 2 364 364 0 9 0
[pid=8075] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-fast0507.opb

[startup+10.0028 s]
Raw data (loadavg): 0.91 0.91 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 2131 0 0 0 991 7 0 0 25 0 1 0 21639206 8556544 1452 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 2089 1452 364 364 0 1725 0
[pid=8075] vsize: 8356
Current children cumulated CPU time (s) 9.98
Current children cumulated vsize (Kb) 8356

[startup+20.0035 s]
Raw data (loadavg): 0.92 0.91 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 2843 0 0 0 1988 9 0 0 25 0 1 0 21639206 10313728 2151 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 2518 2151 364 364 0 2154 0
[pid=8075] vsize: 10072
Current children cumulated CPU time (s) 19.97
Current children cumulated vsize (Kb) 10072

[startup+30.0032 s]
Raw data (loadavg): 0.93 0.92 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 4279 0 0 0 2985 12 0 0 25 0 1 0 21639206 15360000 2842 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 3750 2842 364 364 0 3386 0
[pid=8075] vsize: 15000
Current children cumulated CPU time (s) 29.97
Current children cumulated vsize (Kb) 15000

[startup+40.0039 s]
Raw data (loadavg): 0.94 0.92 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 4569 0 0 0 3984 13 0 0 25 0 1 0 21639206 16035840 3126 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 3915 3126 364 364 0 3551 0
[pid=8075] vsize: 15660
Current children cumulated CPU time (s) 39.97
Current children cumulated vsize (Kb) 15660

[startup+50.0047 s]
Raw data (loadavg): 0.95 0.92 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 4839 0 0 0 4984 13 0 0 25 0 1 0 21639206 16711680 3392 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 4080 3392 364 364 0 3716 0
[pid=8075] vsize: 16320
Current children cumulated CPU time (s) 49.97
Current children cumulated vsize (Kb) 16320

[startup+60.0054 s]
Raw data (loadavg): 0.96 0.92 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 5072 0 0 0 5983 14 0 0 25 0 1 0 21639206 17387520 3621 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 4245 3621 364 364 0 3881 0
[pid=8075] vsize: 16980
Current children cumulated CPU time (s) 59.97
Current children cumulated vsize (Kb) 16980

[startup+70.0061 s]
Raw data (loadavg): 0.96 0.92 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 5283 0 0 0 6983 14 0 0 25 0 1 0 21639206 17928192 3829 4294967295 134512640 135987407 3221224560 3221221872 134555870 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 4377 3829 364 364 0 4013 0
[pid=8075] vsize: 17508
Current children cumulated CPU time (s) 69.97
Current children cumulated vsize (Kb) 17508

[startup+80.0069 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 5478 0 0 0 7983 15 0 0 25 0 1 0 21639206 18333696 4021 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 4476 4021 364 364 0 4112 0
[pid=8075] vsize: 17904
Current children cumulated CPU time (s) 79.98
Current children cumulated vsize (Kb) 17904

[startup+90.0076 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 5660 0 0 0 8982 15 0 0 25 0 1 0 21639206 18874368 4200 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 4608 4200 364 364 0 4244 0
[pid=8075] vsize: 18432
Current children cumulated CPU time (s) 89.97
Current children cumulated vsize (Kb) 18432

[startup+100.007 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 5835 0 0 0 9982 16 0 0 25 0 1 0 21639206 19279872 4372 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 4707 4372 364 364 0 4343 0
[pid=8075] vsize: 18828
Current children cumulated CPU time (s) 99.98
Current children cumulated vsize (Kb) 18828

[startup+110.008 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 6651 0 0 0 10975 22 0 0 25 0 1 0 21639206 22675456 5187 4294967295 134512640 135987407 3221224560 3221221952 134615232 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 5536 5187 364 364 0 5172 0
[pid=8075] vsize: 22144
Current children cumulated CPU time (s) 109.97
Current children cumulated vsize (Kb) 22144

[startup+120.009 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 6821 0 0 0 11971 24 0 0 25 0 1 0 21639206 24248320 5357 4294967295 134512640 135987407 3221224560 3221221532 134636975 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 5920 5357 364 364 0 5556 0
[pid=8075] vsize: 23680
Current children cumulated CPU time (s) 119.95
Current children cumulated vsize (Kb) 23680

[startup+130.01 s]
Raw data (loadavg): 1.05 0.95 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 18442 0 0 0 12936 57 0 0 25 0 1 0 21639206 65339392 15110 4294967295 134512640 135987407 3221224560 3200729088 134854865 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 15952 15110 364 364 0 15588 0
[pid=8075] vsize: 63808
Current children cumulated CPU time (s) 129.93
Current children cumulated vsize (Kb) 63808

[startup+140.01 s]
Raw data (loadavg): 1.04 0.95 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 53928 0 0 0 13847 142 0 0 25 0 1 0 21639206 172818432 37325 4294967295 134512640 135987407 3221224560 3214183280 134878008 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 42192 37325 364 364 0 41828 0
[pid=8075] vsize: 168768
Current children cumulated CPU time (s) 139.89
Current children cumulated vsize (Kb) 168768

[startup+150.011 s]
Raw data (loadavg): 1.04 0.95 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 92290 0 0 0 14754 230 0 0 25 0 1 0 21639206 300089344 59619 4294967295 134512640 135987407 3221224560 3211198324 134636948 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 73264 59619 364 364 0 72900 0
[pid=8075] vsize: 293056
Current children cumulated CPU time (s) 149.84
Current children cumulated vsize (Kb) 293056

[startup+160.012 s]
Raw data (loadavg): 1.03 0.95 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 122472 0 0 0 15683 299 0 0 25 0 1 0 21639206 409387008 77296 4294967295 134512640 135987407 3221224560 3200389800 134856361 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 99948 77296 364 364 0 99584 0
[pid=8075] vsize: 399792
Current children cumulated CPU time (s) 159.82
Current children cumulated vsize (Kb) 399792

[startup+170.012 s]
Raw data (loadavg): 1.03 0.96 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 142815 0 0 0 16633 348 0 0 25 0 1 0 21639206 435474432 97394 4294967295 134512640 135987407 3221224560 3201044144 134887887 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 106317 97394 364 364 0 105953 0
[pid=8075] vsize: 425268
Current children cumulated CPU time (s) 169.81
Current children cumulated vsize (Kb) 425268

[startup+180.013 s]
Raw data (loadavg): 1.02 0.96 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 187022 0 0 0 17536 440 0 0 25 0 1 0 21639206 775426048 122002 4294967295 134512640 135987407 3221224560 3215824448 134887487 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 189313 122002 364 364 0 188949 0
[pid=8075] vsize: 757252
Current children cumulated CPU time (s) 179.76
Current children cumulated vsize (Kb) 757252

[startup+190.014 s]
Raw data (loadavg): 1.02 0.96 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 225663 0 0 0 18447 526 0 0 25 0 1 0 21639206 727101440 135897 4294967295 134512640 135987407 3221224560 3221078412 134636944 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 177515 135897 364 364 0 177151 0
[pid=8075] vsize: 710060
Current children cumulated CPU time (s) 189.73
Current children cumulated vsize (Kb) 710060

[startup+200.014 s]
Raw data (loadavg): 1.01 0.96 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 245954 0 0 0 19396 575 0 0 25 0 1 0 21639206 753459200 155942 4294967295 134512640 135987407 3221224560 3218116640 134887887 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8075/statm): 183950 155943 364 364 0 183586 0
[pid=8075] vsize: 735800
Current children cumulated CPU time (s) 199.71
Current children cumulated vsize (Kb) 735800

[startup+210.014 s]
Raw data (loadavg): 1.01 0.96 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 265882 0 0 0 20348 621 0 0 25 0 1 0 21639206 779952128 175624 4294967295 134512640 135987407 3221224560 3208088048 134887887 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8075/statm): 190418 175624 364 364 0 190054 0
[pid=8075] vsize: 761672
Current children cumulated CPU time (s) 209.69
Current children cumulated vsize (Kb) 761672

[startup+220.014 s]
Raw data (loadavg): 1.01 0.96 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 282688 0 0 0 21309 658 0 0 25 0 1 0 21639206 853667840 192245 4294967295 134512640 135987407 3221224560 3218343104 134887887 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8075/statm): 208415 192246 364 364 0 208051 0
[pid=8075] vsize: 833660
Current children cumulated CPU time (s) 219.67
Current children cumulated vsize (Kb) 833660

[startup+230.014 s]
Raw data (loadavg): 1.01 0.96 0.92 2/55 8075
Raw data (/proc/8075/stat): 8075 (pb2sat) R 8074 8075 4059 0 -1 0 289857 0 0 0 22271 695 0 0 25 0 1 0 21639206 361046016 87682 4294967295 134512640 135987407 3221224560 3221223320 135477274 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8075/statm): 88146 87682 364 364 0 87782 0
[pid=8075] vsize: 352584
Current children cumulated CPU time (s) 229.66
Current children cumulated vsize (Kb) 352584
One traced child (pid=8075) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 232.899
CPU time (s): 232.553
CPU user time (s): 225.411
CPU system time (s): 7.14191
CPU usage (%): 99.8514
Max. virtual memory (cumulated for all children) (Kb): 833660

Verifier Data

ERROR: no interpretation found !