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/submitted/een/normalized-mod008.opb
MD5SUM	18b325bb9311c83b0604c703bacc9a29
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	87
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	7499
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	758444
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.283956
Number of variables	319
Total number of constraints	6
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	186
Maximum length of a constraint	231

Trace number 7037

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-14 21:14:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5147 boxname=wulflinc20 idbench=396 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  18b325bb9311c83b0604c703bacc9a29  /oldhome/oroussel/tmp/wulflinc20/normalized-mod008.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc20/normalized-mod008.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mod008.opb
IDLAUNCH: 5147
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        809224 kB
Buffers:         36244 kB
Cached:         153432 kB
SwapCached:       2628 kB
Active:          58672 kB
Inactive:       136488 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        808972 kB
SwapTotal:     2097892 kB
SwapFree:      2095264 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24564 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:15:53 (client local time) WITH STATUS 30 IN 71.6341 SECONDS
stats: 5147 0 71.6341 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss.ss
c ---[   4]---> BDD-cost:  105
c ---[   3]---> BDD-cost:  168
c ---[   2]---> BDD-cost:  223
c ---[   1]---> BDD-cost:  180
c ---[   0]---> BDD-cost:  187
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2201     7583 |     733       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1995[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:61663     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  150623   354401 |   50207       0        0     nan |  0.000 % |
c |       101 |  150623   354401 |   55227     101      888     8.8 |  0.011 % |
c ==============================================================================
c [1mFound solution: 314[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       117 |  152437   359157 |   50812     117     1022     8.7 |  0.011 % |
c |       217 |  152437   359157 |   55893     217     3103    14.3 |  0.012 % |
c |       367 |  152437   359157 |   61482     367     7893    21.5 |  0.012 % |
c |       592 |  152244   358720 |   67630     547    12761    23.3 |  0.106 % |
c |       930 |  152244   358720 |   74393     885    28023    31.7 |  0.106 % |
c ==============================================================================
c [1mFound solution: 192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1021 |  153083   361007 |   51027     976    39378    40.3 |  0.106 % |
c |      1121 |  153083   361007 |   56129    1076    46498    43.2 |  0.107 % |
c ==============================================================================
c [1mFound solution: 140[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1149 |  153092   361028 |   51030    1104    48862    44.3 |  0.107 % |
c ==============================================================================
c [1mFound solution: 137[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1158 |  153100   361148 |   51033    1113    50249    45.1 |  0.107 % |
c ==============================================================================
c [1mFound solution: 135[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1217 |  153103   361155 |   51034    1172    67430    57.5 |  0.107 % |
c ==============================================================================
c [1mFound solution: 127[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1229 |  153112   361176 |   51037    1184    70759    59.8 |  0.107 % |
c ==============================================================================
c [1mFound solution: 126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1278 |  153429   361975 |   51143    1227    76380    62.2 |  0.107 % |
c |      1380 |  153429   361975 |   56257    1329   111878    84.2 |  0.189 % |
c |      1530 |  153429   361975 |   61883    1479   135009    91.3 |  0.189 % |
c |      1756 |  153429   361975 |   68071    1705   168953    99.1 |  0.189 % |
c |      2094 |  153429   361975 |   74878    2043   275166   134.7 |  0.189 % |
c ==============================================================================
c [1mFound solution: 124[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2279 |  153428   362077 |   51142    2227   317837   142.7 |  0.189 % |
c |      2383 |  153408   362032 |   56256    2330   356796   153.1 |  0.204 % |
c |      2533 |  153408   362032 |   61881    2480   390563   157.5 |  0.204 % |
c |      2761 |  153341   361884 |   68070    2705   437843   161.9 |  0.236 % |
c ==============================================================================
c [1mFound solution: 87[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:28340     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2942 |  210307   495182 |   70102    2795   482828   172.7 |  0.236 % |
c |      3043 |  210197   494932 |   77112    2894   502181   173.5 |  2.921 % |
c |      3193 |  210188   494913 |   84823    3042   528703   173.8 |  2.924 % |
c |      3418 |  209731   493861 |   93305    3254   567591   174.4 |  3.095 % |
c ==============================================================================
c [1mOptimal solution: 87[0m
s OPTIMUM FOUND
v -x0 -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318
c _______________________________________________________________________________
c 
c restarts              : 27
c conflicts             : 3532           (49 /sec)
c decisions             : 42247          (592 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 71.3711 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.92 0.98 0.90 2/54 9884
Raw data (stat): 9884 (runsolver) R 9883 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487750019 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9998 s]
Raw data (loadavg): 0.93 0.98 0.90 2/54 9884
Raw data (stat): 9884 (minisat+) R 9883 27565 27564 0 -1 0 5066 0 0 0 985 12 0 0 25 0 1 0 487750019 22982656 4889 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5611 4889 603 41 0 5570 0
vsize: 22444
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 9884
Raw data (stat): 9884 (minisat+) R 9883 27565 27564 0 -1 0 5233 0 0 0 1985 13 0 0 25 0 1 0 487750019 23744512 5056 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5797 5056 603 41 0 5756 0
vsize: 23188
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 9884
Raw data (stat): 9884 (minisat+) R 9883 27565 27564 0 -1 0 5322 0 0 0 2984 13 0 0 25 0 1 0 487750019 24145920 5145 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5895 5145 603 41 0 5854 0
vsize: 23580
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 9884
Raw data (stat): 9884 (minisat+) R 9883 27565 27564 0 -1 0 5415 0 0 0 3983 14 0 0 25 0 1 0 487750019 24535040 5238 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5238 603 41 0 5949 0
vsize: 23960
[startup+50.002 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 9884
Raw data (stat): 9884 (minisat+) R 9883 27565 27564 0 -1 0 5525 0 0 0 4982 15 0 0 25 0 1 0 487750019 24932352 5348 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6087 5348 603 41 0 6046 0
vsize: 24348
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 9884
Raw data (stat): 9884 (minisat+) R 9883 27565 27564 0 -1 0 7675 0 0 0 5977 20 0 0 25 0 1 0 487750019 36360192 7333 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8877 7333 603 41 0 8836 0
vsize: 35508
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 9884
Raw data (stat): 9884 (minisat+) R 9883 27565 27564 0 -1 0 7776 0 0 0 6976 21 0 0 25 0 1 0 487750019 36757504 7434 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8974 7434 603 41 0 8933 0
vsize: 35896
[startup+71.6606 s]
Raw data (loadavg): 0.97 0.98 0.91 1/53 9884
Raw data (stat): 9884 (minisat+) R 9883 27565 27564 0 -1 0 7776 0 0 0 6976 21 0 0 25 0 1 0 487750019 36757504 7434 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8974 7434 603 41 0 8933 0
vsize: 0

Child status: 30
Real time (s): 71.6603
CPU time (s): 71.6341
CPU user time (s): 71.4031
CPU system time (s): 0.230964
CPU usage (%): 99.9634
Max. virtual memory (Kb): 35896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	87
#### END VERIFIER DATA ####