| ||||
| ||||
![]() Title:Quantifier Instantiations: To Mimic or To Revolt? Conference:SMT 2025 Tags:Probabilistic Term Generation, Quantifier Instantiation and Satisfiability Modulo Theories Abstract: 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. Quantifier Instantiations: To Mimic or To Revolt? ![]() Quantifier Instantiations: To Mimic or To Revolt? | ||||
Copyright © 2002 – 2025 EasyChair |