SHF: Small: Efficient, Deterministic and Formally Certified Methods for Solving Low-dimensional Linear Programs with Floating-point Precision

Linear programs (LPs) are widely used in numerous domains, such as computer arithmetic, robotics, machine learning, computer vision and databases. Existing LP solvers, which have been steadily improved after decades of research, can solve several tens of thousands of constraints. These solvers focus on linear programs where the number of constraints is of the same order of magnitude as the number of variables (i.e., high-dimensional linear programs). However, in many domains, linear programs with billions of constraints but a small number of variables are common. Such linear programs are called "low-dimensional linear programs" (LDLPs). Unfortunately, existing LP solvers cannot solve them. This project aims to develop efficient and deterministic methods to solve low-dimensional linear programs that can be formally verified to produce the correct solution with floating-point precision. In contrast to existing solvers for LP problems that generate real coefficients using rational arithmetic, this project's novelty lies in generating solutions with floating-point (FP) precision using ideas from computational geometry. The project's impacts are in designing scalable LDLP solvers that can handle both linear programs that are full-rank (i.e., there exists a single solution that satisfies all constraints) and those that are not full-rank, with potentially billions of constraints. In the latter case, this project will generate a solution that satisfies the maximum number of constraints. This project will rigorously evaluate the efficacy of the LDLP solver in various domains and has the potential of expanding the use of formal methods to a wider class of applications. It will also educate practitioners, graduate and undergraduate students on foundational abstractions in computing. This project makes the following foundational advances in designing LDLP solvers: (a) It will develop an algorithm to solve LDLPs that are full rank while also identifying the key constraints. A solution that satisfies these key constraints also satisfies all the other constraints. (b) It will develop a novel method for identifying the key constraints by constructing the convex hull in high dimensions using the geometric duality between hyperplanes and points. (c) It will develop a new LP formulation using the key constraints whose solution satisfies the maximum number of constraints in the original non-full-rank LDLP. (d) It will develop an approach to formally verify the construction of the convex hull in high dimensions, especially to handle the degenerate cases that may arise in the presence of numerical and rounding errors, and (e) it will evaluate the LDLP solver in two practical applications: (1) generating correctly rounded math libraries for elementary functions, and (2) fast training of support vector machines for machine learning. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.