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-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-swath1.opb
MD5SUMd4e99ebd08b929dc4252a5f0acf82be9
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 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 1048576000000
Number of bits of the biggest number in a constraint 40
Biggest sum of numbers in a constraint 203989830597156
Number of bits of the biggest sum of numbers48
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables39271
Total number of constraints7608
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)2495
Number of constraints which are nor clauses,nor cardinality constraints5113
Minimum length of a constraint1
Maximum length of a constraint37670

Trace number 10566

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-23 19:05:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=9328 boxname=wulflinc27 idbench=1124 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d4e99ebd08b929dc4252a5f0acf82be9  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-swath1.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-swath1.opb
IDLAUNCH: 9328
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.039
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.039
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:        921256 kB
Buffers:         12752 kB
Cached:          83264 kB
SwapCached:          0 kB
Active:          50968 kB
Inactive:        47964 kB
HighTotal:      131008 kB
HighFree:        43316 kB
LowTotal:       903652 kB
LowFree:        877940 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6984 kB
Slab:             8864 kB
Committed_AS:    63660 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-23 19:07:40 (client local time) WITH STATUS 1 IN 132.99 SECONDS
stats: 9328 7 132.99 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/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22534037 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 373 2 364 364 0 9 0
[pid=11642] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-swath1.opb

[startup+10.0026 s]
Raw data (loadavg): 0.93 0.95 0.92 2/55 11642
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 8463 0 0 0 976 21 0 0 25 0 1 0 22534037 27873280 5177 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 6805 5177 364 364 0 6441 0
[pid=11642] vsize: 27220
Current children cumulated CPU time (s) 9.97
Current children cumulated vsize (Kb) 27220

[startup+20.0034 s]
Raw data (loadavg): 0.94 0.96 0.92 2/55 11642
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 8508 0 0 0 1976 21 0 0 25 0 1 0 22534037 27873280 5222 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 6805 5222 364 364 0 6441 0
[pid=11642] vsize: 27220
Current children cumulated CPU time (s) 19.97
Current children cumulated vsize (Kb) 27220

[startup+30.0043 s]
Raw data (loadavg): 0.95 0.96 0.92 2/55 11642
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 11883 0 0 0 2968 29 0 0 25 0 1 0 22534037 41148416 8464 4294967295 134512640 135987407 3221224560 3210497356 135499901 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 10046 8464 364 364 0 9682 0
[pid=11642] vsize: 40184
Current children cumulated CPU time (s) 29.97
Current children cumulated vsize (Kb) 40184

[startup+40.0051 s]
Raw data (loadavg): 0.95 0.96 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 45383 0 0 0 3886 107 0 0 25 0 1 0 22534037 149590016 29065 4294967295 134512640 135987407 3221224560 3208932284 135499901 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 36521 29065 364 364 0 36157 0
[pid=11642] vsize: 146084
Current children cumulated CPU time (s) 39.93
Current children cumulated vsize (Kb) 146084

[startup+50.0059 s]
Raw data (loadavg): 0.96 0.96 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 76624 0 0 0 4817 173 0 0 25 0 1 0 22534037 301768704 53647 4294967295 134512640 135987407 3221224560 3209541824 134856568 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 73674 53647 364 364 0 73310 0
[pid=11642] vsize: 294696
Current children cumulated CPU time (s) 49.9
Current children cumulated vsize (Kb) 294696

[startup+60.0067 s]
Raw data (loadavg): 0.97 0.96 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 107899 0 0 0 5750 238 0 0 25 0 1 0 22534037 399560704 75275 4294967295 134512640 135987407 3221224560 3208634816 134887487 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 97549 75275 364 364 0 97185 0
[pid=11642] vsize: 390196
Current children cumulated CPU time (s) 59.88
Current children cumulated vsize (Kb) 390196

[startup+70.0065 s]
Raw data (loadavg): 0.97 0.96 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 127798 0 0 0 6705 280 0 0 25 0 1 0 22534037 409948160 82665 4294967295 134512640 135987407 3221224560 3208942896 134636933 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 100085 82665 364 364 0 99721 0
[pid=11642] vsize: 400340
Current children cumulated CPU time (s) 69.85
Current children cumulated vsize (Kb) 400340

[startup+80.0084 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 169397 0 0 0 7616 364 0 0 25 0 1 0 22534037 545460224 104646 4294967295 134512640 135987407 3221224560 3209000668 135479982 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 133169 104646 364 364 0 132805 0
[pid=11642] vsize: 532676
Current children cumulated CPU time (s) 79.8
Current children cumulated vsize (Kb) 532676

[startup+90.0092 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 187241 0 0 0 8576 401 0 0 25 0 1 0 22534037 571547648 122246 4294967295 134512640 135987407 3221224560 3208803952 134931315 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 139538 122246 364 364 0 139174 0
[pid=11642] vsize: 558152
Current children cumulated CPU time (s) 89.77
Current children cumulated vsize (Kb) 558152

[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 226895 0 0 0 9492 484 0 0 25 0 1 0 22534037 694378496 137118 4294967295 134512640 135987407 3221224560 3208983872 134537491 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 169526 137118 364 364 0 169162 0
[pid=11642] vsize: 678104
Current children cumulated CPU time (s) 99.76
Current children cumulated vsize (Kb) 678104

[startup+110.01 s]
Raw data (loadavg): 0.98 0.96 0.92 1/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) T 11641 11642 4005 0 -1 0 241594 0 0 0 10459 517 0 0 25 0 1 0 22534037 749424640 151616 4294967295 134512640 135987407 3221224560 3209358460 135635874 0 0 5 16384 3222434794 0 0 17 0 0 0
Raw data (/proc/11642/statm): 182965 151616 364 364 0 182601 0
[pid=11642] vsize: 731860
Current children cumulated CPU time (s) 109.76
Current children cumulated vsize (Kb) 731860

[startup+120.089 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 260486 0 0 0 11416 559 0 0 25 0 1 0 22534037 781492224 170272 4294967295 134512640 135987407 3221224560 3208817184 134640194 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 190794 170272 364 364 0 190430 0
[pid=11642] vsize: 763176
Current children cumulated CPU time (s) 119.75
Current children cumulated vsize (Kb) 763176

[startup+130.089 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 11644
Raw data (/proc/11642/stat): 11642 (pb2sat) R 11641 11642 4005 0 -1 0 264962 0 0 0 12394 580 0 0 25 0 1 0 22534037 478396416 116344 4294967295 134512640 135987407 3221224560 3221223224 135477320 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/11642/statm): 116796 116344 364 364 0 116432 0
[pid=11642] vsize: 467184
Current children cumulated CPU time (s) 129.74
Current children cumulated vsize (Kb) 467184
One traced child (pid=11642) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 133.338
CPU time (s): 132.99
CPU user time (s): 126.945
CPU system time (s): 6.04508
CPU usage (%): 99.7391
Max. virtual memory (cumulated for all children) (Kb): 763176

Verifier Data

ERROR: no interpretation found !