Integration of an LP Solver into Interval Constraint Propagation
This paper describes the integration of an LP solver into iSAT, a Satisfiability Modulo Theories solver that can solve Boolean combinations of linear and nonlinear constraints. iSAT is a tight integration of the well-known DPLL algorithm and interval constraint propagation allowing it to reason about linear and nonlinear constraints. As interval arithmetic is known to be less efficient on solving linear programs, we will demonstrate how the integration of an LP solver can improve the overall solving performance of iSAT.
How much geometry it takes to reconstruct a 2-manifold in R 3
Known algorithms for reconstructing a 2-manifold from a point sample in R 3 are naturally based on decisions/predicates that take the geometry of the point sample into account. Facing the always present problem of round-off errors that easily compromise the exactness of those predicate decisions, an exact and robust implementation of these algorithms is far from being trivial and typically requires employment of advanced datatypes for exact arithmetic, as provided by libraries like CORE, LEDA, or GMP. In this article, we present a new reconstruction algorithm, one whose main novelties is to throw away geometry information early on in the reconstruction process and to mainly operate combina…
Certifying feasibility and objective value of linear programs
Abstract We present an algorithm that certifies the feasibility of a linear program and computes a safe bound on its objective value while using rational arithmetic as little as possible. Our approach relies on computing a feasible solution that is as far as possible from satisfying an inequality at equality. To this end, we have to detect the set of inequalities that can only be satisfied at equality. Compared to previous approaches, our algorithm has a much higher success rate.
Fast and Accurate Bounds on Linear Programs
We present an algorithm that certifies the feasibility of a linear program while using rational arithmetic as little as possible. Our approach relies on computing a feasible solution of the linear program that is as far as possible from satisfying an inequality at equality. To realize such an approach, we have to detect the set of inequalities that can only be satisfied at equality. Compared to previous approaches for this problem our algorithm has a much higher rate of success.