Challenges in State-of-the-Art Bit-Precise Reasoning

This lecture by Aina Niemetz from Stanford University explores the ongoing challenges in bit-precise reasoning within Satisfiability Modulo Theories (SMT). Dive into the complexities of efficiently handling bit-vector constraints, a critical requirement for formal methods applications across industry and academia. Learn about the scalability issues that arise with increasing bit widths, particularly when dealing with arithmetic operators. The talk examines bit-blasting—the dominant state-of-the-art approach that eagerly reduces problems to propositional logic—and explains how this technique, despite potentially increasing formula size significantly, remains surprisingly effective in practice thanks to advanced SAT solvers. Discover the latest techniques in the field, including a recent procedure designed to improve bit-blasting scalability, as part of the Simons Institute for the Theory of Computing and SLMath Joint Workshop on AI for Mathematics and Theoretical Computer Science.