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/miplib3/normalized-mps-v2-20-10-p0548.opb
MD5SUM10547c6c0f11ab5df74fcaff6ba6d160
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 18719
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
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 benchmark1195.09
Number of variables548
Total number of constraints724
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)550
Number of constraints which are nor clauses,nor cardinality constraints134
Minimum length of a constraint1
Maximum length of a constraint143

Trace number 10115

Launcher Data

LAUNCH ON wulflinc14 THE 2005-09-23 16:59:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8858 boxname=wulflinc14 idbench=654 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc14/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc14/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 8858
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.058
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.058
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:        990084 kB
Buffers:          2200 kB
Cached:          25408 kB
SwapCached:          0 kB
Active:          16868 kB
Inactive:        13628 kB
HighTotal:      131008 kB
HighFree:       101332 kB
LowTotal:       903652 kB
LowFree:        888752 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6984 kB
Slab:             8448 kB
Committed_AS:    63624 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-23 17:03:42 (client local time) WITH STATUS 1 IN 260.811 SECONDS
stats: 8858 7 260.811 1

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

c Decision: 12464/174694	Time: 100.955/86400
c got solution with objective value: 71025
c small objective detected

	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/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21813708 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8670/statm): 373 2 364 364 0 9 0
[pid=8670] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc14/normalized-mps-v2-20-10-p0548.opb

[startup+10.0012 s]
Raw data (loadavg): 0.90 0.96 0.95 2/55 8670
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 29205 0 0 0 929 67 0 0 25 0 1 0 21813708 96432128 17762 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 23543 17762 364 364 0 23179 0
[pid=8670] vsize: 94172
Current children cumulated CPU time (s) 9.96
Current children cumulated vsize (Kb) 94172

[startup+20.0019 s]
Raw data (loadavg): 0.92 0.96 0.95 2/55 8670
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 29981 0 0 0 1925 70 0 0 25 0 1 0 21813708 98942976 18146 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 24156 18146 364 364 0 23792 0
[pid=8670] vsize: 96624
Current children cumulated CPU time (s) 19.95
Current children cumulated vsize (Kb) 96624

[startup+30.0016 s]
Raw data (loadavg): 0.93 0.96 0.95 2/55 8670
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 30789 0 0 0 2920 73 0 0 25 0 1 0 21813708 101777408 18725 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 24848 18725 364 364 0 24484 0
[pid=8670] vsize: 99392
Current children cumulated CPU time (s) 29.93
Current children cumulated vsize (Kb) 99392

[startup+40.0013 s]
Raw data (loadavg): 0.94 0.96 0.95 2/55 8670
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 31237 0 0 0 3913 76 0 0 25 0 1 0 21813708 103698432 19074 4294967295 134512640 135987407 3221224560 3221223120 134788454 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 25317 19074 364 364 0 24953 0
[pid=8670] vsize: 101268
Current children cumulated CPU time (s) 39.89
Current children cumulated vsize (Kb) 101268

[startup+50.0019 s]
Raw data (loadavg): 1.02 0.98 0.95 2/55 8725
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 31400 0 0 0 4905 82 0 0 25 0 1 0 21813708 104501248 19237 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 25513 19237 364 364 0 25149 0
[pid=8670] vsize: 102052
Current children cumulated CPU time (s) 49.87
Current children cumulated vsize (Kb) 102052

[startup+60.0016 s]
Raw data (loadavg): 1.02 0.98 0.95 2/55 8725
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 31417 0 0 0 5896 86 0 0 25 0 1 0 21813708 104697856 19254 4294967295 134512640 135987407 3221224560 3221223120 134788496 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 25561 19254 364 364 0 25197 0
[pid=8670] vsize: 102244
Current children cumulated CPU time (s) 59.82
Current children cumulated vsize (Kb) 102244

[startup+70.0023 s]
Raw data (loadavg): 1.02 0.98 0.95 2/55 8725
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 31424 0 0 0 6889 88 0 0 25 0 1 0 21813708 104697856 19261 4294967295 134512640 135987407 3221224560 3221223248 134811770 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 25561 19261 364 364 0 25197 0
[pid=8670] vsize: 102244
Current children cumulated CPU time (s) 69.77
Current children cumulated vsize (Kb) 102244

[startup+80.0029 s]
Raw data (loadavg): 1.01 0.98 0.95 2/55 8725
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 31843 0 0 0 7884 90 0 0 25 0 1 0 21813708 106287104 19549 4294967295 134512640 135987407 3221224560 3221223248 134811778 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 25949 19549 364 364 0 25585 0
[pid=8670] vsize: 103796
Current children cumulated CPU time (s) 79.74
Current children cumulated vsize (Kb) 103796

[startup+90.0026 s]
Raw data (loadavg): 1.01 0.98 0.95 2/55 8725
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 32102 0 0 0 8879 93 0 0 25 0 1 0 21813708 107225088 19775 4294967295 134512640 135987407 3221224560 3221223248 134811964 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 26178 19775 364 364 0 25814 0
[pid=8670] vsize: 104712
Current children cumulated CPU time (s) 89.72
Current children cumulated vsize (Kb) 104712

[startup+100.002 s]
Raw data (loadavg): 1.01 0.98 0.95 2/57 8727
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 32262 0 0 0 9875 94 0 0 25 0 1 0 21813708 107757568 19869 4294967295 134512640 135987407 3221224560 3221223424 134812647 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8670/statm): 26308 19869 364 364 0 25944 0
[pid=8670] vsize: 105232
Current children cumulated CPU time (s) 99.69
Current children cumulated vsize (Kb) 105232

[startup+110.003 s]
Raw data (loadavg): 1.01 0.98 0.95 1/55 8729
Raw data (/proc/8670/stat): 8670 (pb2sat) T 8669 8670 4060 0 -1 0 33130 0 0 0 10870 97 0 0 25 0 1 0 21813708 109895680 20263 4294967295 134512640 135987407 3221224560 3221223388 135541329 0 0 5 16384 3222434794 0 0 17 1 0 0
Raw data (/proc/8670/statm): 26830 20263 364 364 0 26466 0
[pid=8670] vsize: 107320
Current children cumulated CPU time (s) 109.67
Current children cumulated vsize (Kb) 107320

[startup+120.004 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 33291 0 0 0 11863 100 0 0 25 0 1 0 21813708 110563328 20391 4294967295 134512640 135987407 3221224560 3221223248 134811980 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 26993 20391 364 364 0 26629 0
[pid=8670] vsize: 107972
Current children cumulated CPU time (s) 119.63
Current children cumulated vsize (Kb) 107972

[startup+130.004 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 33420 0 0 0 12857 103 0 0 25 0 1 0 21813708 110960640 20454 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 27090 20454 364 364 0 26726 0
[pid=8670] vsize: 108360
Current children cumulated CPU time (s) 129.6
Current children cumulated vsize (Kb) 108360

[startup+140.004 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 33498 0 0 0 13851 105 0 0 25 0 1 0 21813708 111226880 20499 4294967295 134512640 135987407 3221224560 3221223424 134812696 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 27155 20499 364 364 0 26791 0
[pid=8670] vsize: 108620
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 108620

[startup+150.005 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 33551 0 0 0 14846 107 0 0 25 0 1 0 21813708 111493120 20552 4294967295 134512640 135987407 3221224560 3221223248 134811839 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 27220 20552 364 364 0 26856 0
[pid=8670] vsize: 108880
Current children cumulated CPU time (s) 149.53
Current children cumulated vsize (Kb) 108880

[startup+160.004 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 33814 0 0 0 15841 110 0 0 25 0 1 0 21813708 112820224 20749 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 27544 20749 364 364 0 27180 0
[pid=8670] vsize: 110176
Current children cumulated CPU time (s) 159.51
Current children cumulated vsize (Kb) 110176

[startup+170.005 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 60700 0 0 0 16779 169 0 0 25 0 1 0 21813708 192806912 36422 4294967295 134512640 135987407 3221224560 3221132464 134636927 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8670/statm): 47072 36422 364 364 0 46708 0
[pid=8670] vsize: 188288
Current children cumulated CPU time (s) 169.48
Current children cumulated vsize (Kb) 188288

[startup+180.006 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 103488 0 0 0 17689 255 0 0 25 0 1 0 21813708 324284416 57010 4294967295 134512640 135987407 3221224560 3221189472 134878895 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8670/statm): 79171 57010 364 364 0 78807 0
[pid=8670] vsize: 316684
Current children cumulated CPU time (s) 179.44
Current children cumulated vsize (Kb) 316684

[startup+190.006 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 122143 0 0 0 18647 295 0 0 25 0 1 0 21813708 383115264 75445 4294967295 134512640 135987407 3221224560 3221201328 134537491 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8670/statm): 93534 75445 364 364 0 93170 0
[pid=8670] vsize: 374136
Current children cumulated CPU time (s) 189.42
Current children cumulated vsize (Kb) 374136

[startup+200.007 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 141793 0 0 0 19601 339 0 0 25 0 1 0 21813708 409337856 94862 4294967295 134512640 135987407 3221224560 3221174160 134887887 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 99936 94862 364 364 0 99572 0
[pid=8670] vsize: 399744
Current children cumulated CPU time (s) 199.4
Current children cumulated vsize (Kb) 399744

[startup+210.007 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 207026 0 0 0 20460 476 0 0 25 0 1 0 21813708 646328320 115948 4294967295 134512640 135987407 3221224560 3221213808 134887887 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 157795 115949 364 364 0 157431 0
[pid=8670] vsize: 631180
Current children cumulated CPU time (s) 209.36
Current children cumulated vsize (Kb) 631180

[startup+220.007 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 223654 0 0 0 21423 512 0 0 25 0 1 0 21813708 702185472 132379 4294967295 134512640 135987407 3221224560 3221146248 134637789 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8670/statm): 171432 132379 364 364 0 171068 0
[pid=8670] vsize: 685728
Current children cumulated CPU time (s) 219.35
Current children cumulated vsize (Kb) 685728

[startup+230.007 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 242661 0 0 0 22378 555 0 0 25 0 1 0 21813708 726786048 151158 4294967295 134512640 135987407 3221224560 3221150956 134789859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8670/statm): 177438 151158 364 364 0 177074 0
[pid=8670] vsize: 709752
Current children cumulated CPU time (s) 229.33
Current children cumulated vsize (Kb) 709752

[startup+240.007 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 261505 0 0 0 23337 594 0 0 25 0 1 0 21813708 751251456 169776 4294967295 134512640 135987407 3221224560 3221172144 134887887 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 183411 169776 364 364 0 183047 0
[pid=8670] vsize: 733644
Current children cumulated CPU time (s) 239.31
Current children cumulated vsize (Kb) 733644

[startup+250.007 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 276303 0 0 0 24306 623 0 0 25 0 1 0 21813708 820776960 184396 4294967295 134512640 135987407 3221224560 3221152572 134637002 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/8670/statm): 200385 184396 364 364 0 200021 0
[pid=8670] vsize: 801540
Current children cumulated CPU time (s) 249.29
Current children cumulated vsize (Kb) 801540

[startup+260.007 s]
Raw data (loadavg): 1.00 0.98 0.95 2/55 8731
Raw data (/proc/8670/stat): 8670 (pb2sat) R 8669 8670 4060 0 -1 0 285129 0 0 0 25268 659 0 0 25 0 1 0 21813708 457900032 111354 4294967295 134512640 135987407 3221224560 3221223408 134884021 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8670/statm): 111792 111354 364 364 0 111428 0
[pid=8670] vsize: 447168
Current children cumulated CPU time (s) 259.27
Current children cumulated vsize (Kb) 447168
One traced child (pid=8670) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 261.536
CPU time (s): 260.811
CPU user time (s): 253.971
CPU system time (s): 6.83996
CPU usage (%): 99.7229
Max. virtual memory (cumulated for all children) (Kb): 801540

Verifier Data

ERROR: no interpretation found !