Quantifier Instantiations: To Mimic or To Revolt?
This work addresses a key bottleneck in automated reasoning for SMT solvers, offering an incremental improvement over existing instantiation methods.
The paper tackles the challenge of solving quantified formulas in SMT solvers by introducing a novel instantiation approach that dynamically learns from existing techniques and uses probabilistic context-free grammars to generate new terms, achieving a balance between exploitation and exploration in quantifier reasoning.
Quantified formulas pose a significant challenge for Satisfiability Modulo Theories (SMT) solvers due to their inherent undecidability. Existing instantiation techniques, such as e-matching, syntax-guided, model-based, conflict-based, and enumerative methods, often complement each other. This paper introduces a novel instantiation approach that dynamically learns from these techniques during solving. By treating observed instantiations as samples from a latent language, we use probabilistic context-free grammars to generate new, similar terms. Our method not only mimics successful past instantiations but also explores diversity by optionally inverting learned term probabilities, aiming to balance exploitation and exploration in quantifier reasoning.