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/manquinho/synthesis-ptl-cmos-circuits/normalized-9symml.opb
MD5SUM	48809ba02390b1184dab90aed89aff8e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4517
Optimality of the best value was proved	NO
Number of terms in the objective function	651
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	28138
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	28138
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	651
Total number of constraints	1658
Number of constraints which are clauses	1656
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42

Trace number 24368

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-09 21:18:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2207 boxname=wulflinc31 idbench=246 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  48809ba02390b1184dab90aed89aff8e  /oldhome/oroussel/tmp/wulflinc31/normalized-9symml.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-9symml.opb
IDLAUNCH: 2207
/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:        136264 kB
Buffers:         45552 kB
Cached:         818356 kB
SwapCached:        644 kB
Active:         493060 kB
Inactive:       373232 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        135984 kB
SwapTotal:     2097892 kB
SwapFree:      2096612 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5608 kB
Slab:            26356 kB
Committed_AS:    63652 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-09 21:21:23 (client local time) WITH STATUS 30 IN 191.883 SECONDS
stats: 2207 0 191.883 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c Initial problem consists of 651 variables and 1658 constraints.
c After prepocess the problem consists of 634 variables and 1380 constraints.
c preprocess terminated 0.697 s
c Initial Lower Bound: 4476
c Lower Bound Elapsed time: 0.548375
c Use computed LB before first solution.
c NEW SOLUTION FOUND: 4585 @ 10.813
c NEW SOLUTION FOUND: 4543 @ 11.473
c NEW SOLUTION FOUND: 4542 @ 64.624
c NEW SOLUTION FOUND: 4517 @ 78.264
s OPTIMUM FOUND
v -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 -x319 x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 x365 -x366 -x367 x368 -x369 x370 -x371 -x372 -x373 x374 -x375 x376 x377 x378 x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 x430 -x431 x432 -x433 -x434 -x435 -x436 x437 -x438 -x439 -x440 -x441 x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 x452 -x453 -x454 -x455 -x456 x457 x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 x484 -x485 x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 x495 x496 -x497 x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 x552 -x553 -x554 -x555 -x556 -x557 -x558 x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 x618 -x619 x620 -x621 -x622 -x623 -x624 -x625 -x626 x627 -x628 -x629 -x630 x631 x632 x633 -x634 -x635 x636 x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 x645 x646 x647 -x648 -x649 x650 -x651 
c Exit Code: 30
c Total time: 191.855 s
#### 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.91 0.95 0.90 2/54 3223
Raw data (stat): 3223 (runsolver) R 3222 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 703783806 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+10 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 5365 0 0 0 981 14 0 0 25 0 1 0 703783806 9175040 1385 4294967295 134512640 134714508 3221221792 3221218124 1075113231 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2240 1385 1111 63 0 2177 0
vsize: 8960
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 9995 0 0 0 1969 26 0 0 25 0 1 0 703783806 8671232 1401 4294967295 134512640 134714508 3221221792 3221219996 1077781665 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2117 1401 1111 63 0 2054 0
vsize: 8468
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 17399 0 0 0 2952 44 0 0 25 0 1 0 703783806 9056256 1458 4294967295 134512640 134714508 3221221792 3221220044 1077781665 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2211 1458 1111 63 0 2148 0
vsize: 8844
[startup+40.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 23581 0 0 0 3936 59 0 0 25 0 1 0 703783806 8888320 1501 4294967295 134512640 134714508 3221221792 3221220144 1074153779 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 2170 1501 1111 63 0 2107 0
vsize: 8680
[startup+50.0031 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 29105 0 0 0 4924 72 0 0 25 0 1 0 703783806 10555392 1785 4294967295 134512640 134714508 3221221792 3221218064 1074799107 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2577 1785 1111 63 0 2514 0
vsize: 10308
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 34175 0 0 0 5911 85 0 0 25 0 1 0 703783806 9277440 1596 4294967295 134512640 134714508 3221221792 3221220192 1074153770 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2265 1596 1111 63 0 2202 0
vsize: 9060
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 40685 0 0 0 6895 101 0 0 25 0 1 0 703783806 10895360 1902 4294967295 134512640 134714508 3221221792 3221218032 1075115768 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2660 1902 1111 63 0 2597 0
vsize: 10640
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 47793 0 0 0 7879 117 0 0 25 0 1 0 703783806 11190272 2027 4294967295 134512640 134714508 3221221792 3221217688 1074789548 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2732 2027 1111 63 0 2669 0
vsize: 10928
[startup+90.0045 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 55713 0 0 0 8860 136 0 0 25 0 1 0 703783806 10772480 1908 4294967295 134512640 134714508 3221221792 3221218984 1074138316 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2630 1918 1111 63 0 2567 0
vsize: 10520
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 62948 0 0 0 9842 154 0 0 25 0 1 0 703783806 10436608 1861 4294967295 134512640 134714508 3221221792 3221220096 1074153782 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 2548 1861 1111 63 0 2485 0
vsize: 10192
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 70089 0 0 0 10826 171 0 0 25 0 1 0 703783806 11005952 1988 4294967295 134512640 134714508 3221221792 3221220176 1074153782 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2687 1988 1111 63 0 2624 0
vsize: 10748
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 77225 0 0 0 11809 188 0 0 25 0 1 0 703783806 11186176 2056 4294967295 134512640 134714508 3221221792 3221220044 1077781665 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2731 2056 1111 63 0 2668 0
vsize: 10924
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 83304 0 0 0 12795 202 0 0 25 0 1 0 703783806 11030528 2024 4294967295 134512640 134714508 3221221792 3221220176 1074153792 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2693 2024 1111 63 0 2630 0
vsize: 10772
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 89604 0 0 0 13780 217 0 0 25 0 1 0 703783806 11575296 2152 4294967295 134512640 134714508 3221221792 3221219792 1074918597 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2826 2152 1111 63 0 2763 0
vsize: 11304
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 95412 0 0 0 14763 234 0 0 25 0 1 0 703783806 11091968 2039 4294967295 134512640 134714508 3221221792 3221219824 1077814665 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 2708 2039 1111 63 0 2645 0
vsize: 10832
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 99927 0 0 0 15752 246 0 0 25 0 1 0 703783806 13287424 2474 4294967295 134512640 134714508 3221221792 3221218032 1075115744 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 3244 2474 1111 63 0 3181 0
vsize: 12976
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 105914 0 0 0 16737 261 0 0 25 0 1 0 703783806 13316096 2374 4294967295 134512640 134714508 3221221792 3221218712 1074950114 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 3251 2374 1111 63 0 3188 0
vsize: 13004
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 112008 0 0 0 17721 277 0 0 25 0 1 0 703783806 13430784 2514 4294967295 134512640 134714508 3221221792 3221217760 1074872716 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 3279 2514 1111 63 0 3216 0
vsize: 13116
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 115613 0 0 0 18711 287 0 0 25 0 1 0 703783806 11558912 2153 4294967295 134512640 134714508 3221221792 3221220192 1074153782 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 2822 2153 1111 63 0 2759 0
vsize: 11288
[startup+191.904 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 3223
Raw data (stat): 3223 (bsolo_lpr_cuts) R 3222 7876 7672 0 -1 0 115613 0 0 0 18711 287 0 0 25 0 1 0 703783806 11558912 2153 4294967295 134512640 134714508 3221221792 3221220192 1074153782 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 2822 2153 1111 63 0 2759 0
vsize: 0

Child status: 30
Real time (s): 191.904
CPU time (s): 191.883
CPU user time (s): 188.951
CPU system time (s): 2.93155
CPU usage (%): 99.9891
Max. virtual memory (Kb): 13116
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	4517
#### END VERIFIER DATA ####