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-p0282.opb
MD5SUMdd62132555621025f45a5a6099c90742
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 258411
Optimality of the best value was proved YES
Number of terms in the objective function 282
Biggest coefficient in the objective function 160646
Number of bits for the biggest coefficient in the objective function 18
Sum of the numbers in the objective function 1302615
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 160646
Number of bits of the biggest number in a constraint 18
Biggest sum of numbers in a constraint 1302615
Number of bits of the biggest sum of numbers21
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark24.5993
Number of variables282
Total number of constraints221
Number of constraints which are clauses177
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints44
Minimum length of a constraint2
Maximum length of a constraint57

Trace number 9725

Launcher Data

LAUNCH ON wulflinc8 THE 2005-09-23 15:15:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8478 boxname=wulflinc8 idbench=274 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd62132555621025f45a5a6099c90742  /oldhome/oroussel/tmp/wulflinc8/normalized-p0282.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc8/normalized-p0282.opb
IDLAUNCH: 8478
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.023
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.023
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:        940208 kB
Buffers:         12388 kB
Cached:          65268 kB
SwapCached:          0 kB
Active:          44880 kB
Inactive:        35584 kB
HighTotal:      131008 kB
HighFree:        61852 kB
LowTotal:       903652 kB
LowFree:        878356 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6972 kB
Slab:             8348 kB
Committed_AS:    63620 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-23 15:17:06 (client local time) WITH STATUS 1 IN 111.279 SECONDS
stats: 8478 7 111.279 1

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...
c got solution with objective value: 744052
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/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 18 0 0 0 0 0 0 0 24 0 1 0 21204033 1527808 2 4294967295 134512640 135987407 3221224576 3221224576 134512928 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 373 2 364 364 0 9 0
[pid=7465] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-p0282.opb

[startup+10.0017 s]
Raw data (loadavg): 0.93 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 31440 0 0 0 921 74 0 0 25 0 1 0 21204033 97292288 20243 4294967295 134512640 135987407 3221224576 3221157232 134878690 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 23753 20243 364 364 0 23389 0
[pid=7465] vsize: 95012
Current children cumulated CPU time (s) 9.95
Current children cumulated vsize (Kb) 95012

[startup+20.0025 s]
Raw data (loadavg): 0.94 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 62346 0 0 0 1853 139 0 0 25 0 1 0 21204033 193257472 39936 4294967295 134512640 135987407 3221224576 3221160064 134559186 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 47182 39936 364 364 0 46818 0
[pid=7465] vsize: 188728
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 188728

[startup+30.0032 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 105037 0 0 0 2765 225 0 0 25 0 1 0 21204033 325677056 60432 4294967295 134512640 135987407 3221224576 3221176620 135500006 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 79511 60432 364 364 0 79147 0
[pid=7465] vsize: 318044
Current children cumulated CPU time (s) 29.9
Current children cumulated vsize (Kb) 318044

[startup+40.003 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 123026 0 0 0 3724 265 0 0 25 0 1 0 21204033 383561728 78208 4294967295 134512640 135987407 3221224576 3221168656 134878060 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 93643 78208 364 364 0 93279 0
[pid=7465] vsize: 374572
Current children cumulated CPU time (s) 39.89
Current children cumulated vsize (Kb) 374572

[startup+50.0038 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 146802 0 0 0 4674 312 0 0 25 0 1 0 21204033 559157248 101569 4294967295 134512640 135987407 3221224576 3221188768 134856690 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 136513 101569 364 364 0 136149 0
[pid=7465] vsize: 546052
Current children cumulated CPU time (s) 49.86
Current children cumulated vsize (Kb) 546052

[startup+60.0046 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 207255 0 0 0 5541 440 0 0 25 0 1 0 21204033 646516736 118063 4294967295 134512640 135987407 3221224576 3221182860 134669188 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 157841 118063 364 364 0 157477 0
[pid=7465] vsize: 631364
Current children cumulated CPU time (s) 59.81
Current children cumulated vsize (Kb) 631364

[startup+70.0054 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 223469 0 0 0 6505 474 0 0 25 0 1 0 21204033 702382080 134087 4294967295 134512640 135987407 3221224576 3221188240 134537488 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 171480 134087 364 364 0 171116 0
[pid=7465] vsize: 685920
Current children cumulated CPU time (s) 69.79
Current children cumulated vsize (Kb) 685920

[startup+80.0071 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 242045 0 0 0 7466 511 0 0 25 0 1 0 21204033 726999040 152440 4294967295 134512640 135987407 3221224576 3221201148 135500014 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 177490 152440 364 364 0 177126 0
[pid=7465] vsize: 709960
Current children cumulated CPU time (s) 79.77
Current children cumulated vsize (Kb) 709960

[startup+90.0069 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 260270 0 0 0 8429 546 0 0 25 0 1 0 21204033 750653440 170446 4294967295 134512640 135987407 3221224576 3221187540 134636948 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 183265 170446 364 364 0 182901 0
[pid=7465] vsize: 733060
Current children cumulated CPU time (s) 89.75
Current children cumulated vsize (Kb) 733060

[startup+100.007 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 274880 0 0 0 9397 576 0 0 25 0 1 0 21204033 820318208 184878 4294967295 134512640 135987407 3221224576 3221193244 134637002 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 200273 184878 364 364 0 199909 0
[pid=7465] vsize: 801092
Current children cumulated CPU time (s) 99.73
Current children cumulated vsize (Kb) 801092

[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 7465
Raw data (/proc/7465/stat): 7465 (pb2sat) R 7464 7465 4060 0 -1 0 282675 0 0 0 10363 610 0 0 25 0 1 0 21204033 470564864 114399 4294967295 134512640 135987407 3221224576 3221223424 134884004 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7465/statm): 114884 114399 364 364 0 114520 0
[pid=7465] vsize: 459536
Current children cumulated CPU time (s) 109.73
Current children cumulated vsize (Kb) 459536
One traced child (pid=7465) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 111.555
CPU time (s): 111.279
CPU user time (s): 104.932
CPU system time (s): 6.34704
CPU usage (%): 99.7524
Max. virtual memory (cumulated for all children) (Kb): 801092

Verifier Data

ERROR: no interpretation found !