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/MIPLIB/miplib/normalized-mps-v2-20-10-p0548.opb
MD5SUM6f47095f2d417d23ced995954e641689
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 18719
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
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 benchmark1195.08
Number of variables548
Total number of constraints724
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)550
Number of constraints which are nor clauses,nor cardinality constraints134
Minimum length of a constraint1
Maximum length of a constraint143

Trace number 9989

Launcher Data

LAUNCH ON wulflinc23 THE 2005-09-23 16:21:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8737 boxname=wulflinc23 idbench=533 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6f47095f2d417d23ced995954e641689  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 8737
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.185
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.185
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:        919724 kB
Buffers:         14164 kB
Cached:          82736 kB
SwapCached:          0 kB
Active:          59456 kB
Inactive:        40356 kB
HighTotal:      131008 kB
HighFree:        44016 kB
LowTotal:       903652 kB
LowFree:        875708 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6980 kB
Slab:             9564 kB
Committed_AS:    63624 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-23 16:25:33 (client local time) WITH STATUS 1 IN 263.919 SECONDS
stats: 8737 7 263.919 1

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

c Decision: 12464/174694	Time: 102.378/86400
c got solution with objective value: 71025
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/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 18 0 0 0 0 0 0 0 24 0 1 0 21581130 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 373 2 364 364 0 9 0
[pid=7846] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-p0548.opb

[startup+10.0016 s]
Raw data (loadavg): 0.93 0.95 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 29180 0 0 0 926 70 0 0 25 0 1 0 21581130 96296960 17737 4294967295 134512640 135987407 3221224560 3221223120 134788496 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 23510 17737 364 364 0 23146 0
[pid=7846] vsize: 94040
Current children cumulated CPU time (s) 9.96
Current children cumulated vsize (Kb) 94040

[startup+20.0022 s]
Raw data (loadavg): 0.94 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 29981 0 0 0 1923 72 0 0 25 0 1 0 21581130 98942976 18146 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 24156 18146 364 364 0 23792 0
[pid=7846] vsize: 96624
Current children cumulated CPU time (s) 19.95
Current children cumulated vsize (Kb) 96624

[startup+30.0028 s]
Raw data (loadavg): 0.95 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 30784 0 0 0 2918 75 0 0 25 0 1 0 21581130 101777408 18720 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 24848 18720 364 364 0 24484 0
[pid=7846] vsize: 99392
Current children cumulated CPU time (s) 29.93
Current children cumulated vsize (Kb) 99392

[startup+40.0035 s]
Raw data (loadavg): 0.95 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 31236 0 0 0 3913 77 0 0 25 0 1 0 21581130 103698432 19073 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 25317 19073 364 364 0 24953 0
[pid=7846] vsize: 101268
Current children cumulated CPU time (s) 39.9
Current children cumulated vsize (Kb) 101268

[startup+50.0041 s]
Raw data (loadavg): 0.96 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 31400 0 0 0 4908 79 0 0 25 0 1 0 21581130 104501248 19237 4294967295 134512640 135987407 3221224560 3221223248 134811988 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 25513 19237 364 364 0 25149 0
[pid=7846] vsize: 102052
Current children cumulated CPU time (s) 49.87
Current children cumulated vsize (Kb) 102052

[startup+60.0038 s]
Raw data (loadavg): 0.97 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 31417 0 0 0 5900 82 0 0 25 0 1 0 21581130 104697856 19254 4294967295 134512640 135987407 3221224560 3221223376 134824259 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7846/statm): 25561 19254 364 364 0 25197 0
[pid=7846] vsize: 102244
Current children cumulated CPU time (s) 59.82
Current children cumulated vsize (Kb) 102244

[startup+70.0044 s]
Raw data (loadavg): 0.97 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 31423 0 0 0 6893 84 0 0 25 0 1 0 21581130 104697856 19260 4294967295 134512640 135987407 3221224560 3221223248 134812002 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7846/statm): 25561 19260 364 364 0 25197 0
[pid=7846] vsize: 102244
Current children cumulated CPU time (s) 69.77
Current children cumulated vsize (Kb) 102244

[startup+80.005 s]
Raw data (loadavg): 0.98 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 31843 0 0 0 7889 87 0 0 25 0 1 0 21581130 106287104 19549 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 25949 19549 364 364 0 25585 0
[pid=7846] vsize: 103796
Current children cumulated CPU time (s) 79.76
Current children cumulated vsize (Kb) 103796

[startup+90.0057 s]
Raw data (loadavg): 0.98 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 32079 0 0 0 8885 88 0 0 25 0 1 0 21581130 107225088 19752 4294967295 134512640 135987407 3221224560 3221223248 134811775 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 26178 19752 364 364 0 25814 0
[pid=7846] vsize: 104712
Current children cumulated CPU time (s) 89.73
Current children cumulated vsize (Kb) 104712

[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 32165 0 0 0 9882 89 0 0 25 0 1 0 21581130 107356160 19805 4294967295 134512640 135987407 3221224560 3221223248 134811775 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 26210 19805 364 364 0 25846 0
[pid=7846] vsize: 104840
Current children cumulated CPU time (s) 99.71
Current children cumulated vsize (Kb) 104840

[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 32735 0 0 0 10877 92 0 0 25 0 1 0 21581130 109629440 20210 4294967295 134512640 135987407 3221224560 3221223280 134814273 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 26765 20210 364 364 0 26401 0
[pid=7846] vsize: 107060
Current children cumulated CPU time (s) 109.69
Current children cumulated vsize (Kb) 107060

[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 33268 0 0 0 11869 96 0 0 25 0 1 0 21581130 110428160 20368 4294967295 134512640 135987407 3221224560 3221223248 134811773 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 26960 20368 364 364 0 26596 0
[pid=7846] vsize: 107840
Current children cumulated CPU time (s) 119.65
Current children cumulated vsize (Kb) 107840

[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 33420 0 0 0 12863 98 0 0 25 0 1 0 21581130 110960640 20454 4294967295 134512640 135987407 3221224560 3221223248 134811805 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 27090 20454 364 364 0 26726 0
[pid=7846] vsize: 108360
Current children cumulated CPU time (s) 129.61
Current children cumulated vsize (Kb) 108360

[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 33491 0 0 0 13856 100 0 0 25 0 1 0 21581130 111226880 20492 4294967295 134512640 135987407 3221224560 3221223248 134811775 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 27155 20492 364 364 0 26791 0
[pid=7846] vsize: 108620
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 108620

[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 33545 0 0 0 14850 103 0 0 25 0 1 0 21581130 111493120 20546 4294967295 134512640 135987407 3221224560 3221223120 134788496 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7846/statm): 27220 20546 364 364 0 26856 0
[pid=7846] vsize: 108880
Current children cumulated CPU time (s) 149.53
Current children cumulated vsize (Kb) 108880

[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 33813 0 0 0 15844 105 0 0 25 0 1 0 21581130 112820224 20748 4294967295 134512640 135987407 3221224560 3221223248 134811741 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7846/statm): 27544 20748 364 364 0 27180 0
[pid=7846] vsize: 110176
Current children cumulated CPU time (s) 159.49
Current children cumulated vsize (Kb) 110176

[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 56268 0 0 0 16793 153 0 0 25 0 1 0 21581130 187265024 32044 4294967295 134512640 135987407 3221224560 3221165708 134669200 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 45719 32044 364 364 0 45355 0
[pid=7846] vsize: 182876
Current children cumulated CPU time (s) 169.46
Current children cumulated vsize (Kb) 182876

[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 88262 0 0 0 17726 217 0 0 25 0 1 0 21581130 270843904 54112 4294967295 134512640 135987407 3221224560 3221146860 134636987 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 66124 54112 364 364 0 65760 0
[pid=7846] vsize: 264496
Current children cumulated CPU time (s) 179.43
Current children cumulated vsize (Kb) 264496

[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 117332 0 0 0 18665 276 0 0 25 0 1 0 21581130 376897536 70692 4294967295 134512640 135987407 3221224560 3221192928 134537477 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 92016 70692 364 364 0 91652 0
[pid=7846] vsize: 368064
Current children cumulated CPU time (s) 189.41
Current children cumulated vsize (Kb) 368064

[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 136641 0 0 0 19625 315 0 0 25 0 1 0 21581130 401903616 89769 4294967295 134512640 135987407 3221224560 3221214448 134789843 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 98121 89769 364 364 0 97757 0
[pid=7846] vsize: 392484
Current children cumulated CPU time (s) 199.4
Current children cumulated vsize (Kb) 392484

[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 202282 0 0 0 20481 455 0 0 25 0 1 0 21581130 640110592 111261 4294967295 134512640 135987407 3221224560 3221188576 134636919 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 156277 111261 364 364 0 155913 0
[pid=7846] vsize: 625108
Current children cumulated CPU time (s) 209.36
Current children cumulated vsize (Kb) 625108

[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 218616 0 0 0 21444 491 0 0 25 0 1 0 21581130 695562240 127401 4294967295 134512640 135987407 3221224560 3221148500 135478543 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 169815 127401 364 364 0 169451 0
[pid=7846] vsize: 679260
Current children cumulated CPU time (s) 219.35
Current children cumulated vsize (Kb) 679260

[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 237452 0 0 0 22403 529 0 0 25 0 1 0 21581130 720162816 146012 4294967295 134512640 135987407 3221224560 3221206000 134640497 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 175821 146012 364 364 0 175457 0
[pid=7846] vsize: 703284
Current children cumulated CPU time (s) 229.32
Current children cumulated vsize (Kb) 703284

[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 256283 0 0 0 23361 569 0 0 25 0 1 0 21581130 744493056 164617 4294967295 134512640 135987407 3221224560 3221199116 135499880 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 181761 164617 364 364 0 181397 0
[pid=7846] vsize: 727044
Current children cumulated CPU time (s) 239.3
Current children cumulated vsize (Kb) 727044

[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 271005 0 0 0 24329 600 0 0 25 0 1 0 21581130 814018560 179162 4294967295 134512640 135987407 3221224560 3221213092 135479935 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 198735 179162 364 364 0 198371 0
[pid=7846] vsize: 794940
Current children cumulated CPU time (s) 249.29
Current children cumulated vsize (Kb) 794940

[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7846
Raw data (/proc/7846/stat): 7846 (pb2sat) R 7845 7846 4060 0 -1 0 285129 0 0 0 25300 627 0 0 25 0 1 0 21581130 834531328 193122 4294967295 134512640 135987407 3221224560 3221223380 135479922 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7846/statm): 203743 193122 364 364 0 203379 0
[pid=7846] vsize: 814972
Current children cumulated CPU time (s) 259.27
Current children cumulated vsize (Kb) 814972
One traced child (pid=7846) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 264.655
CPU time (s): 263.919
CPU user time (s): 257.239
CPU system time (s): 6.67998
CPU usage (%): 99.7218
Max. virtual memory (cumulated for all children) (Kb): 814972

Verifier Data

ERROR: no interpretation found !