Fair and Adventurous Enumeration of Quantifier Instantiations

Kód výsledku v IS VaVaI

RIV/68407700:21730/21:00354431 - isvavai.cz

Výsledek na webu

https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_35

DOI - Digital Object Identifier

10.34727/2021/isbn.978-3-85448-046-4_35

Jazyk výsledku

angličtina

Název v původním jazyce

Fair and Adventurous Enumeration of Quantifier Instantiations

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Fair and Adventurous Enumeration of Quantifier Instantiations

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

LL1902: Obohacování SMT řešičů pomocí strojového učení

Návaznosti

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

Rok uplatnění

2021

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

ISBN

978-3-85448-046-4

ISSN

—

e-ISSN

—

Počet stran výsledku

5

Strana od-do

256-260

Název nakladatele

TU Wien

Místo vydání

Wien

Místo konání akce

Yale

Datum konání akce

20. 10. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—