Jan 15
Bits & Bytes Hosts Will Leeson on "Leveraging SMT Solver Instability"
Bits and Bytes hosts Will Leeson on "Leveraging SMT Solver Instability"
Abstract: The Boolean satisfiability (SAT) problem is a longstanding and well-studied problem in computer science. Given a formula consisting of boolean values, variables, and operators, the problem asks whether there is some assignment to the variables in the formula such that the formula evaluates to true. Satisfiability modulo theories (SMT) is a generalization of the SAT problem that allows formulas to contain various other data types (such as integers, arrays, or even strings). SMT solvers are tools that take an SMT formula or query as input and attempt to find a solution to the formula. To solve this task, SMT solvers search for possible assignments to variables that make the formula true. Ultimately, this search is guided by heuristics developed by the specific SMT solver's designers. Oftentimes, heuristics rely on patterns that developers expect in SMT queries. This reliance on heuristics causes SMT Solver Instability: a phenomenon where two semantically identical queries result in different solver runtimes. In this talk, I will show how simple changes to SMT formulas create equivalent queries with significant differences in SMT Solver performance. Additionally, I will demonstrate how we can leverage instability to improve the performance of SMT solvers in general using several machine learning techniques.
Join us for treats, beverages, community and conversation.