Implementace řešíče pro lineární nerovnosti

V určitých kontextech (např. SAT řešiče) se často používá varianta simplexova algoritmu, která je inkrementální a vhodná pro řešení různých verzí podobných soustav nerovností. Student bude implementovat tuto variantu i v racionální i ve floating point aritmetice, a srovnává chování obou verzí.

Literatura: Dutertre, Bruno, and Leonardo De Moura. "A fast linear-arithmetic solver for DPLL (T)." International Conference on Computer Aided Verification. Springer Berlin Heidelberg, 2006.