Congratulations to Profs. Mridul Aanjaneya and Santosh Nagarakatte for receiving an NSF SHF Small grant for their project "Efficient, Deterministic and Formally Certified Methods for Solving Low-dimensional Linear Programs with Floating-point Precision"! The award duration is for three years starting from July 1st, 2023 to June 30th, 2026. The total budget is $540,000.
Project Overview
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. This projects 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 for 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.
More information about this grant is available at the NSF website: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2312220&HistoricalAwards=false
