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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.95:98.opb
MD5SUM5f5bedf3690a537deb8cc97cc5d565ae
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 148
Optimality of the best value was proved NO
Number of terms in the objective function 4624
Biggest coefficient in the objective function 2577
Number of bits for the biggest coefficient in the objective function 12
Sum of the numbers in the objective function 13335
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 2577
Number of bits of the biggest number in a constraint 12
Biggest sum of numbers in a constraint 13335
Number of bits of the biggest sum of numbers14
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1226.76
Number of variables4624
Total number of constraints9886
Number of constraints which are clauses4404
Number of constraints which are cardinality constraints (but not clauses)5482
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint22

Trace number 9846

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-23 15:58:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8603 boxname=wulflinc21 idbench=399 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5f5bedf3690a537deb8cc97cc5d565ae  /oldhome/oroussel/tmp/wulflinc21/normalized-30:30:4.5:0.95:98.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc21/normalized-30:30:4.5:0.95:98.opb
IDLAUNCH: 8603
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.188
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.188
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:        935132 kB
Buffers:         13288 kB
Cached:          68380 kB
SwapCached:          0 kB
Active:          45772 kB
Inactive:        38788 kB
HighTotal:      131008 kB
HighFree:        58296 kB
LowTotal:       903652 kB
LowFree:        876836 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6980 kB
Slab:             9452 kB
Committed_AS:    63624 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-23 16:00:37 (client local time) WITH STATUS 1 IN 111.485 SECONDS
stats: 8603 7 111.485 1

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...
c got solution with objective value: 6106
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/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 18 0 0 0 0 0 0 0 24 0 1 0 21449405 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 373 2 364 364 0 9 0
[pid=8368] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-30:30:4.5:0.95:98.opb

[startup+10.002 s]
Raw data (loadavg): 0.92 0.95 0.96 2/55 8368
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 29372 0 0 0 917 72 0 0 25 0 1 0 21449405 95584256 18183 4294967295 134512640 135987407 3221224560 3220861412 134558838 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 23336 18183 364 364 0 22972 0
[pid=8368] vsize: 93344
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 93344

[startup+20.0027 s]
Raw data (loadavg): 0.93 0.96 0.96 2/55 8368
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 60150 0 0 0 1850 137 0 0 25 0 1 0 21449405 190869504 37750 4294967295 134512640 135987407 3221224560 3220431324 134789772 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 46599 37750 364 364 0 46235 0
[pid=8368] vsize: 186396
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 186396

[startup+30.0034 s]
Raw data (loadavg): 0.94 0.96 0.96 2/55 8368
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 102811 0 0 0 2760 224 0 0 25 0 1 0 21449405 322744320 58218 4294967295 134512640 135987407 3221224560 3220530540 134892452 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 78795 58218 364 364 0 78431 0
[pid=8368] vsize: 315180
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 315180

[startup+40.0041 s]
Raw data (loadavg): 0.95 0.96 0.96 2/55 8368
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 120412 0 0 0 3718 264 0 0 25 0 1 0 21449405 379006976 75607 4294967295 134512640 135987407 3221224560 3220000808 134930929 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 92531 75607 364 364 0 92167 0
[pid=8368] vsize: 370124
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 370124

[startup+50.0047 s]
Raw data (loadavg): 0.96 0.96 0.96 2/55 8368
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 139022 0 0 0 4677 303 0 0 25 0 1 0 21449405 403066880 93994 4294967295 134512640 135987407 3221224560 3220683932 134637002 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 98405 93994 364 364 0 98041 0
[pid=8368] vsize: 393620
Current children cumulated CPU time (s) 49.8
Current children cumulated vsize (Kb) 393620

[startup+60.0054 s]
Raw data (loadavg): 0.96 0.96 0.96 2/55 8368
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 204938 0 0 0 5537 438 0 0 25 0 1 0 21449405 642486272 115761 4294967295 134512640 135987407 3221224560 3220019184 134855042 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 156857 115761 364 364 0 156493 0
[pid=8368] vsize: 627428
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 627428

[startup+70.0061 s]
Raw data (loadavg): 0.97 0.96 0.96 2/55 8368
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 220733 0 0 0 6500 473 0 0 25 0 1 0 21449405 696315904 131367 4294967295 134512640 135987407 3221224560 3220825396 134636948 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 169999 131367 364 364 0 169635 0
[pid=8368] vsize: 679996
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 679996

[startup+80.0068 s]
Raw data (loadavg): 0.97 0.96 0.96 2/55 8368
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 238891 0 0 0 7461 510 0 0 25 0 1 0 21449405 719835136 149307 4294967295 134512640 135987407 3221224560 3221212156 135480732 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 175741 149307 364 364 0 175377 0
[pid=8368] vsize: 702964
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 702964

[startup+90.0075 s]
Raw data (loadavg): 1.05 0.98 0.96 2/55 8423
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 256703 0 0 0 8415 554 0 0 25 0 1 0 21449405 742813696 166905 4294967295 134512640 135987407 3221224560 3220284460 135482121 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 181351 166905 364 364 0 180987 0
[pid=8368] vsize: 725404
Current children cumulated CPU time (s) 89.69
Current children cumulated vsize (Kb) 725404

[startup+100.007 s]
Raw data (loadavg): 1.04 0.98 0.96 2/55 8423
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 271095 0 0 0 9383 584 0 0 25 0 1 0 21449405 811798528 181124 4294967295 134512640 135987407 3221224560 3220248684 135482121 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 198193 181124 364 364 0 197829 0
[pid=8368] vsize: 792772
Current children cumulated CPU time (s) 99.67
Current children cumulated vsize (Kb) 792772

[startup+110.008 s]
Raw data (loadavg): 1.04 0.98 0.96 2/55 8423
Raw data (/proc/8368/stat): 8368 (pb2sat) R 8367 8368 4059 0 -1 0 283491 0 0 0 10358 607 0 0 25 0 1 0 21449405 829202432 193373 4294967295 134512640 135987407 3221224560 3221223380 135479922 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/8368/statm): 202442 193373 364 364 0 202078 0
[pid=8368] vsize: 809768
Current children cumulated CPU time (s) 109.65
Current children cumulated vsize (Kb) 809768
One traced child (pid=8368) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 111.843
CPU time (s): 111.485
CPU user time (s): 105.022
CPU system time (s): 6.46302
CPU usage (%): 99.6799
Max. virtual memory (cumulated for all children) (Kb): 809768

Verifier Data

ERROR: no interpretation found !