Efficient certification of feasibility and objective value of linear programs and its applications

The use of linear programming in various areas has increased with the significant improvement of specialized solvers. Linear programs are used as such to model practical problems, or as subroutines in algorithms such as formal proofs or branch-and-cut frameworks. In many situations a certified answer is needed, for example the guarantee that the linear program is feasible or infeasible, or a provably safe bound on its objective value. Most of the available solvers work with floating-point arithmetic and are thus subject to its shortcomings such as rounding errors or underflow, therefore they can deliver incorrect answers. While adequate for some applications, this is unacceptable for critical applications like flight controlling or nuclear plant management due to the potential catastrophic consequences. We propose a method that gives a certified answer whether a linear program is feasible or infeasible, or returns unknown'. The advantage of our method is that it is reasonably fast and rarely answers unknown'. It works by computing a safe solution that is in some way the best possible in the relative interior of the feasible set. To certify the relative interior, we employ exact arithmetic, whose use is nevertheless limited in general to critical places, allowing us to rnremain computationally efficient. Moreover, when certain conditions are fulfilled, our method is able to deliver a provable bound on the objective value of the linear program. We test our algorithm on typical benchmark sets and obtain higher rates of success compared to previous approaches for this problem, while keeping the running times acceptably small. The computed objective value bounds are in most of the cases very close to the known exact objective values. We prove the usability of the method we developed by additionally employing a variant of it in a different scenario, namely to improve the results of a Satisfiability Modulo Theories solver. Our method is used as a black box in the nodes of a branch-and-bound tree to implement conflict learning based on the certificate of infeasibility for linear programs consisting of subsets of linear constraints. The generated conflict clauses are in general small and give good rnprospects for reducing the search space. Compared to other methods we obtain significant improvements in the running time, especially on the large instances.Der Einsatz von linearer Programmierung in verschiedenen Bereichen ist mit dem signifikanten Fortschritt spezialisierter Löser gewachsen. Lineare Programme finden Anwendung in der Modellierung von praktischen Problemen und als Unterprogramme in Algorithmen, wie zum Beispiel bei formalen Beweisen oder bei branch-and-cut Ansätzen. In vielen Situationen wird eine zertifizierte Antwort benötigt, in Form einer Garantie, dass das lineare Programm lösbar oder unlösbar ist, oder in Form einer beweisbar sicheren Schranke an den Zielfunktionswert. Die meisten verfügbaren Löser arbeiten mit Gleitkommaarithmetik und unterliegen somit den bekannten Defiziten wie Rundungsfehlern oder Unterläufen, welche dazu führen können, dass sie fehlerhafte Antworten liefern. Während dies für die meisten Anwendungen ausreichend ist, ist die Unsicherheit aufgrund der potenziell katastrophalen Folgen für kritische Anwendungen, wie zum Beispiel im Bereich der Flugsicherung oder Kraftwerkssteuerung, untragbar. Wir präsentieren eine Methode, die eine zertifizierte Antwort auf die Frage ob ein lineares Programm lösbar oder unlösbar ist, liefert und ansonsten mit unbekannt' antwortet. Der Vorteil unserer Methode ist, dass sie eine vernünftige Laufzeitrnbesitzt und nur selten unbekannt' zurückliefert. Sie berechnet eine sichere Lösung, welche die beste im relativen Inneren des Lösungsraums ist. Um das relative Innere sicher zu berechnen, verwenden wir exakte Arithmetik, deren Einsatz nur in kritischen Berechnungsschritten akzeptiert wird, damit der Algorithmus laufzeittechnisch effizient bleibt. Des Weiteren ist unsere Methode bei Erfüllbarkeit besonderer Bedingungen in der Lage eine beweisbare Schranke an den Zielfunktionswert des linearen Programms zu liefern. Wir testen unseren Algorithmus an typischen Benchmark-Instanzen und erzielen höhere Erfolgsraten im Vergleich zu vorherigen Ansätzen für dieses Problem, während die Laufzeit akzeptabel klein bleibt. Die berechneten Schranken liegen in den meisten Fällen sehr nah an den bekannten Zielfunktionswerten. Die Einsatzfähigkeit unserer Methode zeigen wir zusätzlich durch die Entwicklung einer Variante, die die Resultate eines Satisfiability Modulo Theories Lösers verbessert. Unsere Methode wird als Black Box in den Knoten eines branch-and-bound Baums genutzt, um ein konfliktgesteuertes Lernverfahren zu unterstützen, das auf den Unlösbarkeits-Zertifikaten linearer Programme beruht, die aus Teilmengen linearer Nebenbedingungen bestehen. Die generierten Konfliktklauseln sind im Allgemeinen klein und liefern somit gute Beschränkungen des Suchraums. Verglichen mit anderen Methoden erhalten wir durch unseren Ansatz, insbesondere bei großen Instanzen, eine signifikante Reduzierung der Laufzeit