Bi-Weekly Talk:Bi-Weekly Talk: Jasper Nalbach: A novel idea for solving satisfiability modulo linear real arithmetic
Wednesday, September 09, 2020, 10:30am
Location: Online Session
Speaker: Jasper Nalbach
Satisfiability modulo theories (SMT) solving is a technology for checking the satisfiability of quantifier-free first-order logic formulas, i.e. Boolean combinations of constraints from some theories. For solving the theory of linear real arithmetic, the Simplex algorithm has successfully been adapted for the DPLL(T) framework. However, this approach reaches its limits at instances with complex Boolean structure. This talk presents a novel method based on the ideas of Simplex attempting to overcome these limits by interleaving Simplex pivot steps with the SAT solving process.