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-pipex.opb
MD5SUM	b9c1029cc1d97a8d60e984f96f5d3267
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	788263
Optimality of the best value was proved	NO
Number of terms in the objective function	48
Biggest coefficient in the objective function	107865
Number of bits for the biggest coefficient in the objective function	17
Sum of the numbers in the objective function	2514082
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	107865
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	2514082
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	48
Total number of constraints	73
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	64
Number of constraints which are nor clauses,nor cardinality constraints	9
Minimum length of a constraint	1
Maximum length of a constraint	16

Trace number 15515

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 05:01:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17198 boxname=wulflinc10 idbench=1323 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b9c1029cc1d97a8d60e984f96f5d3267  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-pipex.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-pipex.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-pipex.opb
IDLAUNCH: 17198
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        552840 kB
Buffers:         32552 kB
Cached:         426516 kB
SwapCached:          0 kB
Active:         129088 kB
Inactive:       332440 kB
HighTotal:      131008 kB
HighFree:          672 kB
LowTotal:       903652 kB
LowFree:        552168 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            14556 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:03:57 (client local time) WITH STATUS 0 IN 121.354 SECONDS
stats: 17198 7 121.354 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################
c   -- Clauses(.)/Splits(s): (none)
c ---[  40]---> BDD-cost:  346
c ---[  39]---> BDD-cost:  318
c ---[  38]---> BDD-cost:  303
c ---[  37]---> BDD-cost:   86
c ---[  36]---> BDD-cost:  103
c ---[  35]---> BDD-cost:   93
c ---[  34]---> BDD-cost:  147
c ---[  33]---> BDD-cost:  315
c ---[  32]---> BDD-cost:  353
c ---[  30]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  26]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    3
c ---[   6]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7108    20822 |    2369       0        0     nan |  0.000 % |
c |       100 |    7108    20822 |    2605     100     1238    12.4 |  1.190 % |
c ==============================================================================
c [1mFound solution: 832532[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 9882     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       144 |   30943    76564 |   10314     144     2085    14.5 |  1.190 % |
c |       244 |   30943    76564 |   11345     244     4098    16.8 |  0.242 % |
c ==============================================================================
c [1mFound solution: 831684[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       335 |   31275    77391 |   10425     335     5857    17.5 |  0.242 % |
c |       435 |   31275    77391 |   11467     435     7919    18.2 |  0.247 % |
c ==============================================================================
c [1mFound solution: 827994[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       500 |   31383    77694 |   10461     500     9458    18.9 |  0.247 % |
c |       600 |   31383    77694 |   11507     600    11250    18.8 |  0.254 % |
c |       750 |   31383    77694 |   12657     750    14080    18.8 |  0.254 % |
c ==============================================================================
c [1mFound solution: 816894[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       812 |   31404    77781 |   10468     812    15202    18.7 |  0.254 % |
c |       912 |   31404    77781 |   11514     912    16958    18.6 |  0.263 % |
c |      1062 |   31404    77781 |   12666    1062    19337    18.2 |  0.263 % |
c |      1287 |   31404    77781 |   13932    1287    23363    18.2 |  0.263 % |
c |      1626 |   31404    77781 |   15326    1626    29711    18.3 |  0.263 % |
c ==============================================================================
c [1mFound solution: 821402[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1889 |   31419    77817 |   10473    1889    34805    18.4 |  0.263 % |
c |      1990 |   31419    77817 |   11520    1990    36137    18.2 |  0.272 % |
c |      2141 |   31419    77817 |   12672    2141    38815    18.1 |  0.272 % |
c |      2366 |   31419    77817 |   13939    2366    42614    18.0 |  0.272 % |
c |      2703 |   31419    77817 |   15333    2703    48548    18.0 |  0.272 % |
c |      3210 |   31419    77817 |   16866    3210    58102    18.1 |  0.272 % |
c |      3969 |   31419    77817 |   18553    3969    72687    18.3 |  0.272 % |
c |      5109 |   31419    77817 |   20408    5109    94220    18.4 |  0.272 % |
c |      6818 |   31419    77817 |   22449    6818   130077    19.1 |  0.272 % |
c ==============================================================================
c [1mFound solution: 816443[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7146 |   31429    77841 |   10476    7146   135662    19.0 |  0.272 % |
c |      7247 |   31429    77841 |   11523    7247   137676    19.0 |  0.281 % |
c |      7397 |   31429    77841 |   12675    7397   140278    19.0 |  0.281 % |
c |      7622 |   31429    77841 |   13943    7622   145185    19.0 |  0.281 % |
c |      7959 |   31429    77841 |   15337    7959   151775    19.1 |  0.281 % |
c |      8465 |   31429    77841 |   16871    8465   164415    19.4 |  0.281 % |
c |      9224 |   31429    77841 |   18558    9224   178148    19.3 |  0.281 % |
c |     10363 |   31429    77841 |   20414   10363   196887    19.0 |  0.281 % |
c |     12071 |   31429    77841 |   22456   12071   225834    18.7 |  0.281 % |
c ==============================================================================
c [1mFound solution: 815897[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12074 |   31542    78117 |   10514   12074   226487    18.8 |  0.281 % |
c ==============================================================================
c [1mFound solution: 815057[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12111 |   31658    78418 |   10552    6074   106906    17.6 |  0.281 % |
c ==============================================================================
c [1mFound solution: 813882[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12156 |   31675    78471 |   10558    6119   108047    17.7 |  0.281 % |
c |     12256 |   31675    78471 |   11613    6219   110177    17.7 |  0.306 % |
c |     12406 |   31675    78471 |   12775    6369   115170    18.1 |  0.306 % |
c |     12631 |   31675    78471 |   14052    6594   123857    18.8 |  0.306 % |
c |     12970 |   31675    78471 |   15457    6933   132845    19.2 |  0.306 % |
c ==============================================================================
c [1mFound solution: 807462[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13453 |   31694    78518 |   10564    7416   144615    19.5 |  0.306 % |
c ==============================================================================
c [1mFound solution: 812028[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 5 3 3 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13503 |   31741    78637 |   10580    7466   146081    19.6 |  0.306 % |
c |     13603 |   31741    78637 |   11638    7566   148793    19.7 |  0.323 % |
c |     13753 |   31741    78637 |   12801    7716   152581    19.8 |  0.323 % |
c |     13979 |   31741    78637 |   14081    7942   157015    19.8 |  0.323 % |
c |     14316 |   31741    78637 |   15490    8279   164752    19.9 |  0.323 % |
c |     14825 |   31741    78637 |   17039    8788   176021    20.0 |  0.323 % |
c |     15587 |   31725    78601 |   18743    9549   191956    20.1 |  0.358 % |
c |     16726 |   31725    78601 |   20617   10688   212658    19.9 |  0.358 % |
c |     18434 |   31725    78601 |   22679   12396   246185    19.9 |  0.358 % |
c |     20996 |   31725    78601 |   24947   14958   290686    19.4 |  0.358 % |
c |     24840 |   31687    78515 |   27441   18800   363161    19.3 |  0.439 % |
c |     30606 |   31687    78515 |   30185   24566   460497    18.7 |  0.439 % |
#### 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.71 0.91 0.89 2/54 24796
Raw data (stat): 24796 (runsolver) R 24795 25347 25346 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 484188265 1052672 97 4294967295 134512640 135381576 3221224432 3221219872 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.99964 s]
Raw data (loadavg): 0.75 0.91 0.89 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1293 0 0 0 996 3 0 0 25 0 1 0 484188265 7135232 1265 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1742 1265 603 41 0 1701 0
vsize: 6968
[startup+19.9998 s]
Raw data (loadavg): 0.79 0.91 0.89 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1405 0 0 0 1995 4 0 0 25 0 1 0 484188265 7671808 1377 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1873 1377 603 41 0 1832 0
vsize: 7492
[startup+30.0008 s]
Raw data (loadavg): 0.82 0.92 0.89 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1517 0 0 0 2994 4 0 0 25 0 1 0 484188265 8114176 1489 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1981 1489 603 41 0 1940 0
vsize: 7924
[startup+40.0003 s]
Raw data (loadavg): 0.85 0.92 0.89 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1606 0 0 0 3994 5 0 0 25 0 1 0 484188265 8527872 1578 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2082 1578 603 41 0 2041 0
vsize: 8328
[startup+50.0006 s]
Raw data (loadavg): 0.87 0.92 0.89 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1622 0 0 0 4994 5 0 0 25 0 1 0 484188265 8527872 1594 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2082 1594 603 41 0 2041 0
vsize: 8328
[startup+60.0006 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1633 0 0 0 5994 5 0 0 25 0 1 0 484188265 8527872 1605 4294967295 134512640 134672761 3221224544 3221223680 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2082 1605 603 41 0 2041 0
vsize: 8328
[startup+70.0012 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1699 0 0 0 6993 5 0 0 25 0 1 0 484188265 8933376 1671 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2181 1671 603 41 0 2140 0
vsize: 8724
[startup+80.0015 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1791 0 0 0 7993 5 0 0 25 0 1 0 484188265 9379840 1763 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2290 1763 603 41 0 2249 0
vsize: 9160
[startup+90.001 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1883 0 0 0 8993 6 0 0 25 0 1 0 484188265 9662464 1855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2359 1855 603 41 0 2318 0
vsize: 9436
[startup+100.002 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 1958 0 0 0 9992 6 0 0 25 0 1 0 484188265 10063872 1930 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2457 1930 603 41 0 2416 0
vsize: 9828
[startup+110.002 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 2027 0 0 0 10992 6 0 0 25 0 1 0 484188265 10354688 1999 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2528 1999 603 41 0 2487 0
vsize: 10112
[startup+120.003 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 2124 0 0 0 11992 6 0 0 25 0 1 0 484188265 10780672 2096 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2632 2096 603 41 0 2591 0
vsize: 10528
[startup+121.36 s]
Raw data (loadavg): 0.96 0.93 0.90 1/53 24796
Raw data (stat): 24796 (minisat+) R 24795 25347 25346 0 -1 0 2124 0 0 0 11992 6 0 0 25 0 1 0 484188265 10780672 2096 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2632 2096 603 41 0 2591 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 121.359
CPU time (s): 121.354
CPU user time (s): 121.272
CPU system time (s): 0.081987
CPU usage (%): 99.9952
Max. virtual memory (Kb): 10528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####