Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
Mridul Aanjaneya, Santosh Nagarakatte
Abstract
This paper proposes a novel method to efficiently solve infeasible low-dimensional linear programs (LDLPs) with billions of constraints and a small number of unknown variables, where all the constraints cannot be satisfied simultaneously. We focus on infeasible linear programs generated in the RL ibm project for creating correctly rounded math libraries. Specifically, we are interested in generating a floating point solution that satisfies the maximum number of constraints. None of the existing methods can solve such large linear programs while producing floating point solutions. We observe that the convex hull can serve as an intermediate representation (IR) for solving infeasible LDLPs using the geometric duality between linear programs and convex hulls. Specifically, some of the constraints that correspond to points on the convex hull are precisely those constraints that make the linear program infeasible. Our key idea is to split the entire set of constraints into two subsets using the convex hull IR: (a) a set X of feasible constraints and (b) a superset V of infeasible constraints. Using the special structure of the RL ibm constraints and the presence of a method to check whether a system is feasible or not. we identify a superset of infeasible constraints by computing the convex hull in 2-dimensions. Subsequently, we identify the key constraints (i.e., basis constraints) in the set of feasible constraints X and use them to create a new linear program whose solution identifies the maximum set of constraints satisfiable in V while satisfying all the constraints in X . This new solver enabled us to improve the performance of the resulting RL ibm polynomials while solving the corresponding linear programs significantly faster.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext ba0df8fe-22ec-40e5-b457-cef4320143a2Cited by top-tier papers1
Ask how each one uses itBuilds on8
- PRIMA: general and precise neural network certification via scalable convex hull approximationsMark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel et al.POPL 2022 · 75 citations
- Provable repair of deep neural networksMatthew Sotoudeh, Aditya V. ThakurPLDI 2021 · 65 citations
- An approach to generate correctly rounded math libraries for new floating point variantsJay P. Lim, Mridul Aanjaneya, John L. Gustafson, Santosh NagarakattePOPL 2021 · 21 citations
- High performance correctly rounded math libraries for 32-bit floating point representationsJay P. Lim, Santosh NagarakattePLDI 2021 · 19 citations
- Architecture-Preserving Provable Repair of Deep Neural NetworksZhe Tao, Stephanie Nawas, Jacqueline Mitchell, Aditya V. ThakurPLDI 2023 · 15 citations
Related papers
- Progressive polynomial approximations for fast correctly rounded math librariesMridul Aanjaneya, Jay P. Lim, Santosh NagarakattePLDI 2022 · 9 citations
- ReLU Hull ApproximationZhongkui Ma, Jiaying Li, Guangdong BaiPOPL 2024 · 7 citations
- One polynomial approximation to produce correctly rounded results of an elementary function for multiple representations and rounding modesJay P. Lim, Santosh NagarakattePOPL 2022 · 15 citations
- Polynomial Invariant Generation for Floating-Point ProgramsXuran Cai, Liqian Chen, Hongfei FuCAV 2026
- Nonlinear Craig Interpolant GenerationTing Gan, Bican Xia, Bai Xue, Naijun Zhan et al.CAV 2020 · 14 citations
