PB'05 competition: run trace

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:

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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-stein45.opb
MD5SUM	980dd801f0823d520b47724b99fabded
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	30
Optimality of the best value was proved	NO
Number of terms in the objective function	45
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	45
Number of bits of the sum of numbers in the objective function	6
Biggest number in a constraint	22
Number of bits of the biggest number in a constraint	5
Biggest sum of numbers in a constraint	67
Number of bits of the biggest sum of numbers	7
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	45
Total number of constraints	376
Number of constraints which are clauses	330
Number of constraints which are cardinality constraints (but not clauses)	46
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	45

Trace number 18843

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 17:02:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17342 boxname=wulflinc3 idbench=1334 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  980dd801f0823d520b47724b99fabded  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-stein45.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-stein45.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-stein45.opb
IDLAUNCH: 17342
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        707788 kB
Buffers:         28672 kB
Cached:         275968 kB
SwapCached:          0 kB
Active:          43436 kB
Inactive:       264040 kB
HighTotal:      131008 kB
HighFree:        60424 kB
LowTotal:       903652 kB
LowFree:        647364 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            13828 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:03:58 (client local time) WITH STATUS 30 IN 90.1643 SECONDS
stats: 17342 0 90.1643 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 331 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................
c ---[   0]---> Sorter-cost:  718     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1860     4585 |     620       0        0     nan |  0.000 % |
c |       102 |    1849     4561 |     682     100      504     5.0 |  3.486 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  288     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       103 |    2112     5194 |     704      38      160     4.2 |  3.486 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       110 |    2140     5266 |     713      45      285     6.3 |  3.486 % |
c |       210 |    2140     5266 |     784     145     2308    15.9 |  4.650 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       213 |    2122     5223 |     707     148     2333    15.8 |  4.650 % |
c |       313 |    2122     5223 |     777     248     3905    15.7 |  5.680 % |
c |       463 |    2122     5223 |     855     398     6420    16.1 |  5.681 % |
c |       688 |    2122     5223 |     941     623    10026    16.1 |  5.681 % |
c |      1027 |    2122     5223 |    1035     962    16344    17.0 |  5.685 % |
c |      1533 |    2122     5223 |    1138     825    14513    17.6 |  5.682 % |
c |      2293 |    2122     5223 |    1252     803    13052    16.3 |  5.685 % |
c |      3434 |    2122     5223 |    1377    1114    17525    15.7 |  5.682 % |
c |      5143 |    2122     5223 |    1515    1192    18634    15.6 |  5.682 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5440 |    2159     5316 |     719    1489    23529    15.8 |  5.682 % |
c |      5541 |    2159     5316 |     790     846    11497    13.6 |  5.729 % |
c |      5691 |    2159     5316 |     869     573     6730    11.7 |  5.729 % |
c |      5916 |    2159     5316 |     956     798    10634    13.3 |  5.729 % |
c |      6253 |    2159     5316 |    1052    1135    15584    13.7 |  5.729 % |
c |      6759 |    2129     5250 |    1157    1072    13154    12.3 |  6.903 % |
c |      7519 |    2129     5250 |    1273    1077    11808    11.0 |  6.905 % |
c |      8658 |    2129     5250 |    1401    1397    17711    12.7 |  6.903 % |
c |     10366 |    2129     5250 |    1541    1392    19044    13.7 |  6.903 % |
c |     12929 |    2129     5250 |    1695    1186    12876    10.9 |  6.908 % |
c |     16773 |    2106     5199 |    1864    1036    11753    11.3 |  7.784 % |
c |     22540 |    2098     5181 |    2051    1346    15751    11.7 |  8.085 % |
c |     31190 |    2075     5129 |    2256    1744    21792    12.5 |  9.111 % |
c |     44165 |    2054     5083 |    2482    2014    23708    11.8 |  9.993 % |
c |     63626 |    2022     5012 |    2730    1965    23606    12.0 | 11.315 % |
c |     92818 |    1983     4923 |    3003    2056    27192    13.2 | 12.929 % |
c |    136608 |    1916     4767 |    3303    2424    27137    11.2 | 16.454 % |
c |    202292 |    1847     4591 |    3634    3519    42482    12.1 | 18.804 % |
c |    300818 |    1637     4051 |    3997    2137    22038    10.3 | 24.527 % |
c ==============================================================================
c [1mOptimal solution: 30[0m
s OPTIMUM FOUND
v V0001_bit0 V0002_bit0 V0003_bit0 V0004_bit0 V0005_bit0 -V0006_bit0 -V0007_bit0 -V0008_bit0 -V0009_bit0 -V0010_bit0 V0011_bit0 V0012_bit0 V0013_bit0 V0014_bit0 V0015_bit0 V0016_bit0 V0017_bit0 V0018_bit0 V0019_bit0 V0020_bit0 V0021_bit0 V0022_bit0 V0023_bit0 V0024_bit0 V0025_bit0 -V0026_bit0 -V0027_bit0 -V0028_bit0 -V0029_bit0 -V0030_bit0 V0031_bit0 V0032_bit0 V0033_bit0 V0034_bit0 V0035_bit0 V0036_bit0 V0037_bit0 V0038_bit0 V0039_bit0 V0040_bit0 -V0041_bit0 -V0042_bit0 -V0043_bit0 -V0044_bit0 -V0045_bit0
c _______________________________________________________________________________
c 
c restarts              : 33
c conflicts             : 332384         (3687 /sec)
c decisions             : 373752         (4146 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 90.1433 s
c _______________________________________________________________________________
#### 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.77 0.92 0.90 2/54 14744
Raw data (stat): 14744 (runsolver) R 14743 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488499584 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.81 0.92 0.90 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 434 0 0 0 997 1 0 0 25 0 1 0 488499584 3350528 412 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 818 412 603 41 0 777 0
vsize: 3272
[startup+20.0005 s]
Raw data (loadavg): 0.84 0.93 0.91 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 460 0 0 0 1997 1 0 0 25 0 1 0 488499584 3485696 438 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 851 438 603 41 0 810 0
vsize: 3404
[startup+30.001 s]
Raw data (loadavg): 0.86 0.93 0.91 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 489 0 0 0 2996 1 0 0 25 0 1 0 488499584 3485696 467 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 851 467 603 41 0 810 0
vsize: 3404
[startup+40.0011 s]
Raw data (loadavg): 0.88 0.93 0.91 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 501 0 0 0 3996 1 0 0 25 0 1 0 488499584 3620864 479 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 884 479 603 41 0 843 0
vsize: 3536
[startup+50.002 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 518 0 0 0 4996 1 0 0 25 0 1 0 488499584 3620864 496 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 884 496 603 41 0 843 0
vsize: 3536
[startup+60.0015 s]
Raw data (loadavg): 0.91 0.93 0.91 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 529 0 0 0 5997 1 0 0 25 0 1 0 488499584 3760128 507 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 918 507 603 41 0 877 0
vsize: 3672
[startup+70.0027 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 559 0 0 0 6997 1 0 0 25 0 1 0 488499584 3891200 537 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 950 537 603 41 0 909 0
vsize: 3800
[startup+80.0035 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 565 0 0 0 7997 1 0 0 25 0 1 0 488499584 3891200 543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 950 543 603 41 0 909 0
vsize: 3800
[startup+90.004 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 574 0 0 0 8997 1 0 0 25 0 1 0 488499584 3891200 552 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 950 552 603 41 0 909 0
vsize: 3800
[startup+90.1775 s]
Raw data (loadavg): 0.95 0.94 0.91 1/53 14744
Raw data (stat): 14744 (minisat+) R 14743 10720 10719 0 -1 0 574 0 0 0 8997 1 0 0 25 0 1 0 488499584 3891200 552 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 950 552 603 41 0 909 0
vsize: 0

Child status: 30
Real time (s): 90.1773
CPU time (s): 90.1643
CPU user time (s): 90.1433
CPU system time (s): 0.020996
CPU usage (%): 99.9856
Max. virtual memory (Kb): 3800
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	30
#### END VERIFIER DATA ####