Implementation of 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:
- Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories. Chapter on Satisfiability Modulo Theories. In E. Clarke and T. Henzinger and H. Veith editors, Handbook on Model Checking. Springer, 2014
- Timothy King, Clark Barrett and Cesare Tinelli. Leveraging Linear and Mixed Integer Programming for SMT. In Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD'14), Lausanne, Switzerland, 2014. IEEE
- G. Faure, R. Nieuwenhuis, A. Oliveras, and E. Rodriguez-Carbonell,
“SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and
Commercial Solvers,” in SAT, 2008, pp. 77–90.
