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

Namesubmitted/een/normalized-fast0507.opb
MD5SUMbc1a4f1c9875fd4d3273e85dcf5e871e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 251
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 benchmark1203.94
Number of variables63001
Total number of constraints489
Number of constraints which are clauses489
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint7753

Trace number 9745

Launcher Data

LAUNCH ON wulflinc3 THE 2005-09-23 15:14:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8475 boxname=wulflinc3 idbench=271 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc1a4f1c9875fd4d3273e85dcf5e871e  /oldhome/oroussel/tmp/wulflinc3/normalized-fast0507.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc3/normalized-fast0507.opb
IDLAUNCH: 8475
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.228
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.228
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:        935264 kB
Buffers:         12288 kB
Cached:          69652 kB
SwapCached:          0 kB
Active:          48268 kB
Inactive:        36568 kB
HighTotal:      131008 kB
HighFree:        57036 kB
LowTotal:       903652 kB
LowFree:        878228 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6972 kB
Slab:             8948 kB
Committed_AS:    63656 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-23 15:18:05 (client local time) WITH STATUS 1 IN 219.301 SECONDS
stats: 8475 7 219.301 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/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21202059 1527808 2 4294967295 134512640 135987407 3221224576 3221224576 134512928 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 373 2 364 364 0 9 0
[pid=7389] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-fast0507.opb

[startup+10.0018 s]
Raw data (loadavg): 0.83 0.94 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 2553 0 0 0 992 7 0 0 25 0 1 0 21202059 9498624 1867 4294967295 134512640 135987407 3221224576 3221221888 134555870 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 2319 1867 364 364 0 1955 0
[pid=7389] vsize: 9276
Current children cumulated CPU time (s) 9.99
Current children cumulated vsize (Kb) 9276

[startup+20.0026 s]
Raw data (loadavg): 0.86 0.94 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 3035 0 0 0 1991 8 0 0 25 0 1 0 21202059 10715136 2341 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 2616 2341 364 364 0 2252 0
[pid=7389] vsize: 10464
Current children cumulated CPU time (s) 19.99
Current children cumulated vsize (Kb) 10464

[startup+30.0035 s]
Raw data (loadavg): 0.88 0.94 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 4406 0 0 0 2987 12 0 0 25 0 1 0 21202059 15626240 2967 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 3815 2967 364 364 0 3451 0
[pid=7389] vsize: 15260
Current children cumulated CPU time (s) 29.99
Current children cumulated vsize (Kb) 15260

[startup+40.0043 s]
Raw data (loadavg): 0.90 0.94 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 4679 0 0 0 3986 13 0 0 25 0 1 0 21202059 16302080 3236 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 3980 3236 364 364 0 3616 0
[pid=7389] vsize: 15920
Current children cumulated CPU time (s) 39.99
Current children cumulated vsize (Kb) 15920

[startup+50.0051 s]
Raw data (loadavg): 0.91 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 4931 0 0 0 4985 14 0 0 25 0 1 0 21202059 16977920 3483 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 4145 3483 364 364 0 3781 0
[pid=7389] vsize: 16580
Current children cumulated CPU time (s) 49.99
Current children cumulated vsize (Kb) 16580

[startup+60.006 s]
Raw data (loadavg): 0.92 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 5154 0 0 0 5984 14 0 0 25 0 1 0 21202059 17518592 3703 4294967295 134512640 135987407 3221224576 3221221888 134555861 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 4277 3703 364 364 0 3913 0
[pid=7389] vsize: 17108
Current children cumulated CPU time (s) 59.98
Current children cumulated vsize (Kb) 17108

[startup+70.0058 s]
Raw data (loadavg): 0.94 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 5359 0 0 0 6984 15 0 0 25 0 1 0 21202059 18059264 3904 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 4409 3904 364 364 0 4045 0
[pid=7389] vsize: 17636
Current children cumulated CPU time (s) 69.99
Current children cumulated vsize (Kb) 17636

[startup+80.0067 s]
Raw data (loadavg): 0.95 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 5550 0 0 0 7983 15 0 0 25 0 1 0 21202059 18599936 4092 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 4541 4092 364 364 0 4177 0
[pid=7389] vsize: 18164
Current children cumulated CPU time (s) 79.98
Current children cumulated vsize (Kb) 18164

[startup+90.0065 s]
Raw data (loadavg): 0.95 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 5732 0 0 0 8983 16 0 0 25 0 1 0 21202059 19005440 4271 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 4640 4271 364 364 0 4276 0
[pid=7389] vsize: 18560
Current children cumulated CPU time (s) 89.99
Current children cumulated vsize (Kb) 18560

[startup+100.007 s]
Raw data (loadavg): 0.96 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 6591 0 0 0 9980 18 0 0 25 0 1 0 21202059 22495232 5128 4294967295 134512640 135987407 3221224576 3221221968 134615250 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 5492 5128 364 364 0 5128 0
[pid=7389] vsize: 21968
Current children cumulated CPU time (s) 99.98
Current children cumulated vsize (Kb) 21968

[startup+110.008 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 6820 0 0 0 10975 22 0 0 25 0 1 0 21202059 24076288 5357 4294967295 134512640 135987407 3221224576 3221221888 134555870 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 5878 5357 364 364 0 5514 0
[pid=7389] vsize: 23512
Current children cumulated CPU time (s) 109.97
Current children cumulated vsize (Kb) 23512

[startup+120.009 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 21543 0 0 0 11936 59 0 0 25 0 1 0 21202059 72876032 17054 4294967295 134512640 135987407 3221224576 3220596816 134856397 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 17792 17054 364 364 0 17428 0
[pid=7389] vsize: 71168
Current children cumulated CPU time (s) 119.95
Current children cumulated vsize (Kb) 71168

[startup+130.01 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 55853 0 0 0 12854 137 0 0 25 0 1 0 21202059 177115136 39228 4294967295 134512640 135987407 3221224576 3206232448 134866075 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 43241 39228 364 364 0 42877 0
[pid=7389] vsize: 172964
Current children cumulated CPU time (s) 129.91
Current children cumulated vsize (Kb) 172964

[startup+140.01 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 93832 0 0 0 13761 226 0 0 25 0 1 0 21202059 303034368 61140 4294967295 134512640 135987407 3221224576 3203638608 134878060 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 73983 61140 364 364 0 73619 0
[pid=7389] vsize: 295932
Current children cumulated CPU time (s) 139.87
Current children cumulated vsize (Kb) 295932

[startup+150.011 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 123742 0 0 0 14688 297 0 0 25 0 1 0 21202059 409628672 78566 4294967295 134512640 135987407 3221224576 3221200412 135480876 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 100007 78566 364 364 0 99643 0
[pid=7389] vsize: 400028
Current children cumulated CPU time (s) 149.85
Current children cumulated vsize (Kb) 400028

[startup+160.011 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 144750 0 0 0 15636 346 0 0 25 0 1 0 21202059 438284288 99328 4294967295 134512640 135987407 3221224576 3220696676 135478476 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 107003 99328 364 364 0 106639 0
[pid=7389] vsize: 428012
Current children cumulated CPU time (s) 159.82
Current children cumulated vsize (Kb) 428012

[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 199250 0 0 0 16517 459 0 0 25 0 1 0 21202059 775532544 134231 4294967295 134512640 135987407 3221224576 3215821440 134887487 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 189339 134231 364 364 0 188975 0
[pid=7389] vsize: 757356
Current children cumulated CPU time (s) 169.76
Current children cumulated vsize (Kb) 757356

[startup+180.012 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 226919 0 0 0 17453 522 0 0 25 0 1 0 21202059 728829952 137132 4294967295 134512640 135987407 3221224576 3213542816 134556288 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 177937 137132 364 364 0 177573 0
[pid=7389] vsize: 711748
Current children cumulated CPU time (s) 179.75
Current children cumulated vsize (Kb) 711748

[startup+190.013 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 246925 0 0 0 18404 570 0 0 25 0 1 0 21202059 754647040 156900 4294967295 134512640 135987407 3221224576 3216453712 134640151 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 184240 156900 364 364 0 183876 0
[pid=7389] vsize: 736960
Current children cumulated CPU time (s) 189.74
Current children cumulated vsize (Kb) 736960

[startup+200.014 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 266666 0 0 0 19355 616 0 0 25 0 1 0 21202059 780058624 176408 4294967295 134512640 135987407 3221224576 3220993592 135499909 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 190444 176408 364 364 0 190080 0
[pid=7389] vsize: 761776
Current children cumulated CPU time (s) 199.71
Current children cumulated vsize (Kb) 761776

[startup+210.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 7389
Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 283399 0 0 0 20313 656 0 0 25 0 1 0 21202059 854855680 192950 4294967295 134512640 135987407 3221224576 3218602256 134854972 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7389/statm): 208705 192950 364 364 0 208341 0
[pid=7389] vsize: 834820
Current children cumulated CPU time (s) 209.69
Current children cumulated vsize (Kb) 834820
One traced child (pid=7389) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 219.639
CPU time (s): 219.301
CPU user time (s): 212.187
CPU system time (s): 7.11392
CPU usage (%): 99.8461
Max. virtual memory (cumulated for all children) (Kb): 834820

Verifier Data

ERROR: no interpretation found !