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

 

Abstract:

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.