Computerized Proof of Fundamental Properties of the p-Median Problem Using Integer Linear Programming and a Theorem Prover

The p-median problem is one of the earliest location-allocation models used in spatial analysis and GIS. It involves locating a set of central facilities (the location decision) and allocating customers to these facilities (the allocation decision) so as to minimize the total transportation cost. It is important not only because of its wide use in spatial analysis but also because of its role as a unifying location model in GIS. A classical way of solving the p-median problem (dating back to the 1970s) is to formulate it as an Integer Linear Program (ILP), and then solve it using off-the-shelf solvers. Two fundamental properties of the p-median problem (and its variants) are the integral assignment property and the closest assignment property. They are the basis for the efficient formulation of the problem, and are important for studying the p-median problems and other location-allocation models. In this paper, we demonstrate that these fundamental properties of the p-median can be proven mechanically using integer linear programming and theorem provers under the program-as-proof paradigm. While these theorems have been proven informally, mechanized proofs using computers are fail-safe and contain no ambiguity. The presented proof method based on ILP and the associated definitions of problem data are general, and we expect that they can be generalized and extended to prove the theoretical properties of other spatial-optimization models, old or new.