Integer Linear Programming (ILP) is a powerful way to formulate sophisticated optimization models for making geospatial decisions in GIS. One of the general modeling constructs in ILP is the multi-level closest assignment (MLCA) constraint in the reliable facility location models with facility failure considerations. Compared with simpler constructs (such as the single-level closest assignment constraint), it involves assigning customers to backup facilities when the closer facility is unavailable. Part of the art of ILP modeling is to find suitable linear constructs to express such complex logic. The desired linear constructs may or may not exist. Even if a model construct is given, whether it can faithfully enforce the intended meaning is unknown. The correctness of the modeling construct is often shown based on informal reasoning or is not verified at all. Consequently, unverified ILP models may be (occasionally) infeasible or give wrong solutions. With the advancement of computerized theorem proving, it is becoming possible to mechanically prove the correctness of modeling constructs in ILP. In this article, we demonstrate that sophisticated model constructs such as MLCA can be proven using induction. This overcomes the inabilities of prior works to handle multiple levels of recursive definitions. Consequently, we are able to provide a first proof (formal or informal) that the specific MLCA form is mathematically correct. Given the generality of the induction method, we expect that it can be applied to prove the correctness of other types of models.
Lei et al. (Mon,) studied this question.