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).
  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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-gt2.opb
MD5SUMf1382105ee9fb79777762a53cf6a73c1
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 21166
Optimality of the best value was proved NO
Number of terms in the objective function 304
Biggest coefficient in the objective function 62376
Number of bits for the biggest coefficient in the objective function 16
Sum of the numbers in the objective function 3092598
Number of bits of the sum of numbers in the objective function 22
Biggest number in a constraint 62376
Number of bits of the biggest number in a constraint 16
Biggest sum of numbers in a constraint 3092598
Number of bits of the biggest sum of numbers22
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.14
Number of variables556
Total number of constraints217
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)26
Number of constraints which are nor clauses,nor cardinality constraints191
Minimum length of a constraint1
Maximum length of a constraint48

Trace number 25667 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-21 15:02:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18436 boxname=wulflinc31 idbench=1419 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  f1382105ee9fb79777762a53cf6a73c1  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-gt2.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-gt2.opb
IDLAUNCH: 18436
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        893360 kB
Buffers:         24224 kB
Cached:          96284 kB
SwapCached:       1076 kB
Active:          58368 kB
Inactive:        64496 kB
HighTotal:      131008 kB
HighFree:        65996 kB
LowTotal:       903652 kB
LowFree:        827364 kB
SwapTotal:     2097892 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5356 kB
Slab:            12832 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-21 15:07:43 (client local time) WITH STATUS 0 IN 330.231 SECONDS
stats: 18436 7 330.231 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c Initial problem consists of 556 variables and 180 constraints.
c After prepocess the problem consists of 556 variables and 193 constraints.
c preprocess terminated 0.777 s
c Initial Lower Bound: 17011
c Lower Bound Elapsed time: 0.1008
c Use computed LB before first solution.
c NEW SOLUTION FOUND: 267669 @ 22.109
c NEW SOLUTION FOUND: 262111 @ 24.574
c NEW SOLUTION FOUND: 261469 @ 24.72

    c  Warning: NO Unit Constraints after backtrack??
	Continuing Execution....


c NEW SOLUTION FOUND: 260717 @ 45.033
c NEW SOLUTION FOUND: 257617 @ 46.632

    c  Warning: NO Unit Constraints after backtrack??
	Continuing Execution....


c NEW SOLUTION FOUND: 255169 @ 107.432
c NEW SOLUTION FOUND: 254507 @ 107.461
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.99 0.99 2/55 12061
Raw data (stat): 12061 (runsolver) R 12060 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 805219536 1056768 100 4294967295 134512640 135381576 3221221680 3221216896 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 3178 0 0 0 986 10 0 0 25 0 1 0 805219536 11984896 2240 4294967295 134512640 134714508 3221221776 3221219560 1077410205 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 2926 2240 1111 63 0 2863 0
vsize: 11704
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 3179 0 0 0 1985 11 0 0 25 0 1 0 805219536 11984896 2241 4294967295 134512640 134714508 3221221776 3221219980 1074152822 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 2926 2241 1111 63 0 2863 0
vsize: 11704
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 11201 0 0 0 2956 39 0 0 25 0 1 0 805219536 13971456 2728 4294967295 134512640 134714508 3221221776 3221219440 1074866649 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 3485 2731 1111 63 0 3422 0
vsize: 13644
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 25039 0 0 0 3913 82 0 0 25 0 1 0 805219536 15945728 3147 4294967295 134512640 134714508 3221221776 3221218016 1075115709 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 3893 3147 1111 63 0 3830 0
vsize: 15572
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 37930 0 0 0 4876 119 0 0 25 0 1 0 805219536 17178624 3515 4294967295 134512640 134714508 3221221776 3221220192 1074116570 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 4194 3515 1111 63 0 4131 0
vsize: 16776
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 49973 0 0 0 5840 156 0 0 25 0 1 0 805219536 19410944 3979 4294967295 134512640 134714508 3221221776 3221218852 1075863600 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 4739 3979 1111 63 0 4676 0
vsize: 18956
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 64684 0 0 0 6802 195 0 0 25 0 1 0 805219536 20455424 4243 4294967295 134512640 134714508 3221221776 3221217788 1074788959 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 4994 4243 1111 63 0 4931 0
vsize: 19976
[startup+80.0032 s]
Raw data (loadavg): 0.96 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 78986 0 0 0 7762 234 0 0 25 0 1 0 805219536 22167552 4709 4294967295 134512640 134714508 3221221776 3221218016 1075115715 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 5412 4709 1111 63 0 5349 0
vsize: 21648
[startup+90.0056 s]
Raw data (loadavg): 0.96 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 95110 0 0 0 8721 276 0 0 25 0 1 0 805219536 22507520 4822 4294967295 134512640 134714508 3221221776 3221219776 1074918583 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 5495 4822 1111 63 0 5432 0
vsize: 21980
[startup+100.005 s]
Raw data (loadavg): 0.97 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 108937 0 0 0 9687 309 0 0 25 0 1 0 805219536 23830528 5027 4294967295 134512640 134714508 3221221776 3221219416 1075850409 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5818 5027 1111 63 0 5755 0
vsize: 23272
[startup+110.008 s]
Raw data (loadavg): 0.97 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 125461 0 0 0 10646 350 0 0 25 0 1 0 805219536 25423872 5534 4294967295 134512640 134714508 3221221776 3221220024 1074138155 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6207 5534 1111 63 0 6144 0
vsize: 24828
[startup+120.009 s]
Raw data (loadavg): 0.98 0.99 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 141824 0 0 0 11607 390 0 0 25 0 1 0 805219536 26984448 5915 4294967295 134512640 134714508 3221221776 3221220236 1077781665 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6588 5915 1111 63 0 6525 0
vsize: 26352
[startup+130.009 s]
Raw data (loadavg): 1.05 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 159317 0 0 0 12564 433 0 0 25 0 1 0 805219536 28663808 6233 4294967295 134512640 134714508 3221221776 3221219240 1074950096 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6899 6225 1111 63 0 6836 0
vsize: 27992
[startup+140.01 s]
Raw data (loadavg): 1.04 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 172723 0 0 0 13531 466 0 0 25 0 1 0 805219536 29245440 6466 4294967295 134512640 134714508 3221221776 3221219708 1077411564 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7140 6466 1111 63 0 7077 0
vsize: 28560
[startup+150.01 s]
Raw data (loadavg): 1.04 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 187277 0 0 0 14494 504 0 0 25 0 1 0 805219536 29913088 6597 4294967295 134512640 134714508 3221221776 3221220064 1074153782 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7303 6597 1111 63 0 7240 0
vsize: 29212
[startup+160.011 s]
Raw data (loadavg): 1.03 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 207795 0 0 0 15443 555 0 0 25 0 1 0 805219536 31309824 6970 4294967295 134512640 134714508 3221221776 3221219504 1075830006 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7644 6970 1111 63 0 7581 0
vsize: 30576
[startup+170.012 s]
Raw data (loadavg): 1.03 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 228381 0 0 0 16395 603 0 0 25 0 1 0 805219536 34283520 7673 4294967295 134512640 134714508 3221221776 3221218968 1074138315 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8370 7673 1111 63 0 8307 0
vsize: 33480
[startup+180.012 s]
Raw data (loadavg): 1.02 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 240399 0 0 0 17360 638 0 0 25 0 1 0 805219536 34611200 7688 4294967295 134512640 134714508 3221221776 3221218368 1074885298 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8450 7688 1111 63 0 8387 0
vsize: 33800
[startup+190.012 s]
Raw data (loadavg): 1.02 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 254996 0 0 0 18325 674 0 0 25 0 1 0 805219536 35049472 7852 4294967295 134512640 134714508 3221221776 3221219976 1074138265 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8557 7852 1111 63 0 8494 0
vsize: 34228
[startup+200.012 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 264376 0 0 0 19301 698 0 0 25 0 1 0 805219536 35495936 7992 4294967295 134512640 134714508 3221221776 3221220012 1077404781 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8666 7992 1111 63 0 8603 0
vsize: 34664
[startup+210.013 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 282063 0 0 0 20254 745 0 0 25 0 1 0 805219536 36679680 8281 4294967295 134512640 134714508 3221221776 3221219688 1074138300 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8955 8281 1111 63 0 8892 0
vsize: 35820
[startup+220.012 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 12061
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 302929 0 0 0 21201 798 0 0 25 0 1 0 805219536 37818368 8559 4294967295 134512640 134714508 3221221776 3221220000 1074143973 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9233 8559 1111 63 0 9170 0
vsize: 36932
[startup+230.012 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 311661 0 0 0 22181 819 0 0 25 0 1 0 805219536 39399424 8942 4294967295 134512640 134714508 3221221776 3221219776 1074918583 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9619 8942 1111 63 0 9556 0
vsize: 38476
[startup+240.014 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 324278 0 0 0 23151 849 0 0 25 0 1 0 805219536 40652800 9171 4294967295 134512640 134714508 3221221776 3221217660 1074788953 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9925 9171 1111 63 0 9862 0
vsize: 39700
[startup+250.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 336902 0 0 0 24119 881 0 0 25 0 1 0 805219536 40157184 9130 4294967295 134512640 134714508 3221221776 3221220064 1074153782 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9805 9131 1111 63 0 9742 0
vsize: 39216
[startup+260.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 346335 0 0 0 25095 905 0 0 25 0 1 0 805219536 41504768 9162 4294967295 134512640 134714508 3221221776 3221218816 1075971395 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10133 9168 1111 63 0 10070 0
vsize: 40532
[startup+270.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 356619 0 0 0 26069 931 0 0 25 0 1 0 805219536 40394752 9188 4294967295 134512640 134714508 3221221776 3221220560 134622318 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9862 9188 1111 63 0 9799 0
vsize: 39448
[startup+280.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 370889 0 0 0 27035 965 0 0 25 0 1 0 805219536 40394752 9188 4294967295 134512640 134714508 3221221776 3221219776 1074056269 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9862 9188 1111 63 0 9799 0
vsize: 39448
[startup+290.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 378848 0 0 0 28016 985 0 0 25 0 1 0 805219536 41971712 9447 4294967295 134512640 134714508 3221221776 3221217744 1074872824 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10247 9447 1111 63 0 10184 0
vsize: 40988
[startup+300.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 389747 0 0 0 28988 1013 0 0 25 0 1 0 805219536 42995712 9527 4294967295 134512640 134714508 3221221776 3221218896 1074834431 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10497 9527 1111 63 0 10434 0
vsize: 41988
[startup+310.017 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 404539 0 0 0 29951 1049 0 0 25 0 1 0 805219536 43057152 9668 4294967295 134512640 134714508 3221221776 3221218112 1075114265 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10512 9668 1111 63 0 10449 0
vsize: 42048
[startup+320.017 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 414136 0 0 0 30929 1072 0 0 25 0 1 0 805219536 43732992 9866 4294967295 134512640 134714508 3221221776 3221218016 1075115768 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10677 9866 1111 63 0 10614 0
vsize: 42708
[startup+330.016 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 425636 0 0 0 31899 1102 0 0 25 0 1 0 805219536 44163072 9964 4294967295 134512640 134714508 3221221776 3221218004 1075115057 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10782 9964 1111 63 0 10719 0
vsize: 43128
[startup+330.229 s]
Raw data (loadavg): 1.00 1.00 0.99 1/54 12063
Raw data (stat): 12061 (bsolo_lpr_cuts) R 12060 7876 7672 0 -1 0 425636 0 0 0 31899 1102 0 0 25 0 1 0 805219536 44163072 9964 4294967295 134512640 134714508 3221221776 3221218004 1075115057 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10782 9964 1111 63 0 10719 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 330.229
CPU time (s): 330.231
CPU user time (s): 319.182
CPU system time (s): 11.0483
CPU usage (%): 100.001
Max. virtual memory (Kb): 43128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####