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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM4f5f6e30a602f3968daa9ca41c7da043
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2058
Optimality of the best value was proved NO
Number of terms in the objective function 133
Biggest coefficient in the objective function 128
Number of bits for the biggest coefficient in the objective function 8
Sum of the numbers in the objective function 9334
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 1024
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 9334
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 benchmark1.05284
Number of variables133
Total number of constraints126
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)56
Number of constraints which are nor clauses,nor cardinality constraints70
Minimum length of a constraint1
Maximum length of a constraint81

Trace number 25459 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-19 14:18:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19710 boxname=wulflinc31 idbench=1517 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  4f5f6e30a602f3968daa9ca41c7da043  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-neos5.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-neos5.opb
IDLAUNCH: 19710
/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:        729680 kB
Buffers:         32324 kB
Cached:         247604 kB
SwapCached:       5400 kB
Active:         219664 kB
Inactive:        66952 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        729428 kB
SwapTotal:     2097892 kB
SwapFree:      2091564 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            12788 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-19 14:21:05 (client local time) WITH STATUS 0 IN 129.89 SECONDS
stats: 19710 7 129.89 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c Initial problem consists of 133 variables and 73 constraints.
c After prepocess the problem consists of 133 variables and 73 constraints.
c preprocess terminated 0.291 s
c Initial Lower Bound: 1665
c Lower Bound Elapsed time: 0.0885
c Use computed LB before first solution.
c NEW SOLUTION FOUND: 2194 @ 1.082
c NEW SOLUTION FOUND: 2188 @ 1.127
c NEW SOLUTION FOUND: 2180 @ 1.167

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



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


#### 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.93 0.98 0.98 2/55 21828
Raw data (stat): 21828 (runsolver) R 21827 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 787677822 1056768 100 4294967295 134512640 135381576 3221221680 3221216896 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+9.99964 s]
Raw data (loadavg): 0.94 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 11295 0 0 0 951 45 0 0 25 0 1 0 787677822 17801216 3630 4294967295 134512640 134714508 3221221776 3221219284 1077378730 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 4346 3630 1111 63 0 4283 0
vsize: 17384
[startup+20.0005 s]
Raw data (loadavg): 0.95 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 24343 0 0 0 1906 90 0 0 25 0 1 0 787677822 27500544 6013 4294967295 134512640 134714508 3221221776 3221220700 1077781665 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 6714 6013 1111 63 0 6651 0
vsize: 26856
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 47801 0 0 0 2836 160 0 0 25 0 1 0 787677822 39301120 8758 4294967295 134512640 134714508 3221221776 3221220176 1074118815 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 9595 8758 1111 63 0 9532 0
vsize: 38380
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 69918 0 0 0 3773 223 0 0 25 0 1 0 787677822 46317568 10504 4294967295 134512640 134714508 3221221776 3221219720 1077410279 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 11308 10504 1111 63 0 11245 0
vsize: 45232
[startup+50.0012 s]
Raw data (loadavg): 0.97 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 90089 0 0 0 4719 277 0 0 25 0 1 0 787677822 51658752 11829 4294967295 134512640 134714508 3221221776 3221219892 1077378626 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 12612 11829 1111 63 0 12549 0
vsize: 50448
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 113558 0 0 0 5659 338 0 0 25 0 1 0 787677822 60354560 13709 4294967295 134512640 134714508 3221221776 3221220156 1077781665 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14735 13709 1111 63 0 14672 0
vsize: 58940
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 139246 0 0 0 6589 408 0 0 25 0 1 0 787677822 70475776 16008 4294967295 134512640 134714508 3221221776 3221218764 1077404742 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17206 16011 1111 63 0 17143 0
vsize: 68824
[startup+80.0022 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 165735 0 0 0 7519 478 0 0 25 0 1 0 787677822 77742080 17815 4294967295 134512640 134714508 3221221776 3221218792 1075110309 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18980 17815 1111 63 0 18917 0
vsize: 75920
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 187567 0 0 0 8459 537 0 0 25 0 1 0 787677822 82972672 19112 4294967295 134512640 134714508 3221221776 3221218764 1077404742 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 20192 19108 1111 63 0 20129 0
vsize: 81028
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 211958 0 0 0 9398 598 0 0 25 0 1 0 787677822 87662592 20347 4294967295 134512640 134714508 3221221776 3221219504 1075828514 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 21402 20347 1111 63 0 21339 0
vsize: 85608
[startup+110.003 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 238962 0 0 0 10329 667 0 0 25 0 1 0 787677822 94261248 21871 4294967295 134512640 134714508 3221221776 3221218224 1075132497 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 23013 21871 1111 63 0 22950 0
vsize: 92052
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 265106 0 0 0 11264 732 0 0 25 0 1 0 787677822 96903168 22646 4294967295 134512640 134714508 3221221776 3221220092 1073987088 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 23658 22646 1111 63 0 23595 0
vsize: 94632
[startup+129.924 s]
Raw data (loadavg): 0.99 0.98 0.98 1/54 21828
Raw data (stat): 21828 (bsolo_lpr_cuts) R 21827 7876 7672 0 -1 0 265106 0 0 0 11264 732 0 0 25 0 1 0 787677822 96903168 22646 4294967295 134512640 134714508 3221221776 3221220092 1073987088 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 23658 22646 1111 63 0 23595 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 129.923
CPU time (s): 129.89
CPU user time (s): 122.019
CPU system time (s): 7.8708
CPU usage (%): 99.9745
Max. virtual memory (Kb): 94632
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####