From MBQI to Enumerative Instantiation and Back
Marek Dan\v{c}o, Petra Hozzov\'a, Mikol\'a\v{s} Janota

TL;DR
This paper explores the relationship between model-based and enumerative quantifier instantiation in SMT, proposing a combined approach that leverages the strengths of both methods to improve reasoning efficiency.
Contribution
It introduces a novel algorithm that integrates MBQI and EI techniques, providing initial experimental results on their combined effectiveness.
Findings
The combined algorithm can potentially improve instantiation quality.
Initial experiments show promising results in SMT solving.
The approach bridges semantic and syntactic instantiation methods.
Abstract
This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at the semantic level and guarantees to find a counterexample to a given a non-model. However, it may lead to weak instantiations. In contrast, EI strives for completeness by systematically enumerating terms at the syntactic level. However, such terms may not be counter-examples. Here we investigate the relation between the two techniques and report on our initial experiments of the proposed algorithm that combines the two.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Formal Methods in Verification · Natural Language Processing Techniques
