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 31723

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-05-27 06:12:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23150 boxname=wulflinc27 idbench=396 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  18b325bb9311c83b0604c703bacc9a29  /oldhome/oroussel/tmp/wulflinc27/normalized-mod008.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-mod008.opb
IDLAUNCH: 23150
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        879900 kB
Buffers:         33076 kB
Cached:         100812 kB
SwapCached:        684 kB
Active:          48172 kB
Inactive:        87816 kB
HighTotal:      131008 kB
HighFree:        27496 kB
LowTotal:       903652 kB
LowFree:        852404 kB
SwapTotal:     2097892 kB
SwapFree:      2096360 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5088 kB
Slab:            13020 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 06:13:56 (client local time) WITH STATUS 30 IN 73.7378 SECONDS
stats: 23150 0 73.7378 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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           (48 /sec)
c decisions             : 42247          (575 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 73.4608 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.91 2/54 29946
Raw data (stat): 29946 (runsolver) R 29945 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853902468 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+10.0006 s]
Raw data (loadavg): 0.93 0.98 0.91 2/55 29950
Raw data (stat): 29946 (minisat+_script) S 29945 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853902468 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 29950
Raw data (stat): 29946 (minisat+_script) S 29945 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853902468 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 29950
Raw data (stat): 29946 (minisat+_script) S 29945 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853902468 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 29950
Raw data (stat): 29946 (minisat+_script) S 29945 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853902468 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0028 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 29950
Raw data (stat): 29946 (minisat+_script) S 29945 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853902468 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 29950
Raw data (stat): 29946 (minisat+_script) S 29945 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853902468 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 29950
Raw data (stat): 29946 (minisat+_script) S 29945 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853902468 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+73.7705 s]
Raw data (loadavg): 0.97 0.98 0.91 1/53 29950
Raw data (stat): 29946 (minisat+_script) S 29945 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853902468 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 73.7699
CPU time (s): 73.7378
CPU user time (s): 73.5028
CPU system time (s): 0.234964
CPU usage (%): 99.9565
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	87
#### END VERIFIER DATA ####