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/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-bnl1.opb
MD5SUMbdc6ebf164274793ca5e27f860835212
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 29490
Biggest coefficient in the objective function 12938266856652800
Number of bits for the biggest coefficient in the objective function 54
Sum of the numbers in the objective function 1063579760735919966
Number of bits of the sum of numbers in the objective function 60
Biggest number in a constraint 12938266856652800
Number of bits of the biggest number in a constraint 54
Biggest sum of numbers in a constraint 1063579760735919966
Number of bits of the biggest sum of numbers60
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables35250
Total number of constraints632
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints632
Minimum length of a constraint30
Maximum length of a constraint2280

Trace number 9861

Launcher Data

LAUNCH ON wulflinc19 THE 2005-09-23 16:01:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8616 boxname=wulflinc19 idbench=412 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bdc6ebf164274793ca5e27f860835212  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-bnl1.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-bnl1.opb
IDLAUNCH: 8616
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        922840 kB
Buffers:         15208 kB
Cached:          76660 kB
SwapCached:          0 kB
Active:          49952 kB
Inactive:        44844 kB
HighTotal:      131008 kB
HighFree:        50876 kB
LowTotal:       903652 kB
LowFree:        871964 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6980 kB
Slab:            11404 kB
Committed_AS:    63660 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-23 16:03:54 (client local time) WITH STATUS 1 IN 126.342 SECONDS
stats: 8616 7 126.342 1

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified

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

[startup+10.0019 s]
Raw data (loadavg): 0.93 0.95 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 2568 0 0 0 990 8 0 0 25 0 1 0 21468559 9506816 1881 4294967295 134512640 135987407 3221224560 3221221872 134555870 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7461/statm): 2321 1881 364 364 0 1957 0
[pid=7461] vsize: 9284
Current children cumulated CPU time (s) 9.98
Current children cumulated vsize (Kb) 9284

[startup+20.0027 s]
Raw data (loadavg): 0.94 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 17087 0 0 0 1957 41 0 0 25 0 1 0 21468559 69169152 11381 4294967295 134512640 135987407 3221224560 3221142556 135500012 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7461/statm): 16887 11381 364 364 0 16523 0
[pid=7461] vsize: 67548
Current children cumulated CPU time (s) 19.98
Current children cumulated vsize (Kb) 67548

[startup+30.0025 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 52078 0 0 0 2880 114 0 0 25 0 1 0 21468559 162156544 29711 4294967295 134512640 135987407 3221224560 3221144380 134636964 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7461/statm): 39589 29711 364 364 0 39225 0
[pid=7461] vsize: 158356
Current children cumulated CPU time (s) 29.94
Current children cumulated vsize (Kb) 158356

[startup+40.0033 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 83047 0 0 0 3817 175 0 0 25 0 1 0 21468559 262582272 50766 4294967295 134512640 135987407 3221224560 3221145280 134856467 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7461/statm): 64107 50766 364 364 0 63743 0
[pid=7461] vsize: 256428
Current children cumulated CPU time (s) 39.92
Current children cumulated vsize (Kb) 256428

[startup+50.0041 s]
Raw data (loadavg): 0.96 0.96 0.95 1/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) T 7460 7461 4060 0 -1 0 111110 0 0 0 4755 234 0 0 25 0 1 0 21468559 367439872 66346 4294967295 134512640 135987407 3221224560 3221148732 135635874 0 0 5 16384 3222434794 0 0 17 0 0 0
Raw data (/proc/7461/statm): 89707 66346 364 364 0 89343 0
[pid=7461] vsize: 358828
Current children cumulated CPU time (s) 49.89
Current children cumulated vsize (Kb) 358828

[startup+60.0039 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 129769 0 0 0 5718 270 0 0 25 0 1 0 21468559 393981952 84782 4294967295 134512640 135987407 3221224560 3221146764 135482121 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7461/statm): 96187 84782 364 364 0 95823 0
[pid=7461] vsize: 384748
Current children cumulated CPU time (s) 59.88
Current children cumulated vsize (Kb) 384748

[startup+70.0037 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 172788 0 0 0 6629 354 0 0 25 0 1 0 21468559 533839872 108200 4294967295 134512640 135987407 3221224560 3221147152 134887887 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7461/statm): 130332 108200 364 364 0 129968 0
[pid=7461] vsize: 521328
Current children cumulated CPU time (s) 69.83
Current children cumulated vsize (Kb) 521328

[startup+80.0036 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 212637 0 0 0 7546 436 0 0 25 0 1 0 21468559 654778368 123284 4294967295 134512640 135987407 3221224560 3221150704 134878060 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7461/statm): 159858 123285 364 364 0 159494 0
[pid=7461] vsize: 639432
Current children cumulated CPU time (s) 79.82
Current children cumulated vsize (Kb) 639432

[startup+90.0044 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 228263 0 0 0 8512 468 0 0 25 0 1 0 21468559 710602752 138725 4294967295 134512640 135987407 3221224560 3221152452 134636948 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7461/statm): 173487 138726 364 364 0 173123 0
[pid=7461] vsize: 693948
Current children cumulated CPU time (s) 89.8
Current children cumulated vsize (Kb) 693948

[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 246883 0 0 0 9471 506 0 0 25 0 1 0 21468559 736907264 157124 4294967295 134512640 135987407 3221224560 3221150800 134537491 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7461/statm): 179909 157124 364 364 0 179545 0
[pid=7461] vsize: 719636
Current children cumulated CPU time (s) 99.77
Current children cumulated vsize (Kb) 719636

[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 265388 0 0 0 10434 542 0 0 25 0 1 0 21468559 762744832 175407 4294967295 134512640 135987407 3221224560 3221152288 134854865 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7461/statm): 186217 175408 364 364 0 185853 0
[pid=7461] vsize: 744868
Current children cumulated CPU time (s) 109.76
Current children cumulated vsize (Kb) 744868

[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7461
Raw data (/proc/7461/stat): 7461 (pb2sat) R 7460 7461 4060 0 -1 0 278588 0 0 0 11408 566 0 0 25 0 1 0 21468559 831217664 188331 4294967295 134512640 135987407 3221224560 3221222828 134636908 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7461/statm): 202934 188331 364 364 0 202570 0
[pid=7461] vsize: 811736
Current children cumulated CPU time (s) 119.74
Current children cumulated vsize (Kb) 811736
One traced child (pid=7461) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 126.599
CPU time (s): 126.342
CPU user time (s): 120.289
CPU system time (s): 6.05308
CPU usage (%): 99.7966
Max. virtual memory (cumulated for all children) (Kb): 811736

Verifier Data

ERROR: no interpretation found !