Proportional symbol maps are a cartographic tool to assist in the visualization and analysis of quantitative data associated with specific locations (earthquake magnitudes, oil well production, temperature at weather stations, etc.). Symbol sizes are proportional to the magnitude of the quantities that they represent. We present a novel integer programming model to draw opaque disks on a map with the objective of maximizing the total visible border of all disks (an established measure of quality). We focus on drawings obtained by layering symbols on top of each other, known as stacking drawings. We introduce decomposition techniques, and several new families of facet-defining inequalities, which are implemented in a cut-and-branch algorithm. We assess the effectiveness of our approach through a series of computational experiments using real demographic and geophysical data. To the best of our knowledge, we are the first to provide provably optimal solutions to some of those problem instances.