Fair and Adventurous Enumeration of Quantifier Instantiations

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00354431" target="_blank" >RIV/68407700:21730/21:00354431 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_35" target="_blank" >https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_35</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.34727/2021/isbn.978-3-85448-046-4_35" target="_blank" >10.34727/2021/isbn.978-3-85448-046-4_35</a>

Result language

angličtina

Original language name

Fair and Adventurous Enumeration of Quantifier Instantiations

Original language description

SMT solvers generally tackle quantifiers by instantiating their variables with tuples of terms from the ground part of the formula. Recent enumerative approaches for quantifier instantiation consider tuples of terms in some heuristic order. This paper studies different strategies to order such tuples and their impact on performance. We decouple the ordering problem into two parts. First is the order of the sequence of terms to consider for each quantified variable, and second is the order of the instantiation tuples themselves. While the most and least preferred tuples, i.e. those with all variables assigned to the most or least preferred terms, are clear, the combinations in between allow flexibility in an implementation. We look at principled strategies of complete enumeration, where some strategies are more fair, meaning they treat all the variables the same but some strategies may be more adventurous, meaning that they may venture further down the preference list. We further describe new techniques for discarding irrelevant instantiations which are crucial for the performance of these strategies in practice. These strategies are implemented in the SMT solver cvc5, where they contribute to the diversification of the solver’s configuration space, as shown by our experimental results.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/LL1902" target="_blank" >LL1902: Powering SMT Solvers by Machine Learning</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2021

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021

ISBN

978-3-85448-046-4

ISSN

—

e-ISSN

—

Number of pages

5

Pages from-to

256-260

Publisher name

TU Wien

Place of publication

Wien

Event location

Yale

Event date

Oct 20, 2021

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—