{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:07:55Z","timestamp":1760058475401,"version":"build-2065373602"},"reference-count":17,"publisher":"MDPI AG","issue":"4","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"Natural Science Foundation","doi-asserted-by":"publisher","award":["BCS-2215155","41971334"],"award-info":[{"award-number":["BCS-2215155","41971334"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China (NSFC)","doi-asserted-by":"publisher","award":["BCS-2215155","41971334"],"award-info":[{"award-number":["BCS-2215155","41971334"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IJGI"],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.3390\/ijgi14040162","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T05:03:07Z","timestamp":1744174987000},"page":"162","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Computerized Proof of Fundamental Properties of the p-Median Problem Using Integer Linear Programming and a Theorem Prover"],"prefix":"10.3390","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2385-9128","authenticated-orcid":false,"given":"Ting L.","family":"Lei","sequence":"first","affiliation":[{"name":"Department of Geography & Atmospheric Science, University of Kansas, Lawrence, KS 66045, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1378-4903","authenticated-orcid":false,"given":"Zhen","family":"Lei","sequence":"additional","affiliation":[{"name":"College of Automation, Wuhan University of Technology, Wuhan 430070, China"}]}],"member":"1968","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1287\/opre.12.3.450","article-title":"Optimum locations of switching centers and the absolute centers and medians of a graph","volume":"12","author":"Hakimi","year":"1964","journal-title":"Oper. Res."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1287\/opre.13.3.462","article-title":"Optimum distribution of switching centers in a communication network and some related graph theoretic problems","volume":"13","author":"Hakimi","year":"1965","journal-title":"Oper. Res."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1016\/S0377-2217(98)00186-6","article-title":"Strategic facility location: A review","volume":"111","author":"Owen","year":"1998","journal-title":"Eur. J. Oper. Res."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ejor.2003.11.032","article-title":"Location analysis: A synthesis and survey","volume":"165","author":"ReVelle","year":"2005","journal-title":"Eur. J. Oper. Res."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1111\/j.1435-5597.1974.tb00902.x","article-title":"The maximal covering location problem","volume":"32","author":"Church","year":"1974","journal-title":"Pap. Reg. Sci. Assoc."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1111\/j.1538-4632.1976.tb00547.x","article-title":"Theoretical and computational links between the p-median, location set-covering, and the maximal covering location problem","volume":"8","author":"Church","year":"1976","journal-title":"Geogr. Anal."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1068\/a160305","article-title":"The p-median structure as a unified linear model for location-allocation analysis","volume":"16","author":"Hillsman","year":"1984","journal-title":"Environ. Plan. A"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1111\/j.1538-4632.1970.tb00142.x","article-title":"Central facilities location","volume":"2","author":"ReVelle","year":"1970","journal-title":"Geogr. Anal."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0966-8349(97)00001-6","article-title":"Closest assignment constraints and location models: Properties and structure","volume":"4","author":"Gerrard","year":"1996","journal-title":"Locat. Sci."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1111\/j.1538-4632.1970.tb00864.x","article-title":"Central facilities location under an investment constraint","volume":"2","author":"Rojeski","year":"1970","journal-title":"Geogr. Anal."},{"key":"ref_11","unstructured":"Swain, R.W. (1971). A Decomposition Algorithm for a Class of Facility Location Problems. [Ph.D. Thesis, Cornell University]."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1111\/j.1467-8306.2004.00410.x","article-title":"Identifying critical infrastructure: The median and covering facility interdiction problems","volume":"94","author":"Church","year":"2004","journal-title":"Ann. Assoc. Am. Geogr."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1177\/0160017610386483","article-title":"Constructs for multilevel closest assignment in location modeling","volume":"34","author":"Lei","year":"2011","journal-title":"Int. Reg. Sci. Rev."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Church, R.L., and Cohon, J.L. (1976). Multiobjective Location Analysis of Regional Energy Facility Siting Problems, Brookhaven National Laboratory. BNL Report 50567.","DOI":"10.2172\/7294043"},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1111\/j.1435-5597.1983.tb00807.x","article-title":"Generalized coverage models and public facility location","volume":"53","author":"Church","year":"1983","journal-title":"Pap. Reg. Sci."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"de Moura, L., and Ullrich, S. (2021, January 12\u201315). The lean 4 theorem prover and programming language. Proceedings of the Automated Deduction\u2013CADE 28: 28th International Conference on Automated Deduction, Virtual Event. Proceedings 28.","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1080\/13658816.2015.1041959","article-title":"A unified approach for location-allocation analysis: Integrating GIS, distributed computing and spatial optimization","volume":"30","author":"Lei","year":"2016","journal-title":"Int. J. Geogr. Inf. Sci."}],"container-title":["ISPRS International Journal of Geo-Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2220-9964\/14\/4\/162\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:13:10Z","timestamp":1760029990000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2220-9964\/14\/4\/162"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":17,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2025,4]]}},"alternative-id":["ijgi14040162"],"URL":"https:\/\/doi.org\/10.3390\/ijgi14040162","relation":{},"ISSN":["2220-9964"],"issn-type":[{"type":"electronic","value":"2220-9964"}],"subject":[],"published":{"date-parts":[[2025,4,9]]}}}