Computerized Proof of Fundamental Properties of the p-Median Problem Using Integer Linear Programming and a Theorem Prover
Bibliographic Data
| ID | 22032756 |
|---|---|
| Authors | Ting L Lei (0000-0003-2385-9128, University of Kansas), Zhen Lei (0000-0002-0826-9763, Wuhan University of Technology, corresponding author) |
| Year | 2025 |
| Volume | 14 |
| Issue | 4 |
| Pages | 162 |
| Publication date | 2025-04-09 |
| Open Access | Yes |
| Type | ARTICLE |
| Venue | ISPRS International Journal of Geo-Information (JOURNAL) |
| Journal identifiers | ISSN: 2220-9964 • E-ISSN: 2220-9964 |
| Publisher | MDPI AG (PUBLISHER • IT) |
| DOI | 10.3390/ijgi14040162 |
| OpenAlex | W4409280247 |
| Language | EN |
| Citations received | 1 |
| References cited | 16 |
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
Algorithm · Automated theorem proving · Branch and price · Discrete mathematics · Gas meter prover · Integer programming · Linear programming · Mathematical proof · Programming language · Computer Science · Evacuation and Crowd Dynamics · Facility Location and Emergency Management · Mathematics · Medicine · Vehicle Routing Optimization Methods
Central Facilities Location
Optimum Locations of Switching Centers and the Absolute Centers and Medians of a Graph
Generalized Coverage Models and Public Facility Location
The Maximal Covering Location Problem
Identifying Critical Infrastructure
The p-Median Structure as a Unified Linear Model for Location-Allocation Analysis
| Citations per year | 1 |
|---|---|
| Citation span | 2026 - 2026 (1) |
| Highly cited | No |