From MBQI to Enumerative Instantiation and Back

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.