«APR SEP Oct 6 «2015 2020 2021 5 captures 12 Sep 15 - 6 Sep 20

Close Help

Implementation of a Solver for Linear Constraints

In some contexts, (e.g., SAT solvers) a variant of the simplex algorithm is used, that allows for light-weight incremental solving of linear constraints. In the thesis, the students implements such a solver in both rational and floating point arithmetic and compares the behavior of both versions. Literature: Dutertre, Bruno, and Leonardo De Moura. "A fast linear-arithmetic solver for DPLL (T)." International Conference on Computer Aided Verification. Springer Berlin Heidelberg, 2006.